Charlie Lidbury

Thesis, Slides, GitHub

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 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:

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

How?

Ochre needs to be easy to use, so people actually use it, and formal enough that people trust the results of its analysis.

<aside> <img src="/icons/info-alternate_gray.svg" alt="/icons/info-alternate_gray.svg" width="40px" /> I am using Rust as my benchmark for “easy to use”: if a program can be written in Rust, it should be about as easy to write in Ochre.

</aside>

Broadly speaking, Ochre achieves its ergonomics by using ownership to make dependent types compatible with mutability. Other tools avoid addressing this incompatibility through a variety of architectures, such as:

Expressing mutation through a pure abstractions like monads (Low*)
Removing the mutation via a translation step (Aeneas)
Reasoning about the effects of mutation totally outside of the type system (Separation logic based approaches?).