Thesis

Slides

GitHub

Ochre is a (work in progress) language which aims to use a new architecture:

<aside> đź’ˇ

Instead of runtime code being expressed in a different language than types, Ochre expresses both in the same language, where types are just a special case of programs where the program has “ambiguity”.

</aside>

In this paradigm, mutability and dependent types are compatible, allowing for a high performance system prover.

What?

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

  1. low-level, systems programming languages like Rust or C and
  2. 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.

<aside> <img src="/icons/info-alternate_gray.svg" alt="/icons/info-alternate_gray.svg" width="40px" /> More or less, Ochre = Rust + Dependent Types.

</aside>

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:

  1. Proving properties we currently tell the compiler to assume, like removing the need for unsafe code in RefCell and Vec.
  2. 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.