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 attributes.
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 pass?
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.
