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

Vitalik posted on the X platform stating that a new type of "high-level programming language" worth trying is a language compiled to Lean (or HOL, etc.), focusing on making it as easy as possible for humans to read definitions and theorems. Rather than proofs, because proofs only need to be correct, the key lies in the definitions and theorems themselves. The envisioned use is that AI outputs a large segment of proof, and the reader needs to understand as easily as possible which precise claims have actually been proven in these outputs.