Vitalik: 새로운 고급 프로그래밍 언어는 정의와 정리를 더 쉽게 읽을 수 있게 해야 한다

Odaily의 보도에 따르면, Vitalik은 X 플랫폼에 글을 올려 "시도해 볼 가치가 있는 새로운 '고급 프로그래밍 언어'는 Lean(또는 HOL 등)으로 컴파일되는 언어로, 인간이 정의와 정리를 최대한 쉽게 읽을 수 있도록 초점을 맞춰야 한다"고 말했습니다. 증명은 정확하기만 하면 되고, 핵심은 정의와 정리 그 자체에 있습니다. 그의 구상에 따르면, AI가 긴 증명을 출력하고 독자는 그 출력에서 실제로 증명된 정확한 주장이 무엇인지 최대한 쉽게 이해할 수 있어야 합니다.