as happy as I am with the explosion of formal verification, we’re immediately running into the classic problem: writing down what the program is supposed to do
proving your program “correct” only works if you know exactly what “correct” means!!
proving your program “correct” only works if you know exactly what “correct” means!!
@rajashree Up to the quality of the specs. Not the same thing.
13
17
189
13,228
@tritlo The theorem of correctness for a program is currently larger than the program itself. Hopefully the underlying tech improves (e.g. with automated tactics everyone understands) to the point where correctness statements are just 2-3x today's type signatures.
7
3
36
3,735
@TimSweeneyEpic @tritlo I depends on what you mean by "program". Syntax is fungible. How about a structure that starts with Wadler's "types are proofs" and node level obligations fall out of the graph 'for free'? arxiv.org/abs/2603.25414
Oct 24, 2026 · 9:18 AM UTC
0
0
0
48