[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)