Re: Generalizing Types as Provable Invariants

[Pixel <address@hidden>]

Waldemar Horwat <waldemar@acm.org> writes:

> A static type system can be thought of as a small framework for proving
> invariants about a program -- in a type-safe language, if a variable is typed
> as an integer then I know that I can't get a string out of it.  The compiler
> knows it too and doesn't let me modify the program to violate that assumption.
> 
> How much work has been done on generalizing the notion of a static type system
> into a more complete framework for proving interesting invariants about a
> program?

various examples of static checks:
- keeping track of exceptions (Java)
- const'ness (C++)
- more generally: A Theory of Type Qualifiers
  http://citeseer.nj.nec.com/foster99theory.html

extended type systems
- dependent types (cf recent thread on comp.lang.functional)
   Cayenne http://www.math.chalmers.se/~augustss/cayenne
   DML & DeCaml http://www.ececs.uc.edu/~hwxi/DML/DML.html
   Delphin http://cs-www.cs.yale.edu/homes/carsten/delphin
- type checked macros using staged evaluation
   MetaOcaml http://cs-www.cs.yale.edu/homes/taha/MetaOCaml/
   (if I understood)
- maybe DrSpidey (and MrFlow) ?

full proof checkers
- method B http://archive.comlab.ox.ac.uk/formal-methods/ b.html
  (programming language, quite heavy and not decidable)
- theorem proovers
   Coq http://coq.inria.fr
   (i don't really know what it is)
- many more things at http://archive.comlab.ox.ac.uk/formal-methods
  (but once again, i don't really know what it is)