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
EssExpressions 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:
See also
VerifiedDesignByContract.
CategoryProgrammingLanguage