Coq is not turing-complete, but IMHO, completeness is overrated :) I was trying to point that the "more powerful" criteria is pretty subjective. The OP said "

Coq is not turing-complete, but IMHO, completeness is overrated :) I was trying to point that the "more powerful" criteria is pretty subjective. The OP said "more powerful than the alternatives", that usually means "runs in the JVM"... and AFAIK, Jaskell or CAL are far from mature.