[tikhonj]

There are completely reasonable languages (distinctly non-broken) that are not Turing complete like Coq and Agda. You can still use them to write interesting, non-trivial programs! In fact, their limitations aren't immediately obvious--the only interesting program it's obvious they can't write is an interpreter for themselves or another programming language at least as powerful.