Спасибо за замечательный вопрос @EliBenSasson!
"В каком языке люди будут программировать".

Как вы знаете, полиномные схемы используются для *проверки*. Cairo скрывает эту разницу, чтобы представить пользователю одну конкретную программную метафору (Cairo VM), что нормально, но многие парадигмы программирования возможны и в любом случае важно не то, что кодируется, а то, что проверяется.

Например: функции можно указать непосредственно в (первостепенной) логике. Раздел 3 статьи показывает как это сделать, и в частности представляет выбор функций, включая общие рекурсивные функции, в рамках Gabbay. В статье, как написано, это теоретическое определение, направленное на теоретиков, и соответственно Gabbay использует рациональные числа вместо конечных полей — но ясно, что аналогичные принципы будут применимы над конечным полем. Это не существенная разница.

Одним специальным случаем является то, что из работы Gabbay ясно, что допустимость дерева вывода может быть указана с помощью этой рамки — например, спецификация деревьев вывода для SK комбинирующего сокращения, что интересно само по себе и потому, что является примером для многих других подобных определений. Индукционные определения являются достаточной и удобной основой для декларативного программирования. Так что если мы хотим представить пользователю программную абстракцию, это один прямой, математически обоснованный способ сделать это, который включает минимальный накладной расход. Есть и другие.

Хотя вышесказанное само по себе не является математическим доказательством, я надеюсь, что это дает представление о ответе на поставленный вопрос.