well, since the halting problem is undecidable, then no. One thing I still do not understand is how languages like Coq and Idris can almost always ensure that programs written in them terminate.