謝謝你的好問題 @EliBenSasson！
「大家會用哪種語言來編程？」

你知道的，多項式電路用來 *驗證*。Cairo 模糊了這個區別，以便向用戶展示一個特定的編程比喻（Cairo VM），這樣做不錯，但是許多編程範式都是可能的，無論如何重要的不是編碼的內容，而是驗證的內容。

例如：函數可以直接在（一階）邏輯中指定。論文第 3 節展示了如何做，特別是它在 Gabbay 的框架內展示了一個選擇的函數，包括一般遞歸函數。在論文中這是一個理論定義，旨在理論家，因此 Gabbay 使用有理數而不是有限域——但是很明顯，類似的原則在有限域上也適用。這不是一個重要的區別。

一個特別的例子是相關的：根據 Gabbay 的論文很明顯，可以使用這個框架來指定推導樹的有效性——例如 SK 組合簡化的推導樹的規範，這本身就很有趣，因為它是許多其他這樣的定義的範例。遞歸定義是宣告式編程的足夠且便捷的基礎。所以如果我們想向用戶展示一個編程抽象，這是一種直接的、數學原理的方法，涉及最小的開銷。還有其他方法。

雖然上述本身不是一個數學證明，但我希望這能給出對這個問題的一個味道。