3 ms·
Somewhat off topic, could someone post a list or examples of non-trivial (or relatively, non-trivial) decidable languages that have implemented compilers/interp
by j1vms 10y ago
Somewhat off topic, could someone post a list or examples of non-trivial (or relatively, non-trivial) decidable languages that have implemented compilers/interpreters? I should say no requirement on supported hw architectures, nor currently active development/maintenance.
- grapevines 10y agoAgda 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 10y agoThanks 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