Formal Proof Sketches (2003) [pdf] | Hacker News Reader

Formal Proof Sketches (2003) [pdf]

cs.ru.nl

30 pointslarve17 comments

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

You may be interested in the 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). 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.

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.

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.

Church's work on Lambda calculus preceded the electronic computer.

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.

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) ) was created in 1973 for manipulating proofs. C was created in 1972.

> formalizing mathematics currently seems far too much work to be worth the time of the working mathematician

A very general statement that isn’t true in all cases. I recommend taking a look at the LEAN mathlib project. It is a group of working mathematicians proving leading edge mathematics correct using a formal proof tool (LEAN).

The problem with leading edge mathematics seems to be that the proofs are too complex for anybody but a few specialists to verify the traditional way. And those specialists are already busy working on their own proofs. So having an automated assistant verifying the proofs seems to be necessary for the future of mathematics. I am not a working mathematician myself however that is the impression I am getting reading articles written by leading edge working mathematicians.

The same way that large complex software applications are too complex for humans to verify without the help of automated proof tools.

When Hales started in 2003 the Flyspeck project https://github.com/flyspeck/flyspeck to formally verify his own proof of the Kepler conjecture he likely didn't know that it would take him (and a team of helpers later) until 2014 to finish. He used hol-light, which is very much geared towards proof automation. Lean is more expressive (being dependently typed) but I am not aware of any real advance in automation over hol-light. Indeed with their focus on code generation (therefore constructive logic) and software verification, proof automation for math is likely harder in Lean. But the expressiveness and good tooling seem to have generated a lot of interests and mathlib has a real active community, which is really good to see.

Yep agree. Having an active team of working mathematicians and field medalists giving feedback to the LEAN development team is really helpful in pushing automation forward.

Having said that, for people like me, who doesn’t care about formalising mathematics but do care about proving code correct, proof automation has already come a long way and is on the edge of becoming a practical tool for highly critical software.

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.

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.

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.

Automated tools like Sledgehammer (Isabell/HOL) removes a lot of the manual work.

I have not used Sledgehammer but even with a SAT solver we still need to handle quantifier instantiations. And in case the SAT solver fails (I mean time-outs, not finding counter-examples) we won't get clues on how to fix it. SAT solvers work on CNF, which is very far from the deeply structured formulaes that math tends to generate.

I am not a working mathematician and don’t care about formalising mathematics. For the things I do care about (proving code correct) tools like Sledgehammer are awesome.

Dafny is a great example of what you are talking about. It automated most of the proving. However you still need to figure out the key invariants.

Reply on news.ycombinator.com