[dependenttypes]

> A language that is Turing complete at compile means that an IDE cannot reliably tell whether code has a syntax error without running a program that can take arbitrarily wrong.

A language that is not Turing complete at compile-time does not necessarily mean that an IDE will be able to reliably tell whether a certain piece of code has a syntax error without running a program that can take an arbitrarily amount of time to finish.

[btilly]

It is possible to construct counterexamples, but in practice it tends to work out much, much better.

The various tools built around Java stand as an example.