[HN Gopher] Formally Verifying Industry Cryptography
       ___________________________________________________________________
        
       Formally Verifying Industry Cryptography
        
       Author : todsacerdoti
       Score  : 21 points
       Date   : 2022-07-12 06:34 UTC (2 days ago)
        
 (HTM) web link (www.computer.org)
 (TXT) w3m dump (www.computer.org)
        
       | mbrodersen wrote:
       | It's great to see that proving code correct is starting to make
       | inroads into commercial software development. Perhaps the term
       | "Software Engineer" should be reserved for software developers
       | who have the training/skills to formally prove software correct?
       | The same way that Engineers in other industries have the formal
       | training/skills needed to use mathematical models to
       | build/construct correctly?
        
         | ebingdom wrote:
         | As someone with years of experience writing machine-checked
         | proofs in Coq, I cannot imagine the term "Software Engineer"
         | shifting to that meaning, even though it may make sense when
         | compared to other engineering disciplines. The programmers who
         | have no experience with this technology outnumber us many
         | thousands to one. They'd never sign off on it.
         | 
         | That said, I'm all for anything that results in more
         | appreciation for mathematical rigor in programming. It's like
         | puling teeth trying to get colleagues to use tools/languages
         | that help with reasoning about code (even just a good type
         | system), and for a lot of programmers math seems to be an
         | unapproachable alien language.
         | 
         | One thing I'd like to change about the software industry is the
         | perception that formal verification is too hard to do in
         | practice because you can't even write down a complete
         | specification for the program. The misconception there is that
         | the all of the program's behavior needs to be specified in
         | order for formal verification to be useful. Why can't gradual
         | formal verification be a thing?
        
       ___________________________________________________________________
       (page generated 2022-07-14 23:00 UTC)