LEO: un lenguaje de programación para las aplicaciones verificadas de conocimiento cero. Resumen
Los libros mayores descentralizados que soportan aplicaciones complejas sufren tres limitaciones:
- Primero, las aplicaciones son pequeños entornos aprovisionados con tiempo de ejecución limitado, tamaño de stack mínimo y conjunto de instrucciones limitado.
- En segundo lugar, las aplicaciones deben revelar transición de su estado, lo que abre posibilidades de ataques frontales a minerosa los mineros e inestabilidad del consenso.
- En tercer lugar, las aplicaciones ofrecen garantías débiles de validez y seguridad.
En Aleo nosotros diseñamos, implementamos y evaluamos LEO, un nuevo lenguaje de programación diseñado para las aplicaciones formalmente verificadas de conocimiento cero.
LEO ofrece un entorno de ejecución potente que no está restringido en
tiempo de ejecución, tamaño de pila o conjunto de instrucciones.
Además de ofrecer privacidad de aplicaciones y mitigar el valor extraíble minero (MEV), LEO consigue dos caracteristicas fundamentales.
- Primero, las solicitudes son formalmente verificados con respecto a sus especificaciones de alto nivel.
- En segundo lugar, las aplicaciones pueden verificarse concisamente por cualquier persona, independientemente del tamaño de la aplicación.
LEO es el primer lenguaje de programación conocido en introducir un marco de prueba, registro de paquetes,resolución de importación, compilador remoto, lenguaje formalmente definido y verificador de teoremas para propósitos generales, aplicaciones de conocimiento cero.
Texto original (papel blanco de Aleo):
