On Wednesday, 8 June 2016 at 13:43:27 UTC, Timon Gehr wrote:
On 08.06.2016 01:59, Walter Bright wrote:
...
I suspect D has long since passed point where it is too
complicated for
the rather limited ability of mathematicians to prove things
about it.
The main reason why it is currently impractical to prove things
about D is that D is not really a mathematical object. I.e.
there is no precise spec.
Besides that, even if a @safe checker is slightly flawed, it only
has to be vetted better than the backend which most likely is
unverified anyway.
This is different from some of the static analysis done on C,
which convert the LLVM bitcode or even X86 assembly into a format
that can be queried using a solver. That way the proof holds even
in the case where the backend is buggy.
