Comment by begriffs | Hacker News Reader

Comment by begriffs | Hacker News Reader

Parent Full thread

Reminds me of what Edsger Dijkstra wrote, "Let me start with a well-established fact: by and large the programming community displays a very ambivalent attitude towards the problem of program correctness. A major part of the average programmer's activity is devoted to debugging, and from this observation we may conclude that the correctness of his programs —or should we say: their patent incorrectness?— is for him a matter of considerable concern. I claim that a programmer has only done a decent job when his program is flawless and not when his program is functioning properly only most of the time. But I have had plenty of opportunity to observe that this suggestion is repulsive to many professional programmers: they object to it violently! Apparently, many programmers derive the major part of their intellectual satisfaction and professional excitement from not quite understanding what they are doing. In this streamlined age, one of our most under-nourished psychological needs is the craving for Black Magic, and apparently the automatic computer can satisfy this need for the professional software engineers, who are secretly enthralled by the gigantic risks they take in their daring irresponsibility. They revel in the puzzles posed by the task of debugging. They defend —by appealing to all sorts of supposed Laws of Nature— the right of existence of their program bugs, because they are so attached to them: without the bugs, they feel, programming would no longer be what is used to be! (In the latter feeling I think —if I may say so— that they are quite correct.)" -- From EWD288

IIRC Dijkstra advocated constructing a proof of your program first. This also involves debugging, mistakes and trial-and-error, just at a different level. Mathematical representations and proofs are powerful because general and certain; but they aren't magic and don't write themselves.

It's a lot easier - and a lot more fun - to deal with specific instances, that are concrete, and can be examined and experimented with on a computer.

Logically, one could also work with proofs with a computer to give the same benefits (e.g. coq proof assistant), but for some reason, it doesn't seem to be as much fun in practice. Perhaps because the abstract versions don't have a direct impact; they aren't "live" (idk).

There is an entire field of CS research on this topic, commonly referred to as formal verification. Some programs are written this way.

Yup and I had to take two modules on it for my degree. I've never encountered anything so dull in my life! [That was probably because the material was presented in such a dry way, I'm pretty sure anything can be interesting if someone with passion is also a skilled presenter]

It's definitely the presentation. I also studied formal verification in my second year and used it as an opportunity to catch up on missed sleep.

However, the third year I studied how to formally define programming languages and really enjoyed it. It was all about delivery.

I think class size has an effect too - it's much easier to engage with smaller classes. The second year module was mandatory, whereas the third year module was optional.

That's quite sad: Formal methods should be one of the more exciting topics in your CS programme. Hope they didn't scar you too badly.

>Apparently, many programmers derive the major part of their intellectual satisfaction and professional excitement from not quite understanding what they are doing.

This is one of my favorites remarks from Dijkstra, but I found it in a video interview with him. I had no idea there's more context to this. Thanks!

Next, tell us why goto is bad.

It's not necessarily bad, for example, see how it's used on the linux kernel (+/- like an exception handler)

But of course, having a mess is bad and goto makes it really easy

GOTO http://stackoverflow.com/a/52307

Humor in programming considered hardful.

Deleted comment

It's interesting that the author wrote the article ironically, but that it still kind of resonates with what Dijkstra observed. Every joke has a kernel of truth.

Reply on news.ycombinator.com