Comment by amw-zero | Hacker News Reader

Comment by amw-zero | Hacker News Reader

Parent Full thread

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.

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.

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.

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'.

I completely agree. There should be motivating problems and examples. But I don't think that's at odds with Dijkstra's viewpoint?

> 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.

If one wants to learn what the Monad abstraction is, then one by definition will have to learn some category theory! I don't think there is any need to understand what a monad is in order to use any practical programming language. My point was that the burrito analogy does more harm than good (as predicted by Dijkstra).

> If one wants to learn what the Monad abstraction is, then one by definition will have to learn some category theory!

Actually, I always thought people were referring to Doug Crockford's talk about monads where he makes an offhand analogy to burritos at the beginning. In that talk the analogy has absolutely nothing to do with the 45 minutes of slides he presents, so it always struck me as weird. I had no idea bloggers had actually used a burrito analogy to explain monads-- I now realize he was making an allusion to that.

At any rate, in his talk he explicitly avoids both category theory and type theory in an attempt to explain monads to Javascript programmers for practical programming purposes.

We can certainly dispense with analogies that only serve as memory aids.

Maybe if they did more than a few 0.x% of students would succeed at maths.

> formal thinking is not how we learn.

The way I've thought about it is that we cannot understand a problem until we've faced it ourselves.

And too often we try to teach each other by going straight to the answer, and then it just doesn't stick.

I recall this happened to me when reading about 'soft' skills (such as collaboration methodologies), it wasn't until I was working with a team of people at a job and was faced with the problems these methodologies attempt to solve that I was able to read about them without immediately thinking "this sounds like bullshit"

I think this is part of why the "Learn X the hard way" method of teaching can be so effective. It's forces you to solve a problem with foundational tools.

> “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?

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.

Agreed on lightweight formal methods. TLA+ and Alloy have been really eye opening to use, and it's almost at no cost. They're just tools for expressing logic and analyzing models.

Even those are very heavyweight to my mind. I’m thinking things as simple as applying semantics to flow charts and making state tables. Exhaustive enumeration of small spaces forms a neat on-ramp to more powerful methods, if we choose to treat them that way.

Many thanks for that. Very thought provoking.

> through expansion "horseback formal methods"

I haven’t heard this terminology before. Any references you can recommend to learn more?

Here "horseback" is a term I'm using to mean "applied in the field, cutting corners as needed to make things valuable now". I'm not sure exactly where I picked it up, but I like the idea.

I'm glad you asked this!

I generally give these business systems the name of "interactive information systems." That's exactly primarily what I work on as well (and I imagine what most people work on, but not all of course).

Maybe counterintuitively, this kind of system is what brought me to math. I kept hearing things like "oh this is just a CRUD app" and it's a solved problem - yet we were opening 50 bug tickets per week (and that's not an exaggeration, we have a large application, and we measure our bug intake and report on it every sprint).

So the first place where math can help with this is at the source - the data! I know not everyone is using a relational database, but the relational model of data is firmly based on math. Learning more about set theory explicitly has improved my interactions with our relational DB immensely.

In my experience, I was taught data access through ORMs. Honestly, the relational model is so much simpler and more elegant. I read somewhere that Edgar Codd used to express relational queries using only predicate logic notation, and I imagine that that would be so much simpler than SQL, and certainly more simpler than bloated ORM code.

On the query front, we like to treat the database as an implementation detail, but I find that this is not practical. Practically, lots of domain logic has to live in queries. I have had 2 bugs recently where a query itself was not returning the right data. Improving my formal reasoning via sets and predicate logic has improved my querying immensely.

Thanks for the great response!

I may be wrong, but it seems your design architecture is similar to “structured design”. Where you model data, and alongside that the transformations to be performed on that data. Traditionally this might have been documented using entity-relationship and dataflow diagrams.

In our case, we model our complex business problem domain using an object model independent of persistence and any particular user/system interaction. Perhaps unusually for these days, we also model the many constraints (business rules) within the object model.

Given that the nature of our domain model is not based on transformations that I guess are more easily quantified (or as Dijksta would say “calculated”), I’m still unsure that formal methods would apply or bring any benefits to us at large, other than perhaps some areas of specific behavior?

Build DSLs with Decision Tables in collaboration with your stakeholders/clients.

Look into the works of Markus Voelter : https://voelter.de/ and https://medium.com/@markusvoelter There is also an implementation of the ideas at http://mbeddr.com/

You might also find the book; The Decision Model: A Business Logic Framework Linking Business and Technology useful.

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!"

Reply on news.ycombinator.com