[HN Gopher] Social processes and proofs of theorems and programs...
       ___________________________________________________________________
        
       Social processes and proofs of theorems and programs (1979) [pdf]
        
       Author : amadeuspagel
       Score  : 18 points
       Date   : 2023-05-18 19:50 UTC (1 days ago)
        
 (HTM) web link (www.cs.umd.edu)
 (TXT) w3m dump (www.cs.umd.edu)
        
       | giraj wrote:
       | The paper argues against those who think that "programming should
       | strive to be more mathematical" through the development and
       | adoption of formal methods. It points out that "more
       | mathematical" does not implicate formal methods, since proofs by
       | mathematicians are informal and their correctness is established
       | by social processes. The author fears that an over-emphasis on
       | formal methods could stifle innovation (in particular, in
       | programming language design).
       | 
       | As a mathematician that works with proof assistants, I largely
       | agree with this thesis. However, I don't think there is any
       | reason to have any such fears associated with formal methods. I
       | think informal proofs, as the exist in both CS and maths, are
       | here to stay. And, on the contrary, I think investigations into
       | formal methods can drive new theory and insight. For example, one
       | could say that the formal system of homotopy type theory (HoTT)
       | is a programming language created in order to reason about highly
       | "coherent" mathematical structures, which HoTT often does very
       | well. In addition, being a formal system, HoTT is well-suited for
       | formal methods -- but even so, many mathematicians still prefer
       | to work informally in this language.
       | 
       | In summary, I think the article makes a valid point, but the
       | motivating fears seems unfounded in retrospect.
        
       | deterministic wrote:
       | The paper shows its age. A lot has happened since 1979. Projects
       | like CompCert, seL4, Project Everest, Coq, Dafny, F* etc. shows
       | what can be done with modern proof tools. And it is getting
       | better every day.
       | 
       | And I will claim that "formal" proofs, as practiced today by most
       | professional mathematicians, are basically just informal proofs
       | with more details, reviewed by flawed humans in a social process.
       | Nothing wrong with that of course! But just pointing out that it
       | doesn't reach the high level of confidence that modern proof
       | tools can deliver.
       | 
       | The LEAN/mathlib project is an interesting example of what the
       | future of truly formal mathematics might look like.
        
       | dang wrote:
       | Related:
       | 
       |  _Social Processes and Proofs of Theorems and Programs (1979)
       | [pdf]_ - https://news.ycombinator.com/item?id=16421444 - Feb 2018
       | (1 comment)
        
       ___________________________________________________________________
       (page generated 2023-05-19 23:02 UTC)