On Thu, Jun 26, 2014 at 04:47:24PM -0700, Andrei Alexandrescu via Digitalmars-d wrote: > On 6/26/14, 4:16 PM, Timon Gehr wrote: > >- Annotations can include a formal proof. > > If a function can be annotated with what other functions it calls > (non-transitively), I agree that it can be guaranteed with local > semantic checking that a program won't overflow. However requiring > such annotations would be onerous, and deducing them would require > whole program analysis. > > >We've had similar discussions before. Why do we _still_ have to argue > >about the _possibility_ of having a system that is helpful for > >proving stack overflows (or other bad behaviours) absent? > > > >You can say "out of scope" or "not a priority" or "this should be > >realized in third-party tool support" but not "it is impossible". > > I also seem to reckon Walter is in the other extreme (he asserts it > can't be done at all, period). My understanding is that it can be done > but only with annotations or whole program analysis. [...]
I think the compiler should be able to tell, at least for the simplest cases, whether something will definitely stop recursing. Proving that something will *not* stop recursing is unsolvable in the general case, but even if we restrict it to a solvable subset, it's still far from trivial for the compiler to invent such a proof (unless we restrict it so much that it excludes too many useful algorithms). One approach is to have the user supply a proof that the compiler can then check -- in general, if a proof exists at all, it should be checkable. Such checks furthermore can probably be done fast enough so as to not adversely affect current compilation times (unless the proof is ridiculously complex, which for practical real-world applications I don't think will happen). However, absence of proof is not proof of absence; just because neither the compiler nor the user is able to come up with a proof that something will stop recursing, doesn't mean that it definitely won't stop recursing. So the compiler cannot definitively reject the code as definitely overflowing the stack. But we *can* make it so that the user tells the compiler "please stop compilation if neither of us can supply a proof that this function will stop recursing". But it has to be opt-in, because there will be many real-world applications that cannot be proven to stop recursing, even though in practice they always will, so we cannot make this a language default. One particular example that comes to mind is the compiler itself: as it parses the input program, there is in theory no guarantee that the input won't have an arbitrarily deep nesting, such that the AST generated by the parser will be infinitely deep, because you cannot statically prove that the input will terminate. You don't know if the input file is actually connected to the output pipe of a program that prints an infinite series of ever-deeper nested structs, for example. However, in practice, such input never occurs, so we generally don't worry about such contrived possibilities. But this does mean that there can be no proof of termination of recursion, even user-supplied ones -- because there *are* cases where the parser *will* recurse forever, even if it never happens in practice. Not accounting for that possibility invalidates the proof, so any proof will always be rejected. Therefore, it is impossible to prove that recursion in the compiler is finite, even though in practice it always is. T -- "Life is all a great joke, but only the brave ever get the point." -- Kenneth Rexroth
