Thanks for the pointer. It appears that proof assistants [0], like Aqda as you mentioned and one of its influences Coq [1], have the properties I were describin

Thanks for the pointer. It appears that proof assistants [0], like Aqda as you mentioned and one of its influences Coq [1], have the properties I were describing and indeed are examples of total functional programming [2]. [0] https://en.wikipedia.org/wiki/Proof_assistant https://en.wikipedia.org/wiki/Proof_assistant [1] https://en.wikipedia.org/wiki/Coq https://en.wikipedia.org/wiki/Coq [2] https://en.wikipedia.org/wiki/Total_functional_programming https://en.wikipedia.org/wiki/Total_functional_programming