When proving there are choices of "proof systems" to use. Each have different properties. One really vital property is non-contradiction. "Proving False" (note the capital 'F') is terminology for showing contradiction. From False you can (trivially) prove anything regardless of whether it is true.
Falso is a joke proof system which assumes False. This makes proofs in the system very short since they are all of the form "If False, [conclusion] is true; False is true; Therefore [conclusion] is true; QED."
Practically, proving False undermines the value of a proof system. Thus Coq, like all real proof systems, would like to ensure that does not contain contradiction.
The first joke is that this bug calls itself an implementation of Falso in Coq---e.g., a demonstration that Coq has a bug sufficiently dangerous to admit contradiction.
The second joke is that Falso's site---which is tongue-in-cheek hyperbolic on the supposed "benefits" of Falso as a proof system---lists "implementations" of Falso. In other words, that section is a "wall of shame" for proof systems which have flaws sufficient to "prove False".
---
To explain the exploit it has to do with a weakness in the `vm_compute` instruction under large sum types.
Essentially, Coq is based on the idea that "generalized lambda terms" are useful as proofs in a proof system. Part of this usefulness arises from the fact that their "proof system" meaning is invariant under evaluation. Normally evaluation of large lambda terms is slow so `vm_compute` compiles them to bytecode in a VM [0] and executes them there.
Apparently the VM chokes on sums larger than 256 variants. Since Coq assumes that "VM computation" is equivalent to "standard lambda term reduction". The VM bug breaks that equivalence and allows us to state that `true = false` which is contradiction.
---
Impact-wise this is pretty minor. It ought to be fixed since accelerating verification is important for UX purposes, but it doesn't show a weakness in the core calculus---the weakness arises from the assumption that VM evaluation is substitutable for standard, theory-driven lambda term reduction. Clearly this is false.
A much worse weakness, for example, was Girard's Paradox which showed that theories of a certain simplifying form were contradictory [1].
Falso is a joke proof system which assumes False. This makes proofs in the system very short since they are all of the form "If False, [conclusion] is true; False is true; Therefore [conclusion] is true; QED."
Practically, proving False undermines the value of a proof system. Thus Coq, like all real proof systems, would like to ensure that does not contain contradiction.
The first joke is that this bug calls itself an implementation of Falso in Coq---e.g., a demonstration that Coq has a bug sufficiently dangerous to admit contradiction.
The second joke is that Falso's site---which is tongue-in-cheek hyperbolic on the supposed "benefits" of Falso as a proof system---lists "implementations" of Falso. In other words, that section is a "wall of shame" for proof systems which have flaws sufficient to "prove False".
---
To explain the exploit it has to do with a weakness in the `vm_compute` instruction under large sum types.
Essentially, Coq is based on the idea that "generalized lambda terms" are useful as proofs in a proof system. Part of this usefulness arises from the fact that their "proof system" meaning is invariant under evaluation. Normally evaluation of large lambda terms is slow so `vm_compute` compiles them to bytecode in a VM [0] and executes them there.
Apparently the VM chokes on sums larger than 256 variants. Since Coq assumes that "VM computation" is equivalent to "standard lambda term reduction". The VM bug breaks that equivalence and allows us to state that `true = false` which is contradiction.
---
Impact-wise this is pretty minor. It ought to be fixed since accelerating verification is important for UX purposes, but it doesn't show a weakness in the core calculus---the weakness arises from the assumption that VM evaluation is substitutable for standard, theory-driven lambda term reduction. Clearly this is false.
A much worse weakness, for example, was Girard's Paradox which showed that theories of a certain simplifying form were contradictory [1].
[0] https://coq.inria.fr/distrib/current/refman/Reference-Manual...
[1] https://coq.inria.fr/library/Coq.Logic.Hurkens.html