''BitC is a SystemProgramming language that combines the "low-level" nature of C with the semantic rigor of Scheme or ML. BitC was designed by careful selection and exclusion of language features in order to support proving properties (up to and including total correctness) of critical systems programs.''

Intended to be used to implement CoyotOs.  Although named after C, source code is composed of EssExpression''''''s like Scheme, sprinkled with type declarations to feed the TypeInference engine and other SyntacticSugar.  BitC source is compiled to CeeLanguage. 
* ''Note that the s-expression syntax will be abandoned at some point before the language is officially released. It's only a placeholder syntax while they refine the semantics.''
** The developers of Lisp said the same thing...

Draft specification:
* http://www.bitc-lang.org/docs/bitc/spec.html

See also VerifiedDesignByContract.

----
CategoryProgrammingLanguage