On 8/29/2018 11:02 AM, Timon Gehr wrote:
Absolutely. But D only strives to provide such automation in @safe code. For @system code, we need a formal specification of what is allowed. (And it needs to include all things that the GC and language do; no magic.) Note that such a formal specification is a prerequisite for any (possibly language-external) automated verification approaches.
I don't think that @system code is amenable to formal verification. After all, you can do UB in it, and it is the programmer's responsibility to ensure it works.
