How Osprey checks a proof: for programmers
Follow a statement and its evidence through the proof kernel written in Osprey.
For programmers. Choose the other audience version or browse the complete series.
Lean is the development oracle for compatible proofs; Osprey checks them independently. Known unsound reference behaviour must be refused, and changing a discipline requires fresh proof validation.
What this demonstrates
The kernel infers a proof term's type and compares it with the claimed statement. The recorded runs show both acceptance and deliberate rejection. This is a check of the supplied statement and proof, not automatic verification of an entire application.
Read the guide and try it yourself. Osprey is actively evolving; the guide distinguishes the recorded demonstration from current corpus progress.
Actual source
Continue learning
Use the Workbench · Current Mathlib port evidence · All twelve films
Transcript
- A proof checker is a program that checks whether a piece of evidence establishes the claim attached to it. Osprey is a functional programming language, and this checker is written in Osprey. Let us follow one small proof from its statement to the result.
- The checker turns a proof into a structured value. A sort describes a kind of type. A variable points to an input. A function waits for an argument. Application supplies one. The checker compares these structures instead of trusting the printed theorem.
- To check a proof, Osprey first infers what type the proof term has. Then it simplifies expressions that compute to the same form. Finally it compares the result with the stated claim. A mismatch becomes an error value, not a crash.
- You do not have to build every proof term by hand. This surface syntax lets you write a theorem in a few lines. Osprey parses it into the kernel's representation. Identity and chained implications are checked examples. A deliberately wrong theorem is refused.
- Here is the same example running. The valid identity proof is accepted. The wrong proof is rejected with the kernel's reason. Both lines come from the executable. Reproducing that pair is more useful than seeing a single success message.
- Osprey keeps ordinary inferred code separate from proof checking. Its pluggable discipline protocol lets a project choose a checker. An existing example checks numeric bounds; the dependent-proof kernel lives outside the compiler too. Here it checks a universal arithmetic theorem. Safe theory forks and fresh checking of dependent proofs remain explicit completion milestones.