Obrigado pela ótima pergunta @EliBenSasson!

"Em qual linguagem as pessoas irão programar?"

Como você sabe, circuitos polinomiais são usados para *verificar*. Cairo obscurece essa distinção para apresentar uma particular metáfora de programação ao usuário (a VM Cairo), o que é bom, mas muitos paradigmas de programação são possíveis e, em qualquer caso, o que importa não é o que é codificado, mas o que é verificado.

Por exemplo, funções podem ser especificadas diretamente em lógica (de primeira ordem). A seção 3 do artigo mostra como, e em particular apresenta uma seleção de funções, incluindo funções recursivas gerais, dentro da estrutura de Gabbay. No artigo como escrito, esta é uma definição teórica voltada para teóricos, e, de acordo, Gabbay usa racionals em vez de campos finitos - mas é bastante claro que princípios similares se aplicariam sobre um campo finito. Não é uma distinção essencial.

Um caso especial é relevante: é claro no artigo de Gabbay que a validade de árvores de derivação pode ser especificada usando esta estrutura - por exemplo, a especificação de árvores de derivação para redução do combinador SK, que é interessante em si mesmo e porque é paradigmático para muitas outras definições. Definições indutivas são uma base suficiente e conveniente para programação declarativa. Então, se quisermos apresentar uma abstração de programação para o usuário, essa é uma maneira direta e matematicamente fundamentada para fazer isso, que envolve um overhead mínimo. Existem outras.

Embora o acima não seja em si uma prova matemática, espero que isso dê uma ideia de uma resposta à pergunta.