The Babylon Programming Language

Summary

"Babylon" is a new programming language which aims to support formal verification (e.g. preconditions, postconditions and invariants) within the context of a C or Rust like language (e.g. compilation to native code, no garbage collection).

The language is not yet finished and the syntax and semantics are still evolving, so it is not yet recommended for production use, but a GitHub repository is available for those who wish to learn more about the project.

Example

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;
    }

For more examples, check out the examples folder and the interactive chess demo in the GitHub repo.

Current Status

A prototype compiler, written in C, is now available (in the GitHub repo).

The compiler has two modes:

  1. "Compile" mode translates an input Bablyon program into an equivalent C program. This can then be compiled with any standard C compiler.
  2. "Verify" mode takes an input Babylon program and proves that the program satisfies all of its pre/post conditions and invariants, and that it cannot raise certain types of errors (e.g. array index out of bounds, divide by zero, integer overflow) at runtime.
    • This is done by formulating a set of verification conditions and then passing these conditions to external SMT solver tools to be proved. (Currently we use Z3, CVC5 and Vampire, although in principle, anything that supports the SMT-LIB interface could be used.)
    • Note that these "proofs" are only valid if we are willing to trust that the SMT solvers are correct, and that the Babylon compiler itself is free of bugs. Both of these assumptions may be questioned; therefore, while Babylon is a useful tool, it cannot give a 100% guarantee of correctness. (If a higher level of assurance is required, then other tools, such as Coq or Isabelle, may be more suitable.)

The current status of the compiler is that it is working reasonably well (although there are probably still a few minor bugs) and, indeed, I am currently using it to write actual programs (the largest having approximately 17,000 lines of code). However, it is still only a prototype, and the following work is ongoing:

It will therefore probably be a number of years before the project can be considered "finished".

Please note that I can (and most likely will) make backward-incompatible changes in the future, so do not expect programs written in the current version of Babylon to continue working in future versions of the compiler.

Future work

The following provides a little bit more detail on the areas that I intend to work on in the future (in no particular order).

  1. Language changes:
    • Allow "abstract" types, e.g. a module should be able to declare "type Foo;" in the interface, but refine that to "type Foo = some_concrete_type;" in the implementation.
    • Revisit the "allocated" keyword in the language. Perhaps instead add a concept of "copyable" vs. "movable" types (like Rust's "Copy" trait). Perhaps we also need something like C++'s move semantics, or Rust's "borrow checker" (but hopefully in a simplified form!).
    • Reconsider the current design for arrays. Perhaps allow array slices/sections (like in Fortran).
    • Improve C interoperability – some kind of "foreign function interface" should be designed and implemented.
    • Add more "quality of life" features (e.g. "for" loops; inference of generic type arguments).
    • Add support for recursion (both recursive types and recursive functions) – I did always intend to add this, but somehow never got round to it (I haven't needed recursion in my own programs so far).
  2. Tool support:
    • Add a packaging system, similar to cabal for Haskell, or cargo for Rust.
    • Make the compiler more user-friendly, e.g. provide better error messages.
    • Support more SMT solvers (or automated theorem provers more generally).
      • Possibly also include a mode where the verification conditions can be exported to an external proof assistant, like Coq or Isabelle, for manual proving, in case the user either doesn't want to trust SMT solvers, or they have a problem that is too hard for automated proof and they are willing to do the work to prove it manually.
    • Consider providing tools to analyse the time and space usage of a program. E.g. we might want to prove that a program, or a certain part of the program, allocates no more than X bytes of heap or Y bytes of stack space, or carries out no more than Z machine operations (where X, Y, Z might be functions of the input data).
  3. Fully document the language, its standard library, and all available tools.
  4. Compiler implementation:
    • Doing a self-hosted implementation (i.e. implementing the compiler in its own language) might be interesting at some point.
    • Ideally, we would also have some kind of formally verified implementation (a bit like the CompCert project), although this might be a bit too ambitious for the time being!

Related projects

The following is a list of some other programming languages and tools that are usable for software verification.

Disclaimer

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.

Stephen Thompson
Email: stephen (at) solarflare.org.uk
Last updated April 2024