¡Gracias por la gran pregunta @EliBenSasson!

"¿En qué lenguaje programarán las personas".

Como sabes, los circuitos polinómicos se utilizan para *verificar*. Cairo oculta esta distinción para presentar una particular metáfora de programación al usuario (la Máquina Virtual de Cairo), lo cual está bien, pero muchos paradigmas de programación son posibles y en cualquier caso lo que importa no es lo que se codifica sino lo que se verifica.

Por ejemplo: las funciones pueden especificarse directamente en lógica (de primer orden). La sección 3 del documento muestra cómo, y en particular presenta una selección de funciones, incluyendo funciones recursivas generales, dentro del marco de Gabbay. En el documento tal como está escrito, esta es una definición teórica dirigida a los teóricos, y en consecuencia Gabbay utiliza racionales en lugar de campos finitos, pero está bastante claro que principios similares se aplicarían sobre un campo finito. No es una distinción esencial.

Un caso especial es relevante: está claro en el documento de Gabbay que la validez de los árboles de derivación puede especificarse usando este marco, por ejemplo, la especificación de árboles de derivación para la reducción del combinador SK, lo cual es interesante en sí mismo y porque es paradigmático para muchas otras definiciones similares. Las definiciones inductivas son una base suficiente y conveniente para la programación declarativa. Así que, si queremos presentar una abstracción de programación al usuario, esa es una forma directa y matemáticamente fundamentada para hacerlo, que implica una sobrecarga mínima. Hay otras.

Aunque lo anterior no es en sí mismo una prueba matemática, espero que esto dé una idea de una respuesta a la pregunta.