Hello!

Thesis, Slides, GitHub

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 stealing 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 more frictionless, and therefore increase how much software is formally verified.

I see this verification naturally 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 compiler respects a formal specification, or that an exchange doesn’t loose or hallucinate any assets.

How?

Ochre uses a new paradigm of type system. Instead of types and terms being distinct concepts, there is only the concept of a program. Programs can be imprecise and approximate other programs. In this paradigm, mutability and dependent types are naturally compatible.

A program is something which can be executed into a result. For example 1 is a program which evaluates into a 1, and 1 + 1 is a program which evaluates into a 2.

An approximate program is a program which could execute into any one of a set of results. For example 1 | 2 is a program which could evaluate to either a 1 or a 2, and 1 + (2 | 3) is a program which could evaluate to either a 3 or a 4. Approximate programs are only used to reason about what other programs will do when they are executed, and are never left in the compiled binary (Ochre uses a deterministic execution model).

Exact programs and approximate programs come into contact with each other via the : operator, which is responsible for checking that one program is an approximation of another, and instructing the compiler to loose information.

The program A : B