[j1vms]

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

[1] https://en.wikipedia.org/wiki/Coq

[2] https://en.wikipedia.org/wiki/Total_functional_programming