18 ms·
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–Howar
by 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 agoYes, 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 agoI 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 agoChurch's work on Lambda calculus preceded the electronic computer.
- pflanze 4y agoI 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 agoThat'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.