[zozbot234]

> I don't see why people won't just take the step D and Lisp do-- allowing full use of the programming language at compile time.

Because "full use of the programming language" implies Turing completeness, which means compilation may require unbounded time and compute resources. You can allow use of a non-Turing complete subset, and this is something that dependently-typed languages can do quite elegantly.

[pilif]

Many type systems are already Turing complete like C++ and indeed Rust as evidenced by the project linked here.

It’s a valid point. Of compilation already is Turing complete, why not just drop the pretense and allow arbitrary compile time expressions.

[dllthomas]

Even where nothing in compilation is Turing complete, many pieces may be unbounded. And where there are artificial bounds, they could as well be applied to something otherwise Turing complete.

[dependenttypes]

A program that requires 2^256 time units and 2^256 memory units is not really any better compared to unbounded computations.