On Thu, Jun 26, 2014 at 04:43:33PM -0700, Andrei Alexandrescu via Digitalmars-d wrote: > On 6/26/14, 2:01 PM, Araq wrote: > >> > >>Spark is a research language that does not work, as I've discovered > >>and discussed with you before. It cannot be determined the max stack > >>usage at compile time, again, this is the halting problem. > >> > > > >What?! It's easily solvable: Forbid recursion and indirect > >function calls > > I do agree that a useful subset of a language can be conservatively > defined that doesn't require solving the halting problem. But that's > not easy at all - it requires interprocedural analysis. [...]
And it may not be feasible for a compiler to automatically prove. One possible approach is to have the user supply the proof of eventual termination, which can be mechanically verified by the compiler. (Checking a supplied proof for correctness is more tractable than coming up with the proof in the first place.) But to handle proofs of non-trivial code beyond just toy examples, you might end up needing a full-scale deductive proof subsystem in the compiler, which may or may not be practical for D's needs! T -- That's not a bug; that's a feature!
