[yogthos]

In Coq your proof is your program, and if you end up proving the wrong thing that's a bug in the program. There's no magic here. Only a human can tell whether the code does what was intended. To do that you have to understand the code.

[antpls]

If you are proving the wrong statement, then you simply didn't state the initial problem correctly, it has nothing to do with a bug in your proof. It's like saying there is a bug in your implementation of a sort function, while we initially asked you to implement a max function. Even if your sort function is correctly implemented, it's still a "bug" to the person who asked you to implement a max function.

[yogthos]

That's my whole point. You're really just pushing the problem as step back instead of solving it. Instead of worrying about bugs in your implementation, you're now worrying about bugs in your specification.

[kazinator]

Problem is that these proofs are not the specification. They are very detailed. Specification says "write me a sort function", and the proof is some gobbledygook that deal with irrelevant minutiae of the sorting implementation. Where is the proof which proves that that proof matches the specification?

[antpls]

A theorem prover let you prove that your code is bug free in some cases. Why not use a theorem prover for your specifications too?

[yogthos]

Because only a human can decide whether the specification matches the intent. This is not a hard concept. The machine can only tell you that your specification is self-consistent, not that it's specifying what you wanted.

[antpls]

The machine could go a level above and helps the human to reflect about its intents. That would basically be a machine convincing the human he/she is already happy right now, and he/she doesn't need to earn more money, and therefore doesn't need that "new e-commerce website". An artificial psychologist conversational agent would help you know about what you really want in life :)

[yogthos]

:)