BitC

BitC was a partially designed and implemented systems programming language developed by researchers at the Johns Hopkins University and The EROS Group, LLC as part of the Coyotos project. It aimed to support formal program verification. The primary designer of BitC stopped working on the language in 2012 claiming it had fundamental design flaws.

The language has two primary objectives:

The goals for the BitC language were set out in 2004 in Towards a Verified, General-Purpose Operating System Kernel (html, pdf) presented at the 2004 NICTA OS Verification Workshop.

Some details of the origins and early evolution of the language can be found in The Origins of the BitC Programming Language (html, pdf). An early compiler for BitC, known as BitCC, was first released in an alpha form (v. 0.10.1) on June 17, 2006, and in the same year Shapiro left Johns Hopkins to form The EROS Group, LLC, and the BitC project became a joint effort between the two organizations.

At the end of 2008 the specification for the first released version of the language and its compiler converged towards its final form, and the prototype compiler was demonstrated to have favorable performance on microbenchmarks.

BitC combines the concepts of higher-order functional programming languages like ML and Haskell with the close hardware interaction of low-level programming languages like C. The current language syntax is derived from the syntax of Lisp, but this is expected to be replaced as the language comes to its first release.