”formal proof methods do not guarantee that the code you've written is bug free. They only guarantee that the code follows the requirements you defined given the conditions you also set on your inputs.”
I think you are mixing “bug” with “out of spec”. If you ask me to write a perfect chess program, you can’t say it’s a bug if it can’t play go.
Bad or incomplete requirements are a problem, but that’s a different problem from “bugs”.
People often use the term "bug" in a more broad sense to mean "the system is behaving in an unexpected or undesirable manner". The "spec" may have not even covered the issue in question -- no one thought of that edge case.
Either way, for Coq programs, it sounds to me like specifying the preconditions is part of the implementation, so the term "bug" seems especially apt
I think you are mixing “bug” with “out of spec”. If you ask me to write a perfect chess program, you can’t say it’s a bug if it can’t play go.
Bad or incomplete requirements are a problem, but that’s a different problem from “bugs”.