Page loading
Skip to main content

Proofs about programs

An interactive tutorial

The halting problem be damned — we can prove all kinds of things about programs, and we can even check those proofs with computers! In this chapter, we’ll use a language called Lean to prove whether the famous Ackermann function always halts. Along the way, we’ll introduce Noetherian induction and formal systems.

Quoted text:

Your feedback will be sent privately to the author. They may reply to you by email. Thanks for helping make this course better!