感谢你的好问题 @EliBenSasson！
“人们将用哪种语言编程？”

如你所知，多项式电路用于 *验证*。Cairo模糊了这一区别，以向用户呈现一种特定的编程隐喻（Cairo虚拟机），这是可以接受的，但是许多编程范式都是可能的，无论如何，重要的不是代码是什么，而是验证的是什么。

例如：函数可以直接在（一阶）逻辑中指定。论文第3节展示了如何，特别是它在Gabbay的框架内展示了一些函数的选择，包括一般递归函数。在论文中，这是一个旨在理论家的理论定义，因此Gabbay使用有理数而不是有限域——但是很明显，类似的原则在有限域上也适用。这不是一个重要的区别。

一个特殊的情况是相关的：从Gabbay的论文中很明显，可以使用这个框架来指定推导树的有效性——例如，用于SK组合减少的推导树的规范，这本身就很有趣，因为它是许多其他这样的定义的范例。归纳定义是一个充分且便捷的宣告式编程基础。因此，如果我们确实想向用户呈现一个编程抽象，这是一种直接的、数学原理的方法，涉及最小的开销。还有其他方式。

虽然上述内容本身并不是数学证明，但我希望这能给出对问题的一个答案的概念。