Vitalik提議開發面向人類閱讀的Lean編譯語言

BiRun 消息，以太坊創始人 Vitalik Buterin 在 X 平台表示，值得嘗試開發一種新的高級編程語言，該語言可編譯為 Lean 或 HOL 等形式化驗証系統。其覈心目標是讓人類更輕鬆地閱讀定義和定理，而非証明過程，因為証明的正確性由機器保証。該語言的預期應用場景是輔助人類審査 AI 生成的証明代碼塊，降低閱讀門檻。