Ochre

What?

Ochre will be a systems theorem prover, which is the intersection between:

• low-level, systems programming languages like Rust or C and
• theorem provers like Lean or Agda.

The former will be achieved by using Rust’s ownership semantics and borrow checker. The latter will be achieved via the inclusion of dependent types and hopefully some rigor.

Why?

These features would allow programmers to verify properties about their programs without leaving the language they’re writing those programs in. Hopefully this will make verification easier, and therefore increase how much software is formally verified globally.

I see this verification dividing into two categories:

• Proving properties we currently tell the compiler to assume, like removing the need for unsafe code in RefCell and Vec.
• Proving properties we currently don’t get the compiler involved in, like proving a financial exchange never creates nor destroys money, or that a compiler respects its formal specification.

There are already languages which support verification, but they are typically dependently typed pure functional languages which makes writing code harder both in terms of ergonomics, and runtime performance.

There are multi-language stacks which allow verification of high performance software, like the Low* translation of F* to C, but they require the programmer to significantly change how they write their programs (in Low*’s case, this means existing within the Stack monad), instead of writing more “natural” code like safe Rust.

The goal of Ochre is to allow programmers to write in a language very similar to Rust, while having access to the power of a dependent type system.

How?

The exact semantics of Ochre, and therefore the proper answer to how Ochre works are given in my masters thesis (PDF at top of this page), but here is the rough “technique” it uses to type check programs which have both dependent types and mutability:

To illustrate how the above three aspects work together, here is an example of mutation interacting with dependent pairs.

A Taste of Ochre

First, we define a few basic types:

Bool = 'true | 'false;
Letter = 'a | 'b | 'c;

' denotes an atom, which is an arbitrary value, uniquely identified by the tag after the '. When being interpreted as a type like they are in this code snippet, atoms are interpreted as the singleton type consisting of just that atom, then | union’s those singleton types together into the non-singleton types Bool and Letter.

Then we define a dependent pair type, where the right can be either a Bool or a Letter, depending on whether the left is 'true or 'false.

DPair = (tag: Bool, match tag {
  'true => Bool,
  'false => Letter,
});

In the above snippet the left of the pair is a Bool, then the right of the pair is an expression which depends on the value of the left. Namely, its a match statement which returns a different type for the true and false case.

Now we can define a function which mutates one of these dependent pairs:

overwrite = (p: &mut DPair) {
  *p = ('true, 'false);
}

This defines a function overwrite which takes in a mutable reference (a pointer + a proof this pointer is unique) to a DPair as defined earlier.

The body of overwrite may change the type being pointed at, but must leave it as a DPair by the end of the function body.

At the end of the function the type of p is the singleton type &mut ('true, 'false), which can then be widened to &mut DPair, since ('true, 'false) is a subtype of DPair.

Progress

My progress so far has been formally specifying Ochre’s syntax and typing rules as my masters project and implementing the type checker for part of the language. Both of these will need substantial work before they can be used to implement and verify useful software, most glaringly: Ochre, as formally specified, is unsound, will need major rework and the implementation doesn’t generate any code.

Show Me More!

For code examples, formal specification, and some evaluation, see my masters thesis.

WhatsApp groupchat if you’ve got questions, want to help, or just want updates as they come