Yet another leak in the sinking ship of @safe

[Timon Gehr via Digitalmars-d]

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.