On 06/26/2014 10:29 PM, Walter Bright wrote:
On 6/26/2014 2:52 AM, Timon Gehr wrote:
On 06/26/2014 11:35 AM, Walter Bright wrote:
On 6/26/2014 2:19 AM, bearophile wrote:
One kind of problem left is to avoid stack overflows.
In general, stack overflow checking at compile time is the halting
problem.
That is irrelevant to his point because he is not suggesting to solve the
general problem precisely. Analogously: In general, checking whether some
variable in e.g. Python is ever assigned a string value is undecidable
as well,
but this does not imply we cannot have 'int' variables in D.
When you're dealing with security issues, which is what this about,
This is about _avoiding stack overflows_. It's written down literally in
the quoted passage.
you'll need a guarantee about stack overflow. Adding annotations is not
helpful with this because they are not checkable.
...
Not true. Basic facts:
- In practice, programs are constructed explicitly to fulfill a
particular purpose and, in particular, if they do never overflow the
stack, they usually do so for a reason.
- Reasoning can be formalized and formal proofs can be written down in
such a way that a machine can check whether the proof is valid.
- Annotations can include a formal proof.
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".
Again, what WORKS is a runtime check.
A runtime check will not avoid the problem, which is exhaustion of stack
space.
