Vitalik Says New Programming Languages Should Prioritize Readable Definitions and Theorems

Vitalik said on X that a new type of advanced programming language worth trying is one that compiles to Lean or HOL. According to Odaily, he said the focus should be on making definitions and theorems as easy for humans to read as possible, rather than the proofs themselves. He said the idea is for AI to produce long proofs while readers can more easily understand the exact claims those proofs establish.