3 ms·
I'm impressed by Filip's knack for explaining complex topics in an approachable manner. His previous post on WebKit's locking infrastructure[1] is a similarly g
by bdash 10y ago
I'm impressed by Filip's knack for explaining complex topics in an approachable manner. His previous post on WebKit's locking infrastructure[1] is a similarly good read.
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".
[1]: https://webkit.org/blog/6161/locking-in-webkit/ https://webkit.org/blog/6161/locking-in-webkit/
- agentultra 10y agoWhile that proof is amusing I was hoping for... an actual proof that I can give to a verifier. Ah well. A hundred or so lines of comments is probably right. Still this looks to be some impressive work and I did enjoy this post.
- pizlonator 10y agoI'm a mathematician. Proofs are one of the means of communication between me and other mathematicians. I don't give a crap if a computer can read my proof.
- corndoge 10y agoWell, us programmers do since computers are the ones we're communicating with.
- pizlonator 10y agoI like to write programs when I program and proofs when I mathematize. The program is for the computer and the proof is for a human. I think you're getting it all mixed up!
- corndoge 10y agoI think you're wrong!
- nickpsecurity 10y agoQuite a few people held that view in this article: https://www.quantamagazine.org/20130222-in-computers-we-trust/ 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.
- nickpsecurity 10y agoMaybe he means proof like lawyers use it instead of mathematicians. Im sure his proofs are quicker that way. ;)
- AnimalMuppet 10y agoLawyers are faster than mathematicians? In fact, that's probably right, but I'm experiencing cognitive dissonance right now...
- moomin 10y agoDepends how much you overclock your mathematician.
- nickpsecurity 10y agoThey sure prove, err argue, faster.
- ooqr 10y agoThe justice system has more overhead.
- nickpsecurity 10y agoJust means it's ripe for disruption by a YC startup.