A few amusing parts of this post that stood out to me:
* A single sentence containing half a dozen links to Filip's previous work on garbage collection.
* "See here for the proof", linking to a 200+ line comment in WebKit's source.
* "But since this is JavaScript, we get to have a lot more fun".
Still this looks to be some impressive work and I did enjoy this post.
I don't give a crap if a computer can read my proof.
I think you're getting it all mixed up!
https://www.quantamagazine.org/20130222-in-computers-we-trus...
It and others I've read on machine-checked proof showed the computer-centric one could catch quite a few problems with higher assurance of correctness. The peer review problem in science also makes me think it's important given I can't be sure the huge proofs will be adequately checked. Far as reliability on computer end, I've read on verified processors, proof assistants, compilers, and so on. Much of the risk can be knocked out but the black box that is human brains is another story.