素晴らしい質問をありがとうございます @EliBenSasson!
「人々はどの言語でプログラミングするのか」という問い。

多項式回路は検証に使用されます。Cairoは、ユーザーに特定のプログラミングのメタファー（Cairo VM）を提示するためにこの区別を曖昧にしていますが、多くのプログラミングパラダイムが可能であり、いずれにせよ重要なのは、何がコード化されるかではなく、何が検証されるかということです。

例えば：関数は（第一順序）論理で直接指定できます。論文のセクション3は、それがどのように行われるかを示しており、特にGabbayのフレームワーク内で一般再帰関数を含む関数の選択を提示しています。この論文では、理論家向けの理論的定義として書かれており、それに応じてGabbayは有限体ではなく有理数を使用していますが、同様の原則が有限体上で適用されることは明らかです。これは本質的な区別ではありません。

一つの特殊なケースは関連しています：Gabbayの論文から明らかなように、このフレームワークを使用して導出木の妥当性を指定できます。例えば、SK コンビネーターの還元の導出木の仕様は、それ自体が興味深く、他の多くの定義のパラダイマティックなものです。帰納的定義は宣言的プログラミングの十分かつ便利な基盤です。したがって、ユーザーにプログラミングの抽象化を提示したい場合、これは数学的に原則に基づいた、最小のオーバーヘッドを伴う簡単な方法です。他にも方法があります。

上記はそれ自体数学的証明ではありませんが、この質問に対する回答の雰囲気を伝えることができれば幸いです。