Coq is a proof assistant, where "proof" is in the mathematical sense of the term. Thanks to Curry-Howard isomorphism [1], it happens that there's a mapping between proofs and programs, meaning that the "proof assistant" can do things like "prove a sorting algorithm correctly sorts all inputs" in a relatively straightforward manner. I mean, still fairly complicated and not something that you'll encounter in an undergrad computer science education in general, but feasible. For instance, a similar tool was recently used to prove that the sorting algorithm in Python and Java had a bug [2], which was a bit surprising given how well-exercised they were.

Something that a computer science program should cover is that a logical implication is always true when the antecedent is false. X -> Y is always true when X is false. Thus, if you can convince your system to prove a false term, you can set that as the X and write anything you want for the Y, and prove anything. (That statement is actually glossing over a bit of discussion on how you can legally introduce statements into your system, and there's variance between the logics on that point anyhow, but that's what it comes out to in most if not all systems.) Therefore, if you can prove a false statement, you can literally prove anything.

This turns out to be an unhelpful characteristic for a proof system to exhibit. In the case of Coq, it means you can now convince it to take any program as satisfying any property. Any program, satisfying any property. You want to prove that "return []" is a proper sorter for any input? This can do that. Heck, you want to prove that "return []" is a valid fully HTTP5 rendering engine? We can do that too!

In this particular case, it exploits a bug in Coq to do that, but the fear mathematicians have developed over the course of the 20th century is that while the bug may be obvious, deeper, more subtle problems in Coq could conceivably be used to prove "False" oven the course of a proof, accidentally and buried in potentially hundreds or thousands of statements, subtly rendering all such proofs flawed. Such are the things that keep mathematicians up at night.

As long as I'm explaining things, let's also explain the joke in Falso. There are, as the page says, a number of different axiom systems. Some of them are simply wildly different; for instance, Euclid's axioms create Euclidean geometry, whereas axioms about vertices and edges create graph theory. Some are more related... the 20th century resulted in several "set theories", which are ultimately characterized by different axiom sets that lead to different places. Axioms are neither right nor wrong, they are the definition of a branch of math, so you can choose them as you like, then see where they take you. Per the previous paragraphs, you prefer not to have an axiom system that allows you to prove false because it reveals your system doesn't actually say anything because it just says "Yes!" no matter what you ask. In some sense this isn't "invalid" or "wrong" either, it's just useless. (And in some sense, there's only one axiom set that just says "return true", there's just more and less complicated ways of spelling it, so there's not much value in trying to "study" one because it's identical to "return true" anyhow.)

The joke in Falso is that it simply takes as an axiom "For all P, the proof of P is the null statement", which, for the purposes of this post, is essentially "Assume false is true." From this, Falso can therefore prove... anything! In one statement! At this point the "comparison table" ought to start making sense. But the page is full of other little mathematician jokes... for instance:

Let us prove that P = NP by contradiction. Assume that P ≠ NP.
Then, by the axiom of the Falso system, we have a contradiction.
Therefore, P = NP.

The joke here being that under the Falso system, "proof by contradiction" isn't actually necessary; you want "P = NP"? Just set it as the "P" in the axiom and read it off in one step, "The empty statement proves P = NP". Proof by contradiction is unnecessary frippery providing the thinnest, thinnest of covers over the triviality of the proof, which is itself the joke. As opposed to a huge proof of dozens of steps, which could be funny in its own way, it is also mathematician-funny to provide the smallest possible obfuscation. (The remainder of the joke is a slightly disguised allusion to the fact that "P ≠ NP" is equally trivially provable under Falso. Estatis Inc. need not wait anxiously by their mailbox for their million dollars from the Clay institute.)

Mathematicians have a strange sense of humor. Strange, but wonderful.

As I said, the last time I encountered this page [3], which HN says was 2 years ago, it didn't have any implementations, it was just an extended joke. The fact that it is now actually "available" is also sort of funny.

Oh, and finally, I can't read or use Coq either. Plus, even if you could, this is ultimately a bug exploit, not a "real proof", which would make it even harder to understand how what is being done relates to the final result; it's like seeing some random-looking assembler that turns out to produce arbitrary code execution due to some quirky combination of bugs, there isn't any apparently relationship between what the assembler looks like it's doing and the result it actually produces. Haskell's close enough for me for now. I'm also willing to wait and see if homotopy type theory follows through on its promises to make proofs simpler... at the moment, as I am ultimately a software engineer and not a mathematician, I can't help but see current proof technology as too much work for too little gain. I wish all those working to change that assessment all the best, though.

[1]: http://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspond...

[2]: http://envisage-project.eu/proving-android-java-and-python-s...

[3]: https://news.ycombinator.com/item?id=5677646