On Monday, 11 July 2016 at 16:18:47 UTC, Dietrich Daroch wrote:
Previous discussion seems to favour @unboundedStack as it can
become a requirement to go beyond the stack-size-safe
operations effectibly tracking where stack overflow may happen
and encourage detailed review of those functions.
I would favour it, but I am not a DMD developer ;-)
Walter's concern is that a great amount of the D runtime
library would make this unpractical. Maybe another attribute to
promise bounded stack without a proof might be required to make
the idea viable.
I really think that this kinds of proofs are somewhat natural
in D, as it follows ideas like contracts, and safe/trusted
Yes. Although keep in mind that DMD does not have a shared
intermediate representation, so each backend probably might have
to implement it over a low level SSA which may or may not be
suitable. So, if they have to implement 3 different versions of
it for DMD, LDC and GDC what are then the chances that this will
Contrast this to a language like Whiley which has an intermediate
representation geared towards theorem-proving.
Would D benefit from a shared intermediate representation
suitable for static analysis? Sure. But you probably need more
than a single feature-request to get there.