3 ms·

but writing large async web projects with a lot of UI & network communication... by all means you want to think about how to cover all your bases, but proving t

but writing large async web projects with a lot of UI & network communication... by all means you want to think about how to cover all your bases, but proving things mathematically about that kind of code isn't realistic or practical, if it ever was. When you are writing async code, it's more important than ever to try to think with the proving mindset, and at least consider in your mind why you won't get deadlocks or race conditions. It's more important in async conditions because you have no chance of finding all the deadlocks and race conditions through testing alone. (Also, you misunderstood Dijkstra's approach. He didn't prove all his code, nor did he teach people to do that. He merely wanted them to have the mindset of trying to think of everything that can go wrong).

dahart 10y ago
Upvoted because I agree with everything you said. Except the part about me misunderstanding. You don't have to claim I'm wrong to make your own point, I did read the essay. It makes me smile that you phrased it as a disagreement and said I misunderstood, but then you repeated back to me the same point I made: you want to think about how to cover all your bases. And my larger point still stands - Dijkstra's quote is anachronistic. Having a mindset of trying to think of everything that can go wrong can no longer in today's world be done without debugging or by "not introducing bugs to start with". That used to be possible with a proving mindset, but it's not anymore. A proving mindset is still valuable, but testing and debugging is now invaluable because we rely more than ever before on software we didn't write. Nobody can reason conclusively about async software that relies on dozens of npm projects. * edit: I just thought of a better way to state what I mean: Having a proving mindset in a modern development environment means debugging and testing. The only way to cover all your bases and prove your code in all cases these days is to run it in all cases. I'd never trust someone who claimed they proved their code in advance and didn't need to debug it because they don't write bugs in the first place. If someone said that to me today, it would be a like saying out loud that they have the exact opposite of a proving mindset, and then I'd prove it by running the code and finding the bugs.
- ktRolster 10y ago
  Except the part about me misunderstanding. Hmmmmm let try to understand what you are saying better then. Nobody can reason conclusively about async software that relies on dozens of npm projects Indeed, as we've seen, a single simple dependency can break a lot of things, and in general it's not practical to go through all the dependencies in npm and make sure they are ok. And my larger point still stands - Dijkstra's quote is anachronistic "not introducing bugs to start with" Dijkstra (especially after "goto considered harmful") had a habit of making hyperbolic quotes that didn't match what he actually believed. To understand what he actually believed, and what he actually did in his own programs, it's necessary to dig deeper. Fortunately Dijkstra wrote a lot, and he wrote a text book which he used to teach beginning programmers the 'ideal' way to program. In his textbook, it's true, he began by teaching students how to prove program correctness. However, he quickly moved on from that, at one point saying, "we gain nothing here by going through the work of proving this program correct." In other words, he was not trying to tell everyone to program by proof, nor did he do it in his own work; rather, he wanted people to have the proving mindset (as opposed to the "hey, it works, ship it!" mindset). Dijkstra was aware of Knuth's famous quote, "Be careful about using the following code — I've only proven that it works, I haven't tested it." In the OP I tried to show that all three of these programmers have that mindset, but it manifests in strikingly different ways. There are many techniques that can be used, but the underlying principal is the same for all of them. And I think you will agree that NPM is just crying out for a little more formality :)
  - dahart 10y ago
    > Dijkstra had a habit of making hyperbolic quotes that didn't match what he actually believed. Then maybe we've learned that choosing to use hyperbolic quotes for blog posts can lead to unnecessary disagreement, or perhaps in our case, violent agreement? ;) > And I think you will agree that NPM is just crying out for a little more formality :) Oh hell yes, and how.
    - ktRolster 10y ago
      >or perhaps in our case, violent agreement? The best kind of agreement :) I updated the essay to hopefully make it more clear, as a result of our discussion.

dahart 10y ago

Upvoted because I agree with everything you said. Except the part about me misunderstanding. You don't have to claim I'm wrong to make your own point, I did read the essay. It makes me smile that you phrased it as a disagreement and said I misunderstood, but then you repeated back to me the same point I made: you want to think about how to cover all your bases. And my larger point still stands - Dijkstra's quote is anachronistic. Having a mindset of trying to think of everything that can go wrong can no longer in today's world be done without debugging or by "not introducing bugs to start with". That used to be possible with a proving mindset, but it's not anymore. A proving mindset is still valuable, but testing and debugging is now invaluable because we rely more than ever before on software we didn't write. Nobody can reason conclusively about async software that relies on dozens of npm projects. * edit: I just thought of a better way to state what I mean: Having a proving mindset in a modern development environment means debugging and testing. The only way to cover all your bases and prove your code in all cases these days is to run it in all cases. I'd never trust someone who claimed they proved their code in advance and didn't need to debug it because they don't write bugs in the first place. If someone said that to me today, it would be a like saying out loud that they have the exact opposite of a proving mindset, and then I'd prove it by running the code and finding the bugs.

ktRolster 10y ago
Except the part about me misunderstanding. Hmmmmm let try to understand what you are saying better then. Nobody can reason conclusively about async software that relies on dozens of npm projects Indeed, as we've seen, a single simple dependency can break a lot of things, and in general it's not practical to go through all the dependencies in npm and make sure they are ok. And my larger point still stands - Dijkstra's quote is anachronistic "not introducing bugs to start with" Dijkstra (especially after "goto considered harmful") had a habit of making hyperbolic quotes that didn't match what he actually believed. To understand what he actually believed, and what he actually did in his own programs, it's necessary to dig deeper. Fortunately Dijkstra wrote a lot, and he wrote a text book which he used to teach beginning programmers the 'ideal' way to program. In his textbook, it's true, he began by teaching students how to prove program correctness. However, he quickly moved on from that, at one point saying, "we gain nothing here by going through the work of proving this program correct." In other words, he was not trying to tell everyone to program by proof, nor did he do it in his own work; rather, he wanted people to have the proving mindset (as opposed to the "hey, it works, ship it!" mindset). Dijkstra was aware of Knuth's famous quote, "Be careful about using the following code — I've only proven that it works, I haven't tested it." In the OP I tried to show that all three of these programmers have that mindset, but it manifests in strikingly different ways. There are many techniques that can be used, but the underlying principal is the same for all of them. And I think you will agree that NPM is just crying out for a little more formality :)
- dahart 10y ago
  > Dijkstra had a habit of making hyperbolic quotes that didn't match what he actually believed. Then maybe we've learned that choosing to use hyperbolic quotes for blog posts can lead to unnecessary disagreement, or perhaps in our case, violent agreement? ;) > And I think you will agree that NPM is just crying out for a little more formality :) Oh hell yes, and how.
  - ktRolster 10y ago
    >or perhaps in our case, violent agreement? The best kind of agreement :) I updated the essay to hopefully make it more clear, as a result of our discussion.