Comment by dhodell | Hacker News Reader

Comment by dhodell | Hacker News Reader

Parent Full thread

Thanks for this.

This seems to be basically what I'm saying through most of the article. Bugs occur because of a gap in a mental model. To fix the gap, we need more understanding. I'm not sure I would say that's necessarily a design or architecture flaw in the software.

Unfortunately, proving things correct in most popular languages is a Very Hard Problem. I do address that to some extent in the article, though. In particular, the sorts of languages that end up being easy to prove correct tend to be difficult for people to learn. Therefore, people are likely to either learn something easier, or they are likely to write code that is "correct" or "safe" but still has logic errors. I think that there are other many valid reasons to write software, and not all of them require correctness to the extent Dijkstra would like.

But I think that's a pipe dream anyway. For one, most software is not written in formally verifiable languages, or formally verifiable dialects of popular languages. Porting all software would be impossible. Second, who defines "correct"? What about bug-compatible software, where the definition of correct is imitating something else that is known to be incorrect? What about ambiguity in specifications like JSON, or undefined behavior in C (some of which can only be detected at runtime, because we don't actually have infinite tape in our Turing machines)?

What happens when there's a bug in the runtime of your formally verifiable language? What happens when there's a hardware bug? I'm not saying these are necessarily common, but regardless of your software environment, you're running on something else that can have the same bugs. People make mistakes, even when proving things. Math is great, but people make mistakes, and our tools are still bounded by the laws of physics.

No matter which way I look at this thing, I keep coming back to teaching and understanding as the only generalizable and approachable ways to address the problems bugs. (Whether that approach is taken by proving correctness of some implementation, or post-hoc with testing and tools.)

Thanks for a great and insightful article and answer. Views like yours should be shared by a wider audience, since it accentuates a section of software engineering that is rarely discussed: understanding and adjusting the mental model of programming (or should I say: systems design?)

Applying formal methods does not automatically entail that a system is proven to be correct, which would be an exaggeration. Proponents of formal methods believe it helps to ascertain certain robustness and reliability aspects of a system. For example, I could prove a Paxos implementation correct, given the specification of a Paxos algorithm, but still use it incorrectly in a larger system, or vice versa.

Correctness is a rather vague and abstract concept and quite distinct from proof. Using a type system, we could prove that, given certain pre-conditions, large state-spaces cannot be visited. Whether it will behave correctly within the reduced state-space, the programmer can only hope. Even formal languages such as Coq rely on correct execution of the assembler, CPU and system environment.

I think what Dijkstra was aiming for was not a replacement, but more a grounds-up reeducation of the field. And to a certain extent this is currently happening. Functional languages and techniques are everywhere. I hear people talk about monads, monoids and functors, others embrace reactive programming, which is the coinductive branch of programming. Coq and Idris are finally reaching a larger audience (but still small). However, the larger change is slow and requires a generational paradigm shift.

It is exactly the thing you are addressing in your article: do the users of a tool believe they are changeable and changed by the tool (Heidegger)? If they do, they also understand the need for self-protection and focus.

Teaching and understanding are indeed the underlying pillars if we want to bring software engineering to a higher level. I think the order in which material is taught greatly influences the mental model of the student. Making multiple iterations, one could start with concepts from category theory and work down with for example Coq, Haskell, LLVM / Assembler, Machine Language/system design, CPU Micro-ops to Digital Electronics. This would lead to view the concept of an LLVM as an implementation artefact of Haskell (which in itself can be expanded to other languages). The mental map becomes relatively machine and system independent. Unfortunately, most programmers nowadays start with an easy language that gives instant reward. It is made difficult for the aspiring programmer in this position to understand the concessions made.

Thanks for clarifying, I agree with all of this, and they're great points!

Reply on news.ycombinator.com