Dear Agent: Prove it. • Rijnard van Tonder

rijnard.com · 2,109 words · saved by 1 readers

Count the number of r's in strawberry. Actually no, prove it instead. Why tests won't save us and how formal verification becomes essential when agents write our code.

Dear Agent: Prove it. Count the number of r's in strawberry. Actually no, prove it instead. At some point it became possible to write the following prompt, and any frontier LLM will give you a correct answer. > Write a Lean program that counts the number of times a character occurs in a string. Prove it's correct. You'll get a program like this, or some variation of it. We'll walk through it in just a minute. /-- Count occurrences of a character in a list. -/ def countCharList (c : Char ) : List Char → Nat | [] => 0 | x :: xs => ( if x = c then 1 else 0 ) + countCharList c xs /-- Count occurre

Dear Agent: Prove it. • Rijnard van Tonder

related reading