Vitalik: A new type of advanced programming language worth trying should make definitions and theorems easier to read

Odaily Planet Daily reported that Vitalik stated on the X platform that a new type of "advanced programming language" worth trying is one that compiles into Lean (or HOL, etc.), with a focus on making definitions and theorems as easy as possible for humans to read. Rather than proofs, because as long as the proof is correct, the key lies in the definitions and theorems themselves. The envisioned use case is that AI outputs a long proof, and readers need to understand as effortlessly as possible which precise claims in those outputs have actually been proven.