Hacker News Reader

Comment by synthecypher | Hacker News Reader

Anyone care to ELI5?

Coq is a proof assistant. It helps you to prove things, or at least check that your proofs are correct. For instance, people use it to prove mathematical theorems, or correctness of critical software.

But apparently, there's a bug in the system that allows you to prove any properties, even invalid ones.

So suppose that you proved Fermat last theorem in Coq, now you're not sure your proof is correct anymore since the deduction system is flawed!

In theory, it invalidates all the proofs written in Coq. In practice, I don't think it's a big deal because it's unlikely that those proofs rely on this bug. But it's pretty funny to see that a system designed to be the ultimate verification tool is bugged.

Logic systems can have bugs in them that make them inconsistent, which means that you can prove false (or bottom or whatever), which means that you can prove anything in this logic. And that, in turn, makes the logic system useless since for any given formula, it is provable in that logic. And being able to prove everything is not fun.

Then you have to patch your logic and make sure that none of your proofs relied on that inconsistency. Or something like that.

You can re-run your proofs once the bug is patched, so its not like this makes all those proofs useless. Actually, that is the nice thing about Coq.

How do you know there isn't another, yet undiscovered, bug?

You don't, but so what? Even proofs done well by hand can have obscure mistakes; most of the time they don't invalidate the proof. Take a proof as strong evidence of correctness and it all works out from a epistemological point of view.

Can you explain what the program itself is doing to do that? That is, can you explain the Coq program itself (and how it triggers the bug)?

The program defines a type `t` with 257 constructors (`C_0` through to `C_256`). As an analogy, the type `boolean` has two constructors (`true` and `false`).

Each of these constructors takes a natural number as an argument.

It then defines a function `is_256` which checks whether it's argument has the form `C_256 n` for some `n`, returning a boolean.

It then defines the value `falso` of type `False` (which shouldn't be possible). It does this by defining two values: one has type `is_256 (C_256 0) = true`, the other has type `is_256 (C_256 0) = false`. This is clearly a contradiction, which is used to construct the value `falso`.

The reason one value gives `true` and the other `false` is that the former is getting calculated by the regular Coq implementation, whilst the latter is getting calculated by the buggy `vm_compute` alternative. vm_compute should give identical results, but faster; but since there's a bug, we can derive a contradiction by mixing correctly-calculated values with incorrectly-calculated values.

How does proving something false as true gives the logic system the ability to prove anything ? Can you explain it with an example

Any statement is either true or false. If we can prove that false is true, then any statement is true.

EDIT: For example: 1+1=3. That's false. We've learnt that false=true, therefore 1+1=3 is true.

I don't think it's that easy. Not every statement is either true or false in Coq, you'd need to accept the law of excluded middle for that.

Reply on news.ycombinator.com