[pdonis]

> Dijkstra wanted us to think on paper, use abstractions that accurately describe real-world systems, and arrive at answers methodically with a trail of checkable work. If our data and methods are sound our answers will always be correct.

I understand the aspiration, but I always think of the counterpoint implicit in Knuth's famous statement: "Beware of bugs in the above code; I have only proved it correct, not tried it."

[bitwize]

The point is, if a system's behavior can be characterized with a set of equations, use the equations to talk about the behavior -- not a flawed metaphor for human cognition. If you find out that your equations incorrectly or incompletely characterize the system's behavior, Occam's razor requires you to assume that what you need is a better set of equations.

[pdonis]

> if a system's behavior can be characterized with a set of equations, use the equations to talk about the behavior

I agree, and I don't think Knuth's quote was saying anything different.

> If you find out that your equations incorrectly or incompletely characterize the system's behavior, Occam's razor requires you to assume that what you need is a better set of equations.

Yes, but you might not have them, and they might not be easy to find. So you might have to face the fact that, now and for the foreseeable future, you might not be able to use your equations to completely predict or characterize the system's behavior, so you need to actually test your code instead of just proving it correct, as Knuth said.

[pdonis]

As a separate point from my other post, characterizing the system's behavior isn't enough. You also need to characterize the requirements that the system is supposed to meet. Even if you have equations for the former, you might not for the latter. So your equations might completely and precisely predict system behavior that turns out not to do what the user actually wants. I think that's part of what Knuth's quote is talking about.