[HN Gopher] BP: Formal Proofs, the Fine Print and Side Effects (... ___________________________________________________________________ BP: Formal Proofs, the Fine Print and Side Effects (2018) [pdf] Author : luu Score : 40 points Date : 2023-07-21 19:42 UTC (1 days ago) (HTM) web link (people.scs.carleton.ca) (TXT) w3m dump (people.scs.carleton.ca) | tromp wrote: | 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. | hovav wrote: | "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] | lapinot wrote: | 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. | _flux wrote: | 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. ___________________________________________________________________ (page generated 2023-07-22 23:00 UTC)