[IngoBlechschmid]

> To me, ultrafinitism is an intellectual curiosity. Proofs which depend upon the axiom of choice, or a notion of infinity, do not always correspond to algorithms which terminate in finite time. Such results are "useless" to a computational mathematician.

Fun fact: For certain kinds of results, there is an explicit procedure for transforming any given ZFC-proof into an IZF-proof. By ZFC, I mean classical "uncomputable" mathematics with the axiom of choice and with the law of excluded middle. By IZF, I mean (a specific flavor of) constructive mathematics without those two contested axioms.

In particular, this metatheorem applies to termination results. So feel free to use the axiom of choice and the law of excluded middle to your heart's content when proving that a program terminates; you can trust that at the end of the day, your proof can be transformed to a constructive proof.

Slides which I hope are also accessible to non-specialists in proof theory: https://www.speicherleck.de/iblech/stuff/37c3-axiom-of-choic...

More pointers to the literature: https://math.stanford.edu/~feferman/papers/reductive.pdf