[grapevines]

Agda is a programming language where "each program in it must terminate and all possible patterns must be matched. Without this feature, the logic behind the language becomes inconsistent, and it becomes possible to prove arbitrary statements."

Since all programs terminate, reasoning about arbitrary properties about said programs becomes decidable.

[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