Types Considered Harmful

David McAllester (dam@ai.mit.edu)
Wed, 10 Aug 94 11:00:31 EDT

I think types in verfication systems are much more significant than
they are in programmiing languages. The main obstacle to machine
verification is machine stupidity --- the nasty level of detail of
mechanically verifiable correctness proofs and the difficulty of
constructing these proofs. I once counted lines in the CLINC short
stack verification and determined that in that case verified code
required about an order of magnitude more lines of formal notation
(code) than unverified code.

One can at least argue that types reduce the difficulty of machine
verification by providing guidance to the automated verifier --- proof
obligations generated by type checking can be verified in certain
stereotypical ways, or with well defined algorithms. The more of the
automated inference that one can move into the type system the greater
the level of automation in the verification overall. PVS has been
particularly aggressive in pursuing this philosophy.

In short, one can argue that there are very concrete pragmatic issues
surrounding the choice of a type formalism in a verification systems.