Vitalik: New advanced programming languages worth trying should make definitions and theorems easier to read

Odaily Planet Daily News Vitalik posted on the X platform, stating that a new type of "high-level programming language" worth trying is one that compiles into Lean (or HOL, etc.), with the focus being on making definitions and theorems as easy as possible for humans to read. Not the proofs, because as long as the proofs are correct, that is sufficient; the key lies in the definitions and theorems themselves. Its envisioned use case is that AI outputs a long proof, and the reader needs to understand as effortlessly as possible the precise claims that have actually been proven in these outputs.