Vitalik: A New Type of High-Level Programming Language Worth Trying Should Make Definitions and Theorems Easier for Humans to Read

Odaily Planet Daily News Vitalik posted on the X platform stating that a new type of "high-level programming language" worth trying would be one that compiles into Lean (or HOL, etc.), with the focus being on making it as easy as possible for humans to read definitions and theorems, rather than proofs. Because as long as the proofs are correct, the key lies in the definitions and theorems themselves. The envisioned use case is that AI outputs a lengthy proof, and readers need to be able to understand, as effortlessly as possible, the precise claims that have actually been proven within those outputs.