Software Assurance Reference Dataset

[H. S. Teoh via Digitalmars-d]

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!