Thesis

Section 3.1 shows Ochre through code examples
Chapter 4 formally specifies Ochre

Repo

https://github.com/charlielidbury/ochre/blob/main/report/thesis/main.pdf

If you clone, you can write Ochre code in compiler/src/main.rs, it will be type checked during Rust compile. Note: only a tiny fraction of Ochre is implemented in that repo.

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.

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

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.