Vitalik: New advanced programming language should make definitions and theorem easier to read

Vitalik stated on platform X that a new type of advanced programming language worth trying is a language that is compiled as Lean or Hol, with a focus on making definitions and theorems easier for humans to read, rather than proof, because the reader needs to understand the precise claims that are proven when the AI output is certified。