capture the behavior of the human or
physical world. Nevertheless, SP is formally stated and the code is guaranteed to satisfy SP. Here, I deliberately
decoupled the correctness of verification from the specification process.
Existing efforts validating and testing
specifications are, of course, valuable
and complementary to the certification process.
Since a dependability claim is made
regarding only the formal machine
model, the TCB of such a certified
framework consists of just the consistency proof of the metalogic and the
integrity of the proof checker, both
of which should be demonstrable by
independent third parties (such as
through the peer-review process of a
top-quality journal). If the computer
science community would agree on a
single metalogic (a good thing), this
task of standardizing a metalogic
would need to be done only once. Certified software would then no longer
be the weakest link in a dependable
system.
Mechanized metalogic. A key enabling technology for certified software is to write formal proofs and
specifications as typed functional
programs, then have a computer automatically check the validity of the
proofs, in the same way a static type-checker does type-checking. This idea
came from the well-known Curry-How-ard correspondence referring to the
generalization of a syntactic analogy
between systems of formal logic and
computational calculi first discovered
by the American logicians Haskell Curry and William Howard. Most advances for developing large-scale machine-checkable proofs were made only
during the past 10 years; see an excellent survey by Barendregt and Geuvers2
and a 2008 overview article by Hales. 11
In the context of certified software,
a few more requirements must be addressed: The logic must be consistent
and expressive so software developers
can express everything they want to
say. It must also support explicit machine-checkable proof objects and be
simple enough that the proof checker
can be hand-verified for correctness.
Because software components may
be developed using different program-
ming languages and certified using
different domain-specific logics and
type systems, mechanized metalogic
must also support meta-reasoning. It
can be used to represent the syntax,
inference rules, and meta-proofs (for
their soundness) of the specialized ob-
ject logics.