Vitalik: Una nueva generación de lenguajes de programación avanzados debería facilitar la lectura de definiciones y teoremas

Odaily informó que Vitalik publicó en X que un nuevo tipo de "lenguaje de programación avanzado" que vale la pena probar es un lenguaje que compile a Lean (o HOL, entre otros), poniendo el énfasis en hacer que las definiciones y teoremas sean lo más fáciles posible de leer para los humanos. No en las demostraciones, porque lo importante de las demostraciones es que sean correctas; la clave está en las definiciones y los teoremas en sí. La idea es que la IA genere pruebas extensas y que el lector pueda comprender fácilmente qué afirmaciones precisas han sido realmente probadas en esos resultados.