From owner-qed Wed Aug 10 10:07:56 1994
Received: from localhost (listserv@localhost) by antares.mcs.anl.gov (8.6.4/8.6.4) id KAA29576 for qed-out; Wed, 10 Aug 1994 10:00:51 -0500
Received: from life.ai.mit.edu (life.ai.mit.edu [128.52.32.80]) by antares.mcs.anl.gov (8.6.4/8.6.4) with SMTP id KAA29569 for <qed@mcs.anl.gov>; Wed, 10 Aug 1994 10:00:36 -0500
Received: from spock (spock.ai.mit.edu) by life.ai.mit.edu (4.1/AI-4.10) for qed@mcs.anl.gov id AA22393; Wed, 10 Aug 94 11:00:33 EDT
From: dam@ai.mit.edu (David McAllester)
Received: by spock (4.1/AI-4.10) id AA12556; Wed, 10 Aug 94 11:00:31 EDT
Date: Wed, 10 Aug 94 11:00:31 EDT
Message-Id: <9408101500.AA12556@spock>
To: Zdzislaw.Meglicki@cisr.anu.edu.au
Cc: qed@mcs.anl.gov
In-Reply-To: Zdzislaw Meglicki's message of Wed, 10 Aug 1994 10:28:30 +1000 (EST) <0iG1wi2KmlE508BWc0@earth>
Subject: Types Considered Harmful
Sender: owner-qed@mcs.anl.gov
Precedence: bulk

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.

	David