BP: Formal Proofs, the Fine Print and Side Effects (2018) [pdf] | Hacker News Reader

BP: Formal Proofs, the Fine Print and Side Effects (2018) [pdf]

people.scs.carleton.ca

50 pointsluu5 comments

It's a nice read, an important topic, that of not trusting blindly formal proofs. No theorem ever applies to real world objects, it can only say facts about ideas. It's good to keep that in mind but at the same time that's all we got, it's like a basic premise of science. That's why it's important be able to also do testing and have executable models, to validate that the model behaves like you think it should. But it's also what serious people do already even when doing formal proofs. And it's also why there's usually a difference between scientifically "solving" something and the art of making it actually work.

I've been practicing a bit TLA+ and one idea I've encountered—which I agree with— is: if we can't even get the idea to work, can we ever hope to get a working implementation?

And similarly: if we have a good idea about how the idea works, then perhaps it is easy to end up with a good implementation.

But the situation is of course completely different when you already have an implementation and you want to get "the simple idea" of how it works. And a lot of things you're going to interact with are those existing implementations, not just ideas of them.

> No theorem ever applies to real world objects, it can only say facts about ideas.

Einstein said something closely related:

https://www.maa.org/press/periodicals/convergence/quotations...

The whole article only has one occurrence of "BP", right there in the title. I wonder what it means?

At first I thought it referred to BulletProofs, a zero knowledge proving system, but it has nothing to do with that.

"Best Practices (BP) papers, up to 10 pages. Suitable papers are those that provide an integration and clarification of ideas on an established, major research area, support or challenge long-held beliefs in such an area with compelling evidence, or present a convincing, comprehensive new taxonomy of some aspect of secure development. Such a paper would be marked with the prefix 'BP:' in the title, and would need to provide new insights, although it could draw upon prior work." [https://secdev.ieee.org/2018/papers/#best-practices]

Reply on news.ycombinator.com