Djikstra was wrong! The #1 benefit of formal methods isn’t being able to prove things top to bottom. It’s to be able to do something like this, which is analyze the actual runtime of a program as data. That’s cool, and I could see a million ways to apply it. I want to say that TLC would have to have a better state space representation than dot to do that, but then again as long as its consistent it doesn’t matter so much.
The other thing this makes me think of is how interesting it is that the real-world C++ program favors certain transitions, so in practice many behaviors are unlikely. This is probably closely tied to why some people aren’t interested in formal methods - they’re ok with effectively ignoring unlikely behaviors. Of course, I think it’s an even bigger argument for formal methods, because those are precisely the behaviors that you’re not likely to see in practice until it’s too late. But I’m biased.
I don’t think “we should prove things top to bottom” is a fair characterization of Dijkstra’s thinking. I think he was much more nuanced than that, but broadly speaking, he wanted us to think mathematically about problems rather than treating machines anthropomorphically or operationally. Deriving a program from a formal model I think would have interested him greatly.
Djikstra was wrong! The #1 benefit of formal methods isn’t being able to prove things top to bottom. It’s to be able to do something like this, which is analyze the actual runtime of a program as data. That’s cool, and I could see a million ways to apply it. I want to say that TLC would have to have a better state space representation than
dotto do that, but then again as long as its consistent it doesn’t matter so much.The other thing this makes me think of is how interesting it is that the real-world C++ program favors certain transitions, so in practice many behaviors are unlikely. This is probably closely tied to why some people aren’t interested in formal methods - they’re ok with effectively ignoring unlikely behaviors. Of course, I think it’s an even bigger argument for formal methods, because those are precisely the behaviors that you’re not likely to see in practice until it’s too late. But I’m biased.
I don’t think “we should prove things top to bottom” is a fair characterization of Dijkstra’s thinking. I think he was much more nuanced than that, but broadly speaking, he wanted us to think mathematically about problems rather than treating machines anthropomorphically or operationally. Deriving a program from a formal model I think would have interested him greatly.
I agree wholly with your second paragraph.
That’s definitely true: https://www.cs.utexas.edu/users/EWD/transcriptions/EWD02xx/EWD209A.html
Thank you for this!