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

Vitalik posted on X platform, stating that a new type of "high-level programming language" worth trying is one that compiles to Lean (or HOL, etc.), with the focus on making definitions and theorems as easy to read as possible for humans. Not the proofs, because proofs just need to be correct; the key lies in the definitions and theorems themselves. The envisioned use case is that AI outputs a large block of proof, and readers need to understand as effortlessly as possible which precise claims are actually being proven in those outputs.