> we will have to very carefully prove that it cannot introduce any way to create a non-terminating function >The author wrote of total functional programming,

> we will have to very carefully prove that it cannot introduce any way to create a non-terminating function >The author wrote of total functional programming, a paradigm in which all functions and programs are provably terminating. So then what are you concerned about? Either use TFP, if indeed all your programs terminate, or have a different non-Turing complete approach, in which case you can still write infinite loops.