[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: Generalizing Types as Provable Invariants
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.
At 01 Jun 2002 01:17:31 +0200, Pixel wrote:
> Waldemar Horwat <firstname.lastname@example.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
> 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)