Vitalik谈编程语言新趋势：让定义和定理更易读是关键

币界网消息，Vitalik在X平台表示，一种值得尝试的新型高级编程语言是编译为Lean或Hol等的语言，重点是让人类更容易阅读定义和定理，而非证明，因为AI输出证明时，读者需要轻松理解其中被证明的精确主张。