Hacker News Reader

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.

View on HN

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.

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

Reply on news.ycombinator.com