There's a lot of interesting work in liquid types [1] which may be applicable to BitC. They've gone quite far in verifying practically unannotated C programs with liquid type inference, for instance (including inferring concurrent safety). The work on liquid types for Haskell is even further along and still being actively developed.
The core approach is consists of basically extending the simple types with refinement predicates that are checked by an external SMT solver. This approach dovetails nicely with Jonathan's desire for programmers to only specify partial specifications where necessary, and having more complicate properties solved via refinements. Sandro [1] http://goto.ucsd.edu/~rjhala/liquid/haskell/blog/about/ _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
