5 ms·

> The thing that remains is a very different activity with very different properties. Do you write a correct formal spec the first time round? I don't. Proofs

> The thing that remains is a very different activity with very different properties. Do you write a correct formal spec the first time round? I don't. Proofs sometimes pass or fail when they shouldn't. When these problem occur I call them bugs, and I call process of finding and fixing them debugging.

lmm 7y ago
> When these problem occur I call them bugs, and I call process of finding and fixing them debugging. What do you find it has in common with the activities that we normally call debugging? For me debugging is characteristically about understanding how a system is behaving, essentially by bisecting: it's all about figuring out what should be the case at each point and identifying the point at which things start to go wrong. Whereas correcting a proof is very different: you immediately know where the problem is, and it's more about coming up with a new lemma or strategy - it's the same kind of activity as writing a new proof/program, whereas (traditional) debugging is very much a separate skill, IME.
- oldgradstudent 7y ago
  I view these as very similar. A proof can fail for many reasons, and even in the simplest possible case, where the tool provides you with a counter example it could either be a real bug in the design/program/protocol, but there could also be something wrong with the specification you were given, or in your implementation of the specification, or in some assumptions you've made to simplify the proof, or there's ambiguity in the natural language description, or even some typo somewhere. You now need to understand the domain and the system well enough to come up with an explanation of the phenomena. This is debugging.
  - lmm 7y ago
    But you have access to everything at every stage. There's no need to figure out what the data is or how it got that way - the hard part of debugging - because there is no data, no state, no user input. It's more like fixing a compilation error than debugging.

lmm 7y ago

> When these problem occur I call them bugs, and I call process of finding and fixing them debugging. What do you find it has in common with the activities that we normally call debugging? For me debugging is characteristically about understanding how a system is behaving, essentially by bisecting: it's all about figuring out what should be the case at each point and identifying the point at which things start to go wrong. Whereas correcting a proof is very different: you immediately know where the problem is, and it's more about coming up with a new lemma or strategy - it's the same kind of activity as writing a new proof/program, whereas (traditional) debugging is very much a separate skill, IME.

oldgradstudent 7y ago
I view these as very similar. A proof can fail for many reasons, and even in the simplest possible case, where the tool provides you with a counter example it could either be a real bug in the design/program/protocol, but there could also be something wrong with the specification you were given, or in your implementation of the specification, or in some assumptions you've made to simplify the proof, or there's ambiguity in the natural language description, or even some typo somewhere. You now need to understand the domain and the system well enough to come up with an explanation of the phenomena. This is debugging.
- lmm 7y ago
  But you have access to everything at every stage. There's no need to figure out what the data is or how it got that way - the hard part of debugging - because there is no data, no state, no user input. It's more like fixing a compilation error than debugging.