Very nice discussion there. It surprises me that a non-trivial piece of code written in C can be verified. It might be of interest that BitC http://www.bitc-la

Very nice discussion there. It surprises me that a non-trivial piece of code written in C can be verified. It might be of interest that BitC http://www.bitc-lang.org/ http://www.bitc-lang.org/ is being developed as a flexible system programming language that supports verification. It seeks to combine the flexibility, safety, and richness of Standard ML or Haskell with the low-level expressiveness of C.... ...it is possible to write a MPEG decoder or SHA-1 hash algorithm in BitC that is fully safe, but performs competatively with the C implementation. Today, that can't be done in SML, O'Caml, or Haskell.