Vitalik: New types of advanced programming languages worth trying should make it easier for people to read definitions and theorems.

Odaily reported that Vitalik posted on platform X, stating that a new type of "advanced programming language" worth trying is a language that compiles to Lean (or HOL, etc.), focusing on making definitions and theorems as human-readable as possible. Instead of proofs—since proofs only need to be correct—the key lies in the definitions and theorems themselves. The envisioned use case is for AI to output a large block of proofs, while readers should be able to easily understand exactly which precise claims have actually been proven in these outputs.