[Jweb_Guru]

A proof that the language and system description are accurate and complete is very difficult, I agree. But it only has to be done once, it does not have to be repeated for each proof, so that does not seem relevant to me wrt the advantages of such a proof.

As for your first point, I would wager (having done it many times) that it is considerably easier to translate a proven, working program to another language correctly, than it is to do the same thing with an abstract state machine.

[ncmncm]

For it to be "done once", it has to be done at all. I have not seen any reason to believe it was done at all. When posting a boast about having done the easy part, it does not inspire confidence that the hard part was done, too, but nobody thought the hard part was worth mentioning.

So, until I see the announcement, the reasonable interpretation is that it has not been done.