On 18.02.2016 21:57, H. S. Teoh via Digitalmars-d wrote:
>If you want to verify guarantees, @safe should be specified by
>inclusion and ideally, type safety should be proved formally (after
>applying a few fixes).
>This first requires a formal language semantics.
>That's already a lot of effort, and after that you still don't have a
>verified implementation.
I'm not sure how feasible it is to do a formal proof with the current
dmd code, since you'd have to freeze it, and as soon as the next PR is
merged, the proof is potentially invalidated.
The most obvious reason why it is infeasible to formally prove
correctness of the current dmd code is that it is not correct.
