The 3 axes of purely functional programming, logic programming and theorem proving are interrelated. It could be imagined that for each language listed below, they have a radar chart on all 3 axes, representing strengths and weaknesses. There's also a 4th axis for those concerned about non-programming language theory, that could be called "practicality", the ability to use it for practical engineering tasks. Finally there's a common theme between all 3 axes, which is "dependent typing".
- Coq - theorem proving
- Idris - functional programming and theorem proving
- Agda - functional programming and theorem proving
- Twelf - logic programming and theorem proving
- Prolog - logic programming