Dicebot on leaving D: It is anarchy driven development in all its glory.

Walter Bright newshound2 at digitalmars.com
Wed Aug 29 19:58:20 UTC 2018


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.


More information about the Digitalmars-d mailing list