비탈릭: 시도해볼 가치가 있는 새로운 고급 프로그래밍 언어는 정의와 정리를 더 쉽게 읽을 수 있게 해야 한다

Vitalik은 X 플랫폼에 글을 올리며, 시도해볼 가치가 있는 새로운 "고급 프로그래밍 언어"는 Lean(또는 HOL 등)으로 컴파일되는 언어라고 밝혔습니다. 이 언어는 가능한 한 인간이 정의와 정리를 쉽게 읽을 수 있도록 하는 데 중점을 두고 있습니다. 증명은 단지 올바르기만 하면 되기 때문에, 핵심은 정의와 정리 자체에 있습니다. 이 언어의 구상된 용도는 AI가 대량의 증명을 출력하고, 독자가 이러한 출력에서 실제로 어떤 정확한 주장이 증명되었는지를 가능한 한 쉽게 이해할 수 있도록 하는 것입니다.