I’m not a mathematician, but Falso is a satire about axiomatic systems. Some mathematicians have debates about which axioms are acceptable or not (I understand it can be very similar to the debates we can have about programming languages and type systems).

Falso assumes contradiction as its only axiom, which makes it super easy to prove anything :)

The link points to an “implementation” of the Falso axiomatic system in Coq, which is an interactive theorem prover. This is funny because 1) this is useless and 2) the implementation was made possible thanks to a minor bug in Coq.

It has come to our attention that several alternative operating systems such as “Linux” include a utility known as “/bin/true” which has been presented as a free, “open source” alternative to our Estatis Falso HyperVerifier program.

Users of these systems should be aware that this pirated software is illegal and infringes on intellectual property belonging to Estatis Inc. Estatis is currently engaged in legal proceedings to enforce its rights and stop the distribution of this unlawful program. Besides, you should know we have identified numerous flaws in “/bin/true” which make it unsuitable for production use and which can lead to grossly incorrect results. (For instance, “/bin/true” fails to check the well-formedness of its input.)

Open source and pirate programs are a threat to your computers and your mathematical activity. Always use genuine versions of Estatis Inc. products.

I’m hoping someone else more versed in the lore will chime in and enlighten us all further but in the meantime - I find it funny because Coq is a tool that’s supposed to help you prove theorems. But if you can prove false then you can prove anything! I suppose this also means that you should take theorems proven by Coq with a grain of salt. I’m not sure how many programs might run into this bug so maybe only a very small grain of salt is in order.

This is an implementation bug. If you don’t use vm_compute (and you shouldn’t, unless your proof needs a large computation and verification is too slow otherwise), you are okay.

Much more worrying are theory bugs. Recently it was found that propositional extensionality (which states “P iff Q” is equivalent to “P is Q”) leads to contradiction in Coq. Details are here: https://news.ycombinator.com/item?id=9261196

For those of us who are not mathematicians, what does this mean, how is it significant or funny?

I’m not a mathematician, but Falso is a satire about axiomatic systems. Some mathematicians have debates about which axioms are acceptable or not (I understand it can be very similar to the debates we can have about programming languages and type systems).

Falso assumes contradiction as its only axiom, which makes it super easy to prove anything :)

The link points to an “implementation” of the Falso axiomatic system in Coq, which is an interactive theorem prover. This is funny because 1) this is useless and 2) the implementation was made possible thanks to a minor bug in Coq.

Reading Falso’s home page may bring some clarity:

http://inutile.club/estatis/falso/

Hah:

I’m hoping someone else more versed in the lore will chime in and enlighten us all further but in the meantime - I find it funny because Coq is a tool that’s supposed to help you prove theorems. But if you can prove false then you can prove anything! I suppose this also means that you should take theorems proven by Coq with a grain of salt. I’m not sure how many programs might run into this bug so maybe only a very small grain of salt is in order.

This is an implementation bug. If you don’t use vm_compute (and you shouldn’t, unless your proof needs a large computation and verification is too slow otherwise), you are okay.

Much more worrying are theory bugs. Recently it was found that propositional extensionality (which states “P iff Q” is equivalent to “P is Q”) leads to contradiction in Coq. Details are here: https://news.ycombinator.com/item?id=9261196