1. 29

  2. 24

    The way I’ve heard a similar sentiment expressed before is:

    You can have a program with obviously no bugs, or you can have a program with no obvious bugs.

    1. 25

      It’s from Tony Hoare’s 1980 Turing Award Lecture:

      There are two ways of constructing a software design: One way is to make it so simple that there are obviously no deficiencies, and the other way is to make it so complicated that there are no obvious deficiencies. The first method is far more difficult. It demands the same skill, devotion, insight, and even inspiration as the discovery of the simple physical laws which underlie the complex phenomena of nature.

    2. 11

      If we have correctness but not readability, that means a functional program that’s hard to understand. It’s likely we’ll introduce a bug. Then we’ll have a buggy program that’s hard to understand. It’ll probably stay that way.

      If you focus on correctness you’ll have tools so that you don’t introduce a bug.

      1. 7

        Also, I have seen a lot of evidence that correctness produces readability.

        1. 5

          A common effect in high-assurance security in old days was formal specifications catching errors without formal proofs. The provers were too basic to handle the specs and programs of the time. The specs had to be simplified a lot for the provers. Yet, even if they didn’t do proofs, they found that simplification step caught errors by itself. Proofs had varying levels of helpfulness but that technique consistently found bugs.

          So, yeah, it’s easier to show something is correct when it’s simple and readable enough for verifier to understand. :)

          1. 4

            Do you think it’s possible that pursuing correctness using the type system can cause less readability? If so, what does that look like? If not, do you draw distinctions between words like “readability” and “accessible”? Or perhaps even more fundamentally, do you see a distinction between correctness and readability at all?

            1. 4

              Do you think it’s possible that pursuing correctness using the type system can cause less readability? If so, what does that look like?

              I know exactly what that looks like. They’re called formal proofs of program correctness. The specs and proofs can be hard to read although the code is usually easy to follow. The trick is, what’s easy for a human to verify is often hard for a machine to check and vice versa. So, machine-checked code might get uglier than human-checked code depending on the algorithm.

              1. 4

                Sure, that’s one extreme end of things. What if we back away from formal proofs and consider other things that are less obvious? For example, is it always true that adding a single additional type—which perhaps seals an invariant you care about—always leads to more readable code? What about two types? Is there a point at which N additional types actually hampers readability even if it makes certain bugs impossible at compile time than could be achieved with N-1 types?

                (Perhaps if I constructed an example that would make this a bit more concrete. But I worry that the example will tempt us too quickly into red herrings.)

                1. 4

                  Some people already say that looking at Ada, ATS or Idris code but usually amateurs in the language. I think the easiest example of correct, hard-to-read code is finite state machines. You can do whole programs as Interacting, State Machines. They’re usually compact, easier to verify, and easy to optimize. Many programmers cant read them, though, because they regularly use or even understand FSM’s.

                  1. 4

                    In a lot of “proofy” languages, proofs take the form of types, and the line between “normal” types and proofs is blurry/nonexistent. So strictly speaking, “proofs can hurt readability” and “types can hurt readability” mean the same thing. Pedantry aside, look at C++: unreadable clever template types are a cottage industry.

            2. 3

              Are there really systems where it’s not possible to introduce a bug? Seems like a pretty hefty claim.

              1. 4

                You can turn (some) would-be-bugs into show-stoppers during the build process. A broken build is very easy to notice. The main difficulty with this approach is that you quickly hit diminishing returns: the amount of effort required to programmatically enforce (parts of) specifications grows much faster than the complexity of the specifications themselves.

                1. 3

                  No. They don’t exist even in high-assurance systems. That’s why most papers in that field are careful to note their Trusted Computing Base (TCB). They say each thing they rely on to work correctly in order for their proven components to work correctly. In the component itself, errors might be introduced in the requirements or specs even if everything else is correct-by-construction from them. If external to the component, it might create interactions with the environment that cause a failure mode that was previously unknown.

                  Just look at the errata sheet of Intel CPU’s if you ever begin to think you know exactly what will happen when a given app executes. There’s a reason Tandem NonStop had multiple CPU’s per process past availability. ;)

                  1. 2

                    If we take it to the extreme and when given appropriate tools, it’s not possible to introduce a bug in the following function:

                    id :: a -> a
                    id a = a

                    There is a single implementation, and you can only compile that function once you have it.

                    The trick is coming up with a specification and translating the specification to whatever tool you’re using. It is possible to specify the wrong thing, which is where validation (rather than verification) is needed.

                    1. 4

                      If we take it to the extreme and when given appropriate tools, it’s not possible to introduce a bug in the following function:

                      Sure it is. Perhaps my intention was to write a function that would square the argument, but I accidentally wrote an overly general and useless function. The hardest bugs to debug (at least, for me) are the ones where I wrote code that correctly does the wrong thing.

                      1. 2

                        I wrote code that correctly does the wrong thing.

                        Is where:

                        validation (rather than verification) is needed

                        1. 3

                          The concept of verification requires a specification. Without a specification a function cannot be correct or incorrect. It might be inconsistent or misleading if for example the function name does not match the behavior.

                          You can argue that the type of a function is a specification and the type checker performs the verification. Unfortunately, nearly all type systems are not powerful enough to express all the specification we desire. Exceptions would be Coq, Isabelle, and other code generating theorem provers.

                          1. 3

                            Obviously it depends on the problem, but a lot of specifications can be quite easily captured in the type system:

                            • Only print HTML-escaped values when outputting HTML
                            • Do not allow any network requests in this block of code
                            • files must be closed at the end of execution
                            • This field is not required

                            I know a lot of specifications are harder to capture, but a good percentage of bugs I encounter in the wild are not the “hard” stuff, but some relatively straightforward stuff that we know how to capture.

                            Of course, at one point the spec becomes a bit of an uphill battle, but I feel like the more interesting exploration happening in “unsafe but really far reaching” type systems like TypeScript will help us build more tools in a safe way but with a larger reach.

                            1. 1

                              Unfortunately, nearly all type systems are not powerful enough to express all the specification we desire.

                              But we can use common tools such as types, parametricity, Fast and Loose Reasoning and property-based testing to specify a lot of things. Not everything - but a lot of things.

                              We should definitely move toward Coq and Isabelle for some systems but it’s also often possible to write bug free software without going all the way there.

                          2. 2

                            Are there any examples that are more likely? I can’t really imagine writing the specification square :: Int -> Int and then implementing it as square n = n without blinking an eye.

                            1. 1

                              In that function, because it applies for all types (id :: a -> a reads, “for all types a, gives an a”), something like squaring the argument is excluded, because not all types have multiplication.

                              This is an example of the overlap between verification and types – in this case we see the degree to which type correctness constrains the implementation.

                      2. 8

                        It’s likely we’ll introduce a bug. Then we’ll have a buggy program that’s hard to understand.

                        So your argument that readability is better is by comparing a program that is readable but not correct to a program that is neither?

                        1. 1

                          I’m not the author of the post, but I imagine the point is not being made about programs where the system checks correctness.

                        2. 6

                          If we have readability but not correctness, that means a buggy program that’s easy to understand.

                          If the program were so easy to understand, the error would have probably not been put into it, right?

                          If we have correctness but not readability

                          The probability of correctly writing a nontrivial program by accident is negligible. If you don’t have a clear and precise description of your program’s design and why it’s correct, it’s safe to assume it isn’t. Of course, this description needn’t be in the program’s source code, but it must be somewhere, right? Because nobody throws away their own hard work so easily.

                          1. 5

                            You could have both as of the 1960’s with Dijkstra’s methods. Cleanroom and Eiffel methods showed it too. Point being these aren’t things that should weight against each other in a general platitude. They’re pretty equivalent in importance and benefit in the general case. Helping one helps the other.

                            1. 6

                              Could you drop a few links that you think would be a good introduction to what you mean?

                              1. 6

                                Dijkstra’s method was building software in hierarchical layers with verification conditions specified in them. Each layer is as independently-testable as possible. Each one then only uses the one below it.


                                Cleanroom was a low-defect, software construction process that used a functional style w/ decomposition into simpler and simpler forms with straight-forward, control flow. It was verified by human eye, argument, tests, or formal methods.


                                Eiffel combined a safer language, OOP, and Design-by-Contract to increase correctness while maintaining readability of code.


                                Logic languages like Prolog were used to go from requirements straight to executable specs with less room for error related to imperative code. Mercury is much improved language at least one company uses for this but here’s a more detailed account from a Prolog company:


                                Finally, DSL’s (esp in 4GL’s) were long used to solve business problems correctly with more readability and productivity than traditional languages. Hintjens at iMatix used them a lot:


                                So, those are where it’s relatively easy to do and adds correctness. I mention a lot more assurance techniques with varying tradeoffs here:


                                1. 2

                                  Thank you so much! I’ve got some reading ahead of me now!

                            2. 3

                              Overall, I find that the premise of the post is true.

                              Programs can be unreadable for several reasons (lousy formatting, bad or no naming conventions, etc.). This makes introducing bugs very easy.

                              Over-engineered code is also a problem. The code might seem well designed at first sight, but you quickly realize that it’s a huge mess and that it’s super hard to understand. Again, introducing a bug in this case is easy.

                              1. 3

                                This was a bit confusing to me. Readability is a very subjective experience. Correctness is much more objective. So it’s very easy to say if a piece of code is correct or not but it’s much harder to say if it’s readable.

                                Instead of readability, I think a measurement of how much information outside of the code I’m reading is needed to understand it. For example, in Ocaml doing Foo.bar x (this applies a function bar which exists in the module Foo to the value x) is pretty easy to grok as long as you know what Foo is. This is how a lot of Ocaml looks where the names of things are bound at compile time rather than run-time. On the other hand, languages like Ruby, Python, and even Java, do almost all binding at run-time. The above code would probably more likely be written as x.bar() in those languages and it’s near impossible to know what code is actually being executed at run-time without knowing a bunch more context. This is why I find Ocaml much more readable than other languages even if the code people write in it can be quite terse. All I have to do is run that code through some automatic indenting software and it becomes easier to read for me. In languages with late binding, all the automatic indenting in the world won’t tell me what is executed.

                                Disclaimer on typeclasses:

                                Haskell is very similar to Ocaml in this regard except for type classes. I don’t have enough experience at scale to know if type classes suffer from the same readability issue that I claim exists for OO languages. Ocaml is likely getting something like type classes in the near future, called modular implicits, and I’m both looking forward to it and nervous that we will enter an age of difficult-to-grok Ocaml code.

                                1. 2

                                  I like the point and want to paraphrase it:

                                  Focusing on making a program readable leads its correctness.

                                  But writing a correct mess is not something we’ll enjoy, so let’s not write any messy code of any kind, this will lead to bugs anyway.

                                  1. 1

                                    Except that the whole point of correctness is that it makes it hard to introduce bugs without getting notified about them. So the problem with correct but unreadable programs isn’t that it’s easy to introduce bugs (it’s not), but rather that it’s hard to make any changes at all until you figure out how to grok it.