"Babylon" is a new programming language that I am currently working on. The language will be similar in style to C or Rust (e.g. compiling to native code, no garbage collection), but with support for formal verification (e.g. preconditions, postconditions, invariants), using SMT solvers to do the proofs.
The language is currently in development and it is not ready for production use yet. However, a prototype compiler, together with some examples/demos, are available for those who want to take a "sneak peek". This can be found in the project's GitHub repository.
The following shows an example program written in the Babylon language.
module Prime
interface {
// Define what is meant by a prime number.
ghost function is_prime(n: i32): bool
{
return n >= 2 &&
forall (i: i32) 2 <= i < n ==> n % i != 0;
}
// Declare a function which will check whether a number is prime.
function check_if_prime(n: i32): bool
ensures return <==> is_prime(n);
}
// The implementation of the "check_is_prime" function.
function check_if_prime(n: i32): bool
ensures return <==> is_prime(n);
{
if n < 2 {
return false;
}
var i: i32 = 2;
while i < n
invariant 2 <= i <= n;
invariant forall (j: i32) 2 <= j < i ==> n % j != 0;
decreases ~i;
{
if n % i == 0 {
return false;
}
i = i + 1;
}
return true;
}
A prototype compiler, written in C, is now available. It can be downloaded from GitHub.
In "verify" mode, the compiler will verify that the program satisfies various properties, including:
The verifier works by formulating a number of "verification conditions" (essentially, first-order logic problems) and then passing these to a set of SMT solvers (currently Z3, CVC5 and Vampire) to see if the conditions are provable. If at least one solver reports success ("unsat" result), then the condition is accepted as verified. If this is true of every condition in the program, then verification succeeds.
In "compile" mode, the compiler will translate each Babylon module into an equivalent C source file. A separate C compiler can then be used to produce a final executable. (A previous version of the compiler produced assembly code directly, but that was removed as it was deemed too complicated.)
The Babylon language itself is now in a reasonably "working" state, and one can write moderately large programs in it, but it is still far from "complete". I am still tinkering with the definition of the language and adding new features. Future versions will most likely not be backwards compatible with the current version, so for that reason, I do not recommend people to start using this language for "serious" work just yet. However, people are still very welcome to download the compiler, try it out, and let me know what they think, if they wish to do so.
The GitHub repo contains a number of examples (including a simple interactive chess game) for those who want to see what the language is capable of.
Here is a list of future changes I would like to make, in no particular order.
The ultimate goal would be to get the language to a point where it no longer a prototype, but a usable system. Currently however I expect it to be quite some time before we reach that point.
The SPARK programming language seems to have very similar goals to those of Babylon. SPARK is a version of the Ada programming language, augmented with features for pre and post conditions, assertions and so on. SMT solvers are used for the proofs, and compilation is to native code.
SPARK does look very interesting (even if the Ada syntax is a little off-putting, to me at least); I intend to have a closer look at it in the future.
Dafny is Microsoft's verification-aware programming language. It is similar to Babylon in that it is an imperative-style language with pre and post conditions (indeed Babylon was very much inspired by Dafny). The main difference is that Dafny targets the .NET runtime, whereas Babylon is about verifying C-like native code (e.g. Babylon does not have garbage collection).
VCC is a Microsoft tool that apparently can verify concurrent C programs, with the proofs being done by SMT solvers. I believe, however, that it is no longer maintained.
Frama-C is a framework for verifying C code. The user writes a normal C program, adding pre and post conditions (and the like) in specially formatted comments, and the tool then checks the program for correctness (using SMT solvers).
Frama-C is interesting, but it seems complicated to use (there are many different plugins and options), and there are also concerns that its verifier may be "under-powered" – see e.g. this blog post in which the author complains that Frama-C is unable to verify a relatively simple function. (I tried that author's example in the latest version of Frama-C – it still appears to time out, unless I was doing something wrong – and in Babylon – where it passed easily, so I am not sure what is going on there.)
The Eiffel programming language supports pre and post conditions. It is quite object oriented; classes feature heavily. There is also a tool called AutoProof which can verify the programs (using SMT solvers). There is an interactive demo which is quite fun.
It is apparently possible to generate executable Ocaml code from Isabelle, therefore, one could use Isabelle as a verified programming language, in some sense. However, this would generate code that runs in a garbage-collected environment, not the native C-like code that I am interested in.
Apparently there is a plugin for Coq that can be used to generate C code from a set of Coq definitions. This is certainly interesting if one wants to write (verified) code in a "functional programming" style, and then convert it to lower-level C.
Note that both Isabelle and Coq are full theorem-proving frameworks, therefore they offer stronger guarantees of correctness than SMT solver based systems.
For the avoidance of doubt: the Babylon compiler is currently considered an experimental prototype, not a fully working system. It is provided WITHOUT WARRANTY OF ANY KIND.