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

[Timon Gehr]

On 29.08.2018 21:58, Walter Bright wrote:
> 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.

If it's amenable to informal verification, it is also amenable to formal 
verification. Computers can check mathematical proofs, and if the code 
is proven correct it does not contain UB. This is independent of whether 
D classifies the code as @safe or @system.