Re: Generalizing Types as Provable Invariants

[Matthias Felleisen <address@hidden>]

Pixel, if a language isn't safe, a type system is only half as helpful. 
Think of C++. If it verifies x is a char, then at run-time it may still
throw in some bits from an int into x, and what do you know -- is it
an int then? No, but it will print as one. 

Is adding more stuff to such type systems truly useful? Be more selective. 

-- Matthias




At 01 Jun 2002 01:17:31 +0200, Pixel wrote:
> 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)