Hacker News Reader

> if you're well known and liked author, you often get a pass on your papers and they're not well checked for errors.

A friend who was advised by a "famous" (i.e., in his/her field) mathematician told me basically the same thing. This person unquestionably has had brilliant insights during the course of their career, most of which turned out to be correct. But (s)he has also published several false results, including one "major" false result. Some mathematicians are known to be sloppy and the field puts up with it, which seems weird to me.

Regarding Coq, never tried it, but here is my guess at what's going on. Coq seems to be mainly embraced by algebraists and people doing discrete math, less so in fields which are more analytic (optimization, probability, functional analysis, PDE, etc.) Proofs in the latter branches of math seem to more commonly invoke geometric or "intuitive" arguments which, while completely rigorous, are harder to reduce to a sequence of logical statements. Take for example "convexity implies continuity". You can basically prove this in 1d by drawing a picture, whereas the full, gory, rigorous version, though elementary, requires a little effort. Proofs in modern algebra, otoh, involve a lot of symbol pushing, which computers excel at. Just a guess.

When I worked as an RA while getting my BSCS (and for a time during my first post-college job), I spent quite a bit of time with ACL2 (a language, logic, and proof assistant using a first-order variant of common lisp). I spent a lot of time applying ACL2 to my research area (information flow analysis for secure systems), and I feel your pain re: proof strategies. It was almost like learning how to prove things again (e.g. learning new induction strategies that matched the logical framework used by the tool).

That said, there was an incredible amount of freedom in knowing that if the tool accepted a proof, it was (probably) correct. Occasionally I would stumble on to a strategy without knowing why exactly it worked, and the interactive nature of the tool helped me gain understanding by letting my apply transformations to terms interactively without having to worry about whether I screwed up some minor detail.

I'd love to see one of these tools (though, probably not ACL2 at this point - first-order logic frequently felt limiting (e.g. when proving things about parameterized equivalence relations)) used in a book covering some math topic I'd like to learn, as interactive formalism seems well-suited to self-exploration (you don't need an instructor to point out your trivial errors)

I really think that proof assistants like Coq are going to eventually be the future of math. Once they are less painful to use :(

I spent a term working as a research assistant on Coq, proving a new induction scheme for Featherweight Java classes. I came into the term quite hopeful, and already with some Coq experience, but I really don't feel like these tools are good enough to expect regular people to use. Even mathematicians.

I'm hopeful that in the distant future, we can get some AI assistance going on, so that the proof assistant can actually assist, not just check and impede.

I would like my month spent on transitivity of subclassing back :( It's really hard to use these tools as they are now.

I've heard some from people that it's almost like we are still at 'the assembly language' level when it comes to theorem proving. We still have a great deal to build in order to be productive at higher levels of abstraction.

>I would like my month spent on transitivity of subclassing back :(

Oh God, that gave me flashbacks. I've done at least one transitivity of subtyping proof where I actually got the right theorem, then found later in the module that I had to rewrite the whole thing with a graph-theory library supplying some theorems about DAGs/finite posets. It's horrible, and that piece of work still isn't done!

Analysis and the real numbers tend to be very hard to encode in constructive foundations. We still haven't got the right balance between checking for computability of the proof and all objects it hypothesizes, versus letting some of the types we hypothesize over be uncomputable and uncountably large, while requiring that propositional types (squash types) have continuous elements.

I was very interested in this as well for learning purposes. Without an instructor it's fairly easy to accidently make logical jumps and come up with wrong proofs. I figured that math is effectively a somewhat formal language for communicating concepts, so a compiler that checks errors (or even suggests corrections) could work well.

Tools like coq are great, but difficult to use (even as a programmer used to languages like Haskell) and they don't have a large set of existing proofs to work off of.

My opinion is that we need a good intermediate representation for proof tools (to share results; each new tool now needs a huge base built up to start being useful) and simpler tools to work with. It would be an enormous benefit to mathematicians and the world at large.

That'd be great, but I think the hard part about sharing representations is that many of the proof tools are based on different underlying type theories, which make it hard to go back and forth. For example Coq is based on the calculus of inductive constructions whereas Isabelle is based on HOL. Though, I'm guessing it's possible once a type scheme is fixed. Just poking around briefly, here's an SO question and answer on some of the differences between CIC and HOL (https://stackoverflow.com/questions/30152139/what-are-the-st...)

This should be possible when the underlying logics are similar (e.g. Isabelle/HOL and HOLight) but can be tricky if the logics are far apart (e.g. Isabelle/HOL and Coq).

Fair. I need to spend a few weeks with coq before I really form an opinion of how these things could be improved.

Newbie question: if one is not interested in extracting programs, but only in proving stuff, is a proof assistant like Isabelle/HOL easier to use than one based on constructive logic like Coq?

The short answer is yes. That's because (1) a classical system like HOL can use external automatic theorem provers ("sledgehammer") that are based on classical logic (most of them are), in a way that constructive systems like Coq cannot (at least currently). Moreover (2) classical proofs can be shorter and simpler, sometimes considerably so.

In practise many other dimensions also play an important role, in particular available tactics, tactic definition languages, proof editors, available decision procedures for the specific axioms one is interested in, libraries and so on.

Are there downsides to the HOL approach when compared to constructive systems?

It's hard to take something that's been proven true and turn it into something that's been proven useful without employing some constructive means.

I'm not sure I agree. For example CakeML [1] is the first fully verified self-hosting compiler for a substantial programming language, and seL4 [2] is the first fully verified substantial operating system kernel. Both were verified in LCF provers using HOL as a logic. Are you saying that the guarantees of correctness are not in themselves useful?

[1] https://cakeml.org/

[2] https://sel4.systems

If I write a program X and tell you it was proven correct, do you know that X is useful?

To know that a correct program is useful, you have to know what it does. And if you know what it does, you have constructed an implementation.

Which is to say that a nonconstructive verifier is really just deferring the 'constructive' part of its operation to the compiler and programmer. (And this is the 'hard part' I was referring to.)

I'm not sure what you mean.

We are discussing the (dis)advantages of HOL vs constructive reasoning (e.g. Coq). The main difference is that HOL-based provers like Isabelle/HOL has classical built in from the start -- all proof automation supports classical reasoning. Constructive reasoning eschews classical methods.

In order to prove the correctness of a program X, I need a specification S, and then I construct a proof P that X |= S, i.e. that X satisfies the specification S. I use an interactive proof assistant to check the proof P. There is no disadvantage that I can see if the proof P of X |= S is classical, at least from the point of view of program correctness.

Maybe you mean something else?

Depends what you want to do.

If you are interested in program verification, then not all that much, because everything is about automation. Coq/Agda have a small edge if you want to prove something about Lambda calculus since Coq/Agda are themselves Lambda calculi, and not surprisingly most Coq/Agda work is about Lambda calculus ... The HOL school has probably a small edge in other areas.

In practise the underlying approach (LCF vs Curry-Howard and dependent types vs HOL) makes much less of a difference than automation and availablility of proof libraries.

Although Coq is using constructive logic by default, it is not limited to it. One can use classical logic results just by importing the "Classical" module. Or course one then loose the benefits of having a constructive proof (like code extraction), but if the interest is only in checking a mathematical proof then it can be acceptable. The choice and trade-off is up to the user.

That is true, but does proof automation work as well for classical reasoning in Coq as it does in Isabelle/HOL where classical reasoning is 'baked in' from the start?

As far as I'm aware, the question of moving the "sledgehammer" approach to a constructive setting is still an open problem.