Generalizing Types as Provable Invariants

[Waldemar Horwat <address@hidden>]

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?  In essence, I'd like the source code of 
a program to consist of two interweaved parts:

1.  The actual code of the program
2.  Machine-checkable proofs of assertions about the program

Viewed this way, parametrized types are only a slightly more 
sophisticated proof system than monomorphic types.  I'd like to be 
able to write a simple proof that, say, the index of an array access 
will never exceed the dynamic size of the array I'm using.  In 
another case I'd like to write a proof that the insert routine will 
leave my tree sorted if it was sorted before.  I'd also like to be 
able to define new kinds of characteristics (rather than just 
membership in a set or range) that can be manipulated by the 
machine-checkable proofs.  Furthermore, these assertions should be 
easy to communicate and machine-verify across abstraction boundaries 
in the language.

Something like this might be useful in the maintenance of large 
systems.  I find that the hardest part nowadays in developing large 
systems isn't writing the initial code; rather, it is keeping track 
of the assumptions that were made along the way and ensuring (hoping 
in most cases) that modifications respect those assumptions. 
Furthermore, as a system evolves, invariably the invariants 
themselves have to evolve; it would be nice to be able to change what 
the invariant is and have the compiler notify me of all cases/uses I 
forgot to consider.  Having assertions in a language or development 
methodology helps a little, but doesn't provide much design insight 
and only works if the test cases happen to exercise the code well.

     Waldemar