[HN Gopher] Formal Proof Sketches (2003) [pdf]
       ___________________________________________________________________
        
       Formal Proof Sketches (2003) [pdf]
        
       Author : larve
       Score  : 25 points
       Date   : 2022-08-22 23:41 UTC (1 days ago)
        
 (HTM) web link (www.cs.ru.nl)
 (TXT) w3m dump (www.cs.ru.nl)
        
       | pflanze wrote:
       | (I'm a software developer, not a mathematician. I'm just starting
       | to try to understand the proof world.)
       | 
       | I'm not sure about the "disdain" the authors have about "program
       | source code". The parallel between proofs and programs seems
       | clear, a runnable program is only one for which all
       | functions/subroutines/methods (in other words, abstractions) have
       | been implemented.
       | 
       | We try to structure programs so that the abstractions are as
       | sensible as possible, with good, preferably memorable names. A
       | well-written program is one where the higher level is short and
       | understandable without (always) having to dive into what the used
       | abstractions do. It is an aim we seem to share with the writers
       | of the paper. Sure, real world might be different, but the
       | technology allows us to write well-readable programs.
       | 
       | Other attempts like UML/flowcharts exist, but AFAIK attempting to
       | connect these to runnable programs (i.e. make them _formal
       | program sketches_ in the sense of the proof sketches in the
       | linked paper) has largely been a failure (correct me if I 'm
       | wrong). The idea to write the program and mark the parts that
       | should show up in a flowchart (i.e. the inverse of what I've
       | mostly seen talked about, program generation from UML), to get a
       | "human readable" version of the program, might be a new one.
       | Maybe if mathematicians succeed with that, it would be as
       | applicable to software engineering?
       | 
       | In any case, am I correct in saying that the envisioned aim is
       | the same? Does mathematics have peculiarities that make the
       | situation different (other than, perhaps, mathematicians
       | generally not being used to "programming", or fully formalizing
       | something)? Is this a "teething" stage in mathematics like UML
       | was in software engineering and will largely be superseded by
       | just "structuring programs/proofs well", which entails creating
       | "nice libraries"?
       | 
       | PS. I have ignored that the paper is from 2003 (about the time of
       | UML's heyday, incidentally). What has happend to the idea of
       | proof sketches in the mean time? Is this what "tactics" is about?
        
       | fspeech wrote:
       | We need to develope tools that can automatically fill small gaps
       | (ones left as errors in the essay), because the point of having
       | mechanized proofs is to not have gaps. Then practitioners can
       | write lemmas and let the computers do the checking.
        
         | reuben364 wrote:
         | In the proof assistants I'm familiar with, such as Lean and
         | Coq, you can write tactics which generate proofs for a goal and
         | potentially produce more subgoals. However there isn't a "one
         | size fits all" tactic for these gaps. One area that is being
         | explored is ML for generating proofs, but training data is
         | limited.
        
           | fspeech wrote:
           | The tactics still require users to be aware of their
           | existence and using them correctly (a non trivial mental
           | load). And the resulting proof script is brittle and hard to
           | read. This is what the essay attempted to improve over.
        
       ___________________________________________________________________
       (page generated 2022-08-24 23:02 UTC)