Vitalik: Neue fortschrittliche Programmiersprachen, die es wert sind, ausprobiert zu werden, sollten Definitionen und Theoreme leichter lesbar machen.

Odaily berichtete, dass Vitalik auf der Plattform X erklärte, eine neue und empfehlenswerte Art von „fortschrittlicher Programmiersprache“ sei eine Sprache, die nach Lean (oder HOL usw.) kompiliert wird und den Schwerpunkt darauf legt, Definitionen und Theoreme für Menschen so leicht lesbar wie möglich zu machen. Der Fokus liegt nicht auf den Beweisen selbst, denn diese müssen lediglich korrekt sein; entscheidend sind die Definitionen und Theoreme. Der vorgesehene Anwendungsfall ist, dass eine KI einen langen Beweis liefert und der Leser möglichst einfach nachvollziehen kann, welche konkreten Aussagen darin tatsächlich bewiesen wurden.