BitC
Encyclopedia
BitC is a systems programming language developed by researchers at the Johns Hopkins University
and The EROS Group, LLC as part of the Coyotos
project. It aims to support formal program verification.
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.
languages like ML and Haskell
with the close hardware interaction of low-level programming language
s 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.
From the standpoint of programming language evolution, BitC's most important innovation is the first sound and complete type inference algorithm that handles generalized state and unboxing. With the recent (not yet implemented) addition of effect typing, BitC presents an interesting middle position between purely functional
and traditionally state-oriented languages.
From the perspective of systems programmers, BitC may be more interesting for the fact that the non-optimizing research prototype compiler is delivering performance on early benchmarks that falls within 1% to 1.5% of C on comparable code.
- announced that he had accepted a position at Microsoft
to work on the Midori
project, and that after August 2009 he would not be working further on BitC. However, in March 2010 he announced that he would leave Microsoft and continue to work on BitC.
Johns Hopkins University
The Johns Hopkins University, commonly referred to as Johns Hopkins, JHU, or simply Hopkins, is a private research university based in Baltimore, Maryland, United States...
and The EROS Group, LLC as part of the Coyotos
Coyotos
Coyotos is a capability-based security-focused microkernel operating system developed by The EROS Group, LLC. It is a successor to the EROS system that was created at the University of Pennsylvania and Johns Hopkins University.- History :...
project. It aims to support formal program verification.
Objectives
The language has two primary objectives:- To merge the advances of modern programming languages; sound type systems with abstraction, sound and complete type inferenceType inferenceType inference refers to the automatic deduction of the type of an expression in a programming language. If some, but not all, type annotations are already present it is referred to as type reconstruction....
, let-polymorphism, and mathematically grounded semantics — with the requirements of systems programming; first-class treatment of state, support for prescriptive low-level representation, explicitly unboxed types, and performance comparable to C. - To support formal program verification of low-level systems programs, such as kernels/microkernelMicrokernelIn computer science, a microkernel is the near-minimum amount of software that can provide the mechanisms needed to implement an operating system . These mechanisms include low-level address space management, thread management, and inter-process communication...
s.
History
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.
Language innovations
BitC combines the concepts of higher-order functional programmingFunctional programming
In computer science, functional programming is a programming paradigm that treats computation as the evaluation of mathematical functions and avoids state and mutable data. It emphasizes the application of functions, in contrast to the imperative programming style, which emphasizes changes in state...
languages like ML and Haskell
Haskell (programming language)
Haskell is a standardized, general-purpose purely functional programming language, with non-strict semantics and strong static typing. It is named after logician Haskell Curry. In Haskell, "a function is a first-class citizen" of the programming language. As a functional programming language, the...
with the close hardware interaction of low-level programming language
Low-level programming language
In computer science, a low-level programming language is a programming language that provides little or no abstraction from a computer's instruction set architecture. Generally this refers to either machine code or assembly language...
s like C
C (programming language)
C is a general-purpose computer programming language developed between 1969 and 1973 by Dennis Ritchie at the Bell Telephone Laboratories for use with the Unix operating system....
. The current language syntax is derived from the syntax of Lisp
Lisp programming language
Lisp is a family of computer programming languages with a long history and a distinctive, fully parenthesized syntax. Originally specified in 1958, Lisp is the second-oldest high-level programming language in widespread use today; only Fortran is older...
, but this is expected to be replaced as the language comes to its first release.
From the standpoint of programming language evolution, BitC's most important innovation is the first sound and complete type inference algorithm that handles generalized state and unboxing. With the recent (not yet implemented) addition of effect typing, BitC presents an interesting middle position between purely functional
Purely functional
Purely functional is a term in computing used to describe algorithms, data structures or programming languages that exclude destructive modifications...
and traditionally state-oriented languages.
From the perspective of systems programmers, BitC may be more interesting for the fact that the non-optimizing research prototype compiler is delivering performance on early benchmarks that falls within 1% to 1.5% of C on comparable code.
Status
In April 2009, Shapiro - driving force behind both BitC and CoyotosCoyotos
Coyotos is a capability-based security-focused microkernel operating system developed by The EROS Group, LLC. It is a successor to the EROS system that was created at the University of Pennsylvania and Johns Hopkins University.- History :...
- announced that he had accepted a position at Microsoft
Microsoft
Microsoft Corporation is an American public multinational corporation headquartered in Redmond, Washington, USA that develops, manufactures, licenses, and supports a wide range of products and services predominantly related to computing through its various product divisions...
to work on the Midori
Midori (operating system)
Midori is the code name for a managed code operating system being developed by Microsoft Research. It has been reported to be a possible commercial implementation of the Singularity operating system, a research project started in 2003 to build a highly-dependable operating system in which the...
project, and that after August 2009 he would not be working further on BitC. However, in March 2010 he announced that he would leave Microsoft and continue to work on BitC.
External links
- BitC homepage
- BitC Language Specification (html, pdf)
- BitC-dev mailing list archives
- Coyotos homepage
- Jonathan Shapiro's homepage