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.
