Table of Contents

Masters Interim Report

Introduction

Ochre will be a programming language which is both

1. a theorem prover and
2. a low-level systems language.

<aside> 💡 More or less, Ochre = Rust + Dependent Types.

</aside>

I hereby dub this type of programming language, a systems theorem prover (systems language + theorem prover).

Repo for the project:

https://github.com/charlielidbury/ochre

The Vision

Software for which Rust is a good fit for, could instead be written in Ochre without much overhead.

Then, theorem proving could be used to:

1. remove the need for unsafe code and
2. prove arbitrary properties about your programs.