Лиспоподобный языкдля системных задач, был разработан для написания на нём верифицированных ядер операционных систем.

> -- Цитата:
> BitC is a new systems programming language. It seeks to combine the flexibility, safety, and richness of Standard ML or Haskell with the low-level expressiveness of C.
> -- Цитата:
> As a litmus test, 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.

Автор языка -- Jonathan Shapiro, год назад уходя из своего универа в Майкрософт, собирался забросить BitC, но сейчас собрался вернуться и с новыми силами взяться за этот язык.