Thank you for the great question @EliBenSasson!
"Which language will folks program in".

As you know, polynomial circuits are used to verify. Cairo obscures this distinction in order to present one particular programming metaphor to the user (the Cairo VM), which is fine, but many programming paradigms are possible and in any case what matters is not what gets coded but what gets verified.

For instance: functions can be specified directly in (first-order) logic. Section 3 of the paper shows how, and in particular it presents a selection of functions, including general recursive functions, within Gabbay's framework. In the paper as written this is a theoretical definition aimed at theoreticians, and accordingly Gabbay uses rationals instead of finite fields -- but it's quite clear that similar principles would apply over a finite field. It's not an essential distinction.

One special case is relevant: it's clear from Gabbay's paper that validity of derivation-trees can be specified using this framework - e.g. the specification of derivation-trees for SK combinator reduction, which is interesting in itself and because it is paradigmatic for many other such definitions. Inductive definitions are a sufficient and convenient basis for declarative programming. So if we do want to present a programming abstraction to the user, that's one straightforward, mathematically principled way to do it, that involves minimal overhead. There are others.

While the above is not in itself a mathematical proof, I hope this gives a flavor of an answer to the question.