6 ms·

(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 abou

(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 4y ago
You may be interested in the Curry-Howard correspondence https://en.m.wikipedia.org/wiki/Curry–Howard_correspondence https://en.m.wikipedia.org/wiki/Curry–Howard_correspondence Tactics can be thought of functions that manipulate proof contexts (e.g. sequent calculi https://encyclopediaofmath.org/wiki/Gentzen_formal_system https://encyclopediaofmath.org/wiki/Gentzen_formal_system). Tactical proof is like imperative programming where one specifies explicitly how a proof should be constructed. Ideally we want to move towards declarative proofs, where one specifies lemmas that can be checked automatically. To be exact, suppose H1, ..., Hn are hypotheses (including known axioms and theorems), we want to derive Th by finding a sequence of propositions L1 ... Lm (=Th) such that L_(i+1) can be derived automatically from the hypotheses plus L1 through Li.
- zozbot234 4y ago
  Yes, the whole problem of defining a "formal proof sketch" becomes trivial if you have a declarative proof language. More recently, even tactics-based scripts have gained semi-declarative features such as "bullet" characters for marking subgoals, and such things might ease transition towards a fully declarative format.
  - pflanze 4y ago
    I see, so maybe the "disdain" about "program source code" might be more about disdain for imperative programming? It sounds a bit funny or at least interesting to me if mathematicians pick up functional programming no earlier than the software engineering world, given that functional programming is about being descriptive like mathematics itself.
    - fspeech 4y ago
      Church's work on Lambda calculus preceded the electronic computer.
      - pflanze 4y ago
        I know (although I still haven't actually read Church's work). So I know some mathematicians approached things that way. I'm just a bit puzzled that it's not the default for formalizing proofs, too. But I'll stop making conjectures now.
        fspeech 4y ago
        That's because proof calculus (such as natural deduction) specifies how parts of a logic formula can be manipulated without changing its meaning. It's easier to prove and maintain the universal correctness of underlying mechanics that way. As for functional programming, ML (the Meta Language, where the object language is HOL or Higher Order Logic https://en.m.wikipedia.org/wiki/ML_(programming_language) https://en.m.wikipedia.org/wiki/ML_(programming_language) ) was created in 1973 for manipulating proofs. C was created in 1972.

fspeech 4y ago

You may be interested in the Curry-Howard correspondence https://en.m.wikipedia.org/wiki/Curry–Howard_correspondence https://en.m.wikipedia.org/wiki/Curry–Howard_correspondence Tactics can be thought of functions that manipulate proof contexts (e.g. sequent calculi https://encyclopediaofmath.org/wiki/Gentzen_formal_system https://encyclopediaofmath.org/wiki/Gentzen_formal_system). Tactical proof is like imperative programming where one specifies explicitly how a proof should be constructed. Ideally we want to move towards declarative proofs, where one specifies lemmas that can be checked automatically. To be exact, suppose H1, ..., Hn are hypotheses (including known axioms and theorems), we want to derive Th by finding a sequence of propositions L1 ... Lm (=Th) such that L_(i+1) can be derived automatically from the hypotheses plus L1 through Li.

zozbot234 4y ago
Yes, the whole problem of defining a "formal proof sketch" becomes trivial if you have a declarative proof language. More recently, even tactics-based scripts have gained semi-declarative features such as "bullet" characters for marking subgoals, and such things might ease transition towards a fully declarative format.
- pflanze 4y ago
  I see, so maybe the "disdain" about "program source code" might be more about disdain for imperative programming? It sounds a bit funny or at least interesting to me if mathematicians pick up functional programming no earlier than the software engineering world, given that functional programming is about being descriptive like mathematics itself.
  - fspeech 4y ago
    Church's work on Lambda calculus preceded the electronic computer.
    - pflanze 4y ago
      I know (although I still haven't actually read Church's work). So I know some mathematicians approached things that way. I'm just a bit puzzled that it's not the default for formalizing proofs, too. But I'll stop making conjectures now.
      - fspeech 4y ago
        That's because proof calculus (such as natural deduction) specifies how parts of a logic formula can be manipulated without changing its meaning. It's easier to prove and maintain the universal correctness of underlying mechanics that way. As for functional programming, ML (the Meta Language, where the object language is HOL or Higher Order Logic https://en.m.wikipedia.org/wiki/ML_(programming_language) https://en.m.wikipedia.org/wiki/ML_(programming_language) ) was created in 1973 for manipulating proofs. C was created in 1972.