7 ms·

I’ve read a lot from Djikstra, but never this one. After giving it a read, it’s one of his most concise summaries of his overall philosophy. If he’s wrong about

I’ve read a lot from Djikstra, but never this one. After giving it a read, it’s one of his most concise summaries of his overall philosophy. If he’s wrong about anything, it’s how formal methods are not up to speed with the scale of software that we want to build, and that I believe we can never get away from operational reasoning. I’ve been keeping a bug journal for some time now. It’s very enlightening because instead of making things up, I have raw data about what goes wrong at work, for me. For me, logic errors account for probably 40% of bugs. Another 40% are operational problems, mostly performance related. The rest are typos and unintentional breakages of parts of the program that are unknowingly coupled to something I changed. All that being said, even when he’s wrong, he’s right. Logical soundness must come first. This cannot be done without math. All programmers are doing math whether they acknowledge it or not, specifically mathematical logic and set theory. Refactors to improve performance must keep the logical function of the program the same. I believe him wholeheartedly when he says: > The statement that a given program meets a certain specification amounts to a statement about all computations that could take place under control of that given program. And since this set of computations is defined by the given program, our recent moral says: deal with all computations possible under control of a given program by ignoring them and working with the program. We must learn to work with program texts while (temporarily) ignoring that they admit the interpretation of executable code. This man understood computation far more deeply than anyone out there today. Today, we have completely baseless claims being spouted like religion. We are in the era of the personality - a person’s personality determines how much they are listened to in our field. That is tragic, and while Djikstra might not have the answer for software of our scale, he has the only correct point of view in my opinion.

qsort 6y ago
I agree a lot with Dijkstra as well, especially when he denounces how childish it is to compare computational processes with physical ones instead of understanding them for what they are (i.e. 'the radical novelty'), but to play the devil's advocate, formal thinking is not how we learn. I personally find it hard to understand a concept, even in pure math, if I don't understand the motivations that lead to that concept being formulated (not necessarily practical applications, I'm fine with purely theoretical concepts, just why that definition solves a problem, I guess); it's simply too much to ask someone to "get" programming without an intuition of what types of problems it solves. The fact that more and more people get into programming, even professionally, without proper mathematical fundamentals is another topic entirely.
- willtim 6y ago
  I cannot imagine a mathematics lecturer telling his students "a monad is like a burrito". Sometimes I think the analogies can actually hurt our understanding of something very abstract or novel, as is the case with the bad burrito analogy.
  - jcelerier 6y ago
    Maybe if they did more than a few 0.x% of students would succeed at maths.
  - qsort 6y ago
    I completely agree with that but my angle was slightly different. Burrito monads are the prime example of what not to do, but my university course on category theory didn't start with the lecturer throwing out definitions, it started with an explanation in plain English (well, it wasn't English but you get the point :)) of what the theory is trying to accomplish. I'm completely behind the Dijkstrian viewpoint that computing is a radical novelty in itself, but I don't see why trying to explain the purpose of what you are doing is bad. To make a more low-level example, pretty much every explanation ever of the concept of R-module started with 'we are trying to generalize the concept of a vector space to sets that have a ring structure but not a field structure', not 'here, have a bunch of axioms'.
    - willtim 6y ago
      I completely agree. There should be motivating problems and examples. But I don't think that's at odds with Dijkstra's viewpoint?
  - sriku 6y ago
    We can certainly dispense with analogies that only serve as memory aids.
  - jancsika 6y ago
    > I cannot imagine a mathematics lecturer telling his students "a monad is like a burrito". Well of course that's fatuous-- a math teacher's job in this case is to explain category theory. It would be professional malpractice for them to use an analogy to justify not teaching category in the interest of teaching practical programming techniques.
deleted 6y ago
[deleted]
aryehof 6y ago
> “Logical soundness must come first. This cannot be done without math.” I’ve long had this (mistaken?) belief that formal methods and mathermatics do not primarily apply to the areas of computing I’m involved with. I am involved with business systems that are primarily concerned with the recording of activities. Those activities relate to thing/s, and often involve people and places acting in some role (context). In some ways I am modeling interactions between phenomena, together with the concepts through which they are abstracted. Consider for example a payroll system or a airline reservation system. How can formal methods and mathematics help in this?
- naringas 6y ago
  they can help you avoid malformed requirements. and/or preempt situations such as "oops your reservation has vanished because a bug; but now thanks to your complaint we've fixed it!"
- tel 6y ago
  These systems are in one sense ideal for formal methods: they're complex interactions between systems, often coordinating over resources and time, with many easily identified constraints that must be maintained. On the other hand, they're awful for formal methods to the tune of how expensive and valuable it is to actually get a complete description of what the intended behavior of these systems even is. The bane of application of formal methods in software is that many practical automated systems are only intended to perform against an incomplete, often somewhat inconsistent, and often rapidly changing goal specification. They could be leveraged very fruitfully against these problems, but to do so would invite a long, expensive requirements gathering process between modelers and business owners. There's some anecdotal evidence that this is a valuable process, but the economics don't work out. Even in circumstances where the benefit is obviously there, formal methods front load cost and thus increase delivery risk in many projects. I think the right way of bringing these techniques to practical software is through expansion "horseback formal methods": lightweight semi-formal tooling and practice which pays out moderate value for moderate investment. These techniques could be run earlier on in a project and demonstrate the value of formal methods while reducing the eventual cost of implementing the heavy hitting tools later on. A lot of software engineers practice this already, but don't always have the experience to connect back-of-the-envelope domain modeling to mathematical modeling. Or don't find it sufficiently valuable, which is fair. Hopefully, expansion of popularity in these methods will increase the popularity of making smoother transitions from lightweight modeling to more expensive, formal, comprehensive modeling.

qsort 6y ago

I agree a lot with Dijkstra as well, especially when he denounces how childish it is to compare computational processes with physical ones instead of understanding them for what they are (i.e. 'the radical novelty'), but to play the devil's advocate, formal thinking is not how we learn. I personally find it hard to understand a concept, even in pure math, if I don't understand the motivations that lead to that concept being formulated (not necessarily practical applications, I'm fine with purely theoretical concepts, just why that definition solves a problem, I guess); it's simply too much to ask someone to "get" programming without an intuition of what types of problems it solves. The fact that more and more people get into programming, even professionally, without proper mathematical fundamentals is another topic entirely.

willtim 6y ago
I cannot imagine a mathematics lecturer telling his students "a monad is like a burrito". Sometimes I think the analogies can actually hurt our understanding of something very abstract or novel, as is the case with the bad burrito analogy.
- jcelerier 6y ago
  Maybe if they did more than a few 0.x% of students would succeed at maths.
- qsort 6y ago
  I completely agree with that but my angle was slightly different. Burrito monads are the prime example of what not to do, but my university course on category theory didn't start with the lecturer throwing out definitions, it started with an explanation in plain English (well, it wasn't English but you get the point :)) of what the theory is trying to accomplish. I'm completely behind the Dijkstrian viewpoint that computing is a radical novelty in itself, but I don't see why trying to explain the purpose of what you are doing is bad. To make a more low-level example, pretty much every explanation ever of the concept of R-module started with 'we are trying to generalize the concept of a vector space to sets that have a ring structure but not a field structure', not 'here, have a bunch of axioms'.
  - willtim 6y ago
    I completely agree. There should be motivating problems and examples. But I don't think that's at odds with Dijkstra's viewpoint?
- sriku 6y ago
  We can certainly dispense with analogies that only serve as memory aids.
- jancsika 6y ago
  > I cannot imagine a mathematics lecturer telling his students "a monad is like a burrito". Well of course that's fatuous-- a math teacher's job in this case is to explain category theory. It would be professional malpractice for them to use an analogy to justify not teaching category in the interest of teaching practical programming techniques.

deleted 6y ago

[deleted]

aryehof 6y ago

> “Logical soundness must come first. This cannot be done without math.” I’ve long had this (mistaken?) belief that formal methods and mathermatics do not primarily apply to the areas of computing I’m involved with. I am involved with business systems that are primarily concerned with the recording of activities. Those activities relate to thing/s, and often involve people and places acting in some role (context). In some ways I am modeling interactions between phenomena, together with the concepts through which they are abstracted. Consider for example a payroll system or a airline reservation system. How can formal methods and mathematics help in this?

naringas 6y ago
they can help you avoid malformed requirements. and/or preempt situations such as "oops your reservation has vanished because a bug; but now thanks to your complaint we've fixed it!"
tel 6y ago
These systems are in one sense ideal for formal methods: they're complex interactions between systems, often coordinating over resources and time, with many easily identified constraints that must be maintained. On the other hand, they're awful for formal methods to the tune of how expensive and valuable it is to actually get a complete description of what the intended behavior of these systems even is. The bane of application of formal methods in software is that many practical automated systems are only intended to perform against an incomplete, often somewhat inconsistent, and often rapidly changing goal specification. They could be leveraged very fruitfully against these problems, but to do so would invite a long, expensive requirements gathering process between modelers and business owners. There's some anecdotal evidence that this is a valuable process, but the economics don't work out. Even in circumstances where the benefit is obviously there, formal methods front load cost and thus increase delivery risk in many projects. I think the right way of bringing these techniques to practical software is through expansion "horseback formal methods": lightweight semi-formal tooling and practice which pays out moderate value for moderate investment. These techniques could be run earlier on in a project and demonstrate the value of formal methods while reducing the eventual cost of implementing the heavy hitting tools later on. A lot of software engineers practice this already, but don't always have the experience to connect back-of-the-envelope domain modeling to mathematical modeling. Or don't find it sufficiently valuable, which is fair. Hopefully, expansion of popularity in these methods will increase the popularity of making smoother transitions from lightweight modeling to more expensive, formal, comprehensive modeling.