Hacker News Reader

Comment by AnimalMuppet | Hacker News Reader

Two comments. First, it's interesting to me that they're saying that category theory really isn't adequate. Given how Haskell is based on category theory, is there somewhere more to go in programming languages?

Second, about proof-by-Coq: If there's ever a bug in Coq, they're going to have to re-run all the proofs that have been done this way, and see which (if any) of them are actually invalid. (It still may be better than proof by convincing humans, though...)

View on HN

> Two comments. First, it's interesting to me that they're saying that category theory really isn't adequate. Given how Haskell is based on category theory, is there somewhere more to go in programming languages?

Haskell isn't really "based on" category theory. There are just a lot of type-classes that implement category-theoretic machinery for quantifying over types and what you can do with the resulting data in a neat way.

>Second, about proof-by-Coq: If there's ever a bug in Coq, they're going to have to re-run all the proofs that have been done this way, and see which (if any) of them are actually invalid. (It still may be better than proof by convincing humans, though...)

It's been done before, when, IIRC, a VM bug appeared in Coq that allowed certain ill-formed programs to prove False.

Someone in another comment also mentioned the possibility of "proof libraries" that could be used to assemble more complex proofs from simpler ones. My first thought was, "I wonder what'll happen when someone finds a suble bug on one of the most common proof libraries?" It's bound to happen, after all. Some theorems will be proven false that were true and vice versa. A few people 90% of the way through their PhD will have years of their lives swept away.

The interesting thing about this is that trivial errors like this cannot happen (unless there is a bug in coq itself). For instance, I imagined using a library might be something like using a certain Theorem 1, with proof given by Proof 1. Since T1 and P1 are formalized, they've been verified!

So I can only think of some nontrivial mistakes: the Theorem 1 is correct, but it doesn't prove what you assume in your head T1 is saying, so that you may build some valid but tautological claims. I don't know if that's a huge concern, but in any case it could happen without proof verifiers anyway.

Disclaimer: I'm not actually a mathematician and I haven't tried coq yet (although I most certainly will! seems very interesting).

Check dedukti: http://dedukti.gforge.inria.fr/

It's a different proof assistant that can convert Coq's (and other P.A.) proofs into its own language and check them. It's not a guarantee of course, both Coq and Dedukti could have a similar bug. But it certainly helps having independent implementations being able to check the same proofs.

We're talking proofs here tho, and you aren't allowed to prove something by "throwing enough input at it", isn't it like saying that unit tests are proofs of the correctness of a program?

Well perhaps you could actually prove the correctness of coq itself.

In any case it's just a matter of reliability in the traditional sense: we're going to end with a small set of statements that will have to be verified by humans upon which we can rest everything else. Those statements will need enough people looking at them to get a level of certainty we're comfortable with.

I believe the risk of a major flaw going unnoticed is astronomically low, and the good thing is this certainty propagates all the way to modern proofs if we take care to go through formal verification.

That's no different from how regular math works. The whole point of this article is that mathematics is not formally verified today -- mathematicians just spot check and probe suspicious parts using informal analysis.

This is actually a valid proof technique with finite cases. This is known as a Proof by Exhaustion.

You can't have a bug in the proof library, or the proof-checker won't accept your proof as true! You can have a bug in the proof-checking kernel which makes it accept false theorems, but that's precisely why we keep proof-checking kernels as small and well-debugged as possible, sometimes going so far as to formally verify them too (Coq in Coq[1]).

[1] http://www.lix.polytechnique.fr/~barras/publi/coqincoq.pdf

Note that this already happens today. Mathematicians get a prestigious appointment based on a breakthrough work, which is then proven to be a mistake.

I'm no mathematician, but drawing a parallel between the general software world and software-aided mathematical proofs: wouldn't it be natural for a "compiler" to start off by using another technology (in this case, a classic "informal" programming language), and in a later date self-host? I'm saying, couldn't coq reach a state where he could prove itself and the technology stack below him down to axioms?

It's already in this state. See Coq-in-Coq, where Coq formalizes its own foundations. Note that this is not entirely convincing, because if Coq was in fact inconsistent then the fact that it could prove its consistency is not surprising. But it is impossible to truly overcome this, and it certainly goes a long way to improve confidence in the system.

If anything, Haskell is based on lambda calculus. More particularly System F.

As in any lambda calculus, you can interpret the type system as a category where the objects are types and the arrows are functions. Classes like Functor and Monad are based on this interpretation.

Well, all right, but then if you interpret the type system using a univalent approach, what do you get?

Reply on news.ycombinator.com