Vitalik Buterin propone un linguaggio per prove AI leggibili

Punti chiave

Vitalik Buterin ha proposto un linguaggio di programmazione che compilerebbe direttamente in Lean o HOL per definizioni di prova e teoremi leggibili dagli esseri umani. Buterin ha sostenuto che gli elementi interni delle prove devono solo essere corretti dal punto di vista matematico, mentre definizioni e teoremi devono mostrare che cosa il software garantisce effettivamente. I ricercatori di Ethereum usano già Lean per verificare codice crittografico e logica di consenso, e non esiste ancora alcun prototipo del nuovo linguaggio.