How ignorant am I, and how do I formally specify that in my code?

(written by lawrence krubner, however indented passages are often quotes). You can contact lawrence at: lawrence@krubner.com, or follow me on Twitter.

On most projects, as time goes by, you understand the problems better and better, and you understand the solutions better and better, and so you move from ignorance to Enlightenment. Is there a way to formally document this within one’s code? Doing so would offer the best kind of documentation, one immediately relevant and clear. The easiest way to do this is to write code assertions about what one expects the inputs and outputs of a function to be. I offer examples below.

For decades, computer programmers have argued with each other over the issue of strict data-type enforcement, versus dynamic data-type unenforcement. And after 16 years of computer programming, I have come down firmly in the middle: I like optional typing.

In computer programming, the static type advocates wear a perpetual sneer, claiming that many problems in programming would be solved if only we adopted their approach. And yet, many languages are statically typed, and software written with those languages continue to have a large number of bugs (for example, think of any open source Java project over time). So clearly, static typing does not get us to Nirvana.

The most obvious argument against static typing is that it claims a level of confidence that it can not possibly have. Developers using static typing specify all types at the beginning of their project, before they have learned anything about the problem they need to solve. The advocates of static typing will make the counter-argument that it is easy to change types as one learns more about the problem. But I would assert that it is misleading to pretend that you understand the system at the beginning. I want to be honest about how ignorant I am when I begin to work on a problem that I have never encountered before, I think such honesty communicates something important to everyone else attached to the project, including the junior level developers, and also the project managers.

All the same, I have struggled to explain what I see as the advantages of dynamic typing. And this article, by Mark Tarver, does a good job of getting at part of the truth:

I have the strange feeling that types hampers programmer’s
creativity.

The italic sentence is a compact summary of the reluctance that programmers often feel in migrating to statically typed languages – that they are losing something, a degree of freedom that the writer identifies as hampering creativity.

Is this true? I will argue, to a degree – yes. A type checker for a functional language is in essence, an inference engine; that is to say, it is the machine embodiment of some formal system of proof. What we know, and have known since Godel’s incompleteness proof [9] [11], is that the human ability to recognise truth transcends our ability to capture it formally. In computing terms our ability to recognise something as correct predates and can transcend our attempt to formalise the logic of our program. Type checkers are not smarter than human programmers, they are simply faster and more reliable, and our willingness to be subjugated to them arises from a motivation to ensure our programs work.

That said, not all type checkers are equal. The more rudimentary and limited our formal system, the more we may have to compromise on our natural coding impulses. A powerful type system and inference engine can mitigate the constraints placed on what the above writer terms our creativity. At the same time a sophisticated system makes more demands of the programmer in terms of understanding. The invitation of adding types was thus taken up by myself, and the journey to making this program type secure in Shen emphasises the conclusion in this paragraph

Mark Tarver has developed an optional type system that is Turing Complete. It is worth studying, because it is an highly sophisticated approach to formalizing one’s early ignorance, as well as one’s increasing Enlightenment. He invented the Shen computer programming language to demonstrate his research.

However, his research is not yet mainstream, and perhaps not yet ready for widespread commercial use. So I use a much simple technique.

The war between static-type advocates and dynamic type advocates tends to be unrelenting — programmers prefer one style or the other, never both. And yet, as I work on a project, I will add in type information to each function, as soon as I feel sure of it. Advocates of static typing, when they see this, laugh with contempt, and claim that I am creating a broken, ad-hoc, pseudo type system. Why does this approach feel like the right way to go for me?

I have a new theory about the 2 types of programmers:

1.) one group of programmers are willing to start off by saying “This is the truth”. As they get new information, they will change their definition of what is true, but at any given time they will insist on having a complete statement of what they think is true. These are the people who love static typing.

2.) the other group of programmers start off saying “There is a great deal that I do not know about this particular problem, and I am unwilling to commit myself to absolute statements of truth, while I’m still groping in the dark.” They proceed with small experiments, watch where they fail, they learn about the problem, they discover the solutions, and they add in type information incrementally, as they feel more confident that they possess a workable solution. These are the dynamic type advocates.

As I said, the easiest way to document one’s ignorance, and one’s growing Enlightenment, is to write code assertions about what one expects the inputs and outputs of a function to be. How thoroughly one asserts truths about the inputs and outputs is an exact measure of how confident one is feeling that one understands the right path forward. There are roughly 3 levels of knowing:

1.) when you start, your functions have no assertions

2.) as you become more confident, you write assertions about each of your inputs, and your final return value. When you’ve written at least one assertion about each input, and the output, you’ve achieved an important milestone

3.) finally, you write assertions that reach deep into the inputs and the outputs. One of your inputs might be a map that holds a vector that must contain at least one map, so you write an assertion that tests exactly this proposition. Some might argue that this violates encapsulation, but my whole point is that you only write this assertion once you are sure that the structure of your data types are no longer going to change. It wouldn’t make sense to do this in a statically typed language, but it is a wise precaution once you want to solidify an architecture written in a dynamic language. And why not use a statically typed language for this? Exactly because these data structures change too much, too often, during the early phase when you are first working out what the architecture should be.

Some simple examples. I’m going to use Clojure, as this allows very easy pre and post conditions. Remember to, the JVM has compilation flags that allow me to strip out all pre and post conditions, so I can use these assertions when I’m first testing a version of the app, and if all seems well, I can then strip out the pre and post conditions and thus benefit from a speed boost.

I might start off with a simple database query such as:

(defn persist-this-item [item]
  (let [item (if (nil? (:created-at item))
               (assoc item :created-at (tyme/current-time-as-datetime))
               item)
        item (assoc item :updated-at (tyme/current-time-as-datetime))
        item (assoc item :_id (ObjectId.))]
    (mc/insert "tma" item)))

As I learn more about what patterns are going to be common for this app, I will add a large number of :pre and :post assertions, forcing the code to check types and data content, such as:

(defn persist-this-item [item]
  {:pre [
         (map? item)
         (= (type (:item-name item)) java.lang.String)
         (= (type (:item-type item)) java.lang.String)
         (if (:created-at item)
           (= (type (:created-at item)) org.joda.time.DateTime)
           true)
         ]}
  (let [item (if (nil? (:created-at item))
               (assoc item :created-at (tyme/current-time-as-datetime))
               item)
        item (assoc item :updated-at (tyme/current-time-as-datetime))
        item (assoc item :_id (ObjectId.))]
    (mc/insert "tma" item)))

This can be considered a kind of “design by contract” — the assertion statements help all future programmers understand how this code is suppose to be used. The assertions are a kind of documentation, and it is automatically up to date (though without a promise of being complete), since you would get errors if an input changed in a manner that violated one of the assertions.

Are the advocates of static typing correct to claim that I am creating a broken, ad-hoc, pseudo type system? That is best thought of as irrelevant. I am documenting what I have learned about my system so far, I am encoding certain patterns that I am sure are true. If you look at my code, after I have worked on a project for a few months, you will see that some of my functions enforce type assertions, and some don’t. Thus you are seeing my exact level of ignorance, and my exact level of certainty. Any function with type assertions is a function I’m sure of, and those functions without type assertions are the ones that I am still figuring out. But if I took a static-typing approach, then every function would specify all of its types from the moment I wrote my first function. If you look at statically typed code, every function has ever type specified, so you have no idea what the programmer is confident about, and where they still feel ignorant; you would not know where I still felt confused, you would not know where I was struggling to come up with a solution, you would not know where I was plagued with doubts. With static typing, I have to pretend to have 100% confidence right from the start. Only with Optional Typing can I correctly communicate where I am certain, and where I have doubts.

I posted the above example to Hacker News and got his response:

I like Clojure, but this looks rather painful.
If you’re dead set on adding type declarations, perhaps you’d be better off with Haskell or something?

and also:

Maybe I’m misunderstanding, but it looks like every time these functions get called, they’re type checking their inputs and outputs? That seems like a waste of resources. Why not just write unit tests that ensure that they will always be called with the types you expect (or fail at an earlier step if not)? Identify the places where there might be ambiguity in something’s type (e.g. when a JSON blob arrives, it might map a key to a list instead of a dictionary, or if a function might return multiple types, etc), and use unit testing to ensure that the type you expect will emerge from those places, or else a failure will occur.

and someone followed up with:

Unit testing cannot prove the absence of bugs and shit happens in spite of their presence. That’s why I still value (good) static type systems. But besides a good static type system that can prove certain properties about the code (and I’m not talking about Java’s type system here), you can also do design by contract [1], which is precisely what @krubner is doing and I find that to be pretty cool.

Well, it would be cooler if the compiler could check those contracts at compile-time and issue some helpful warnings, but at runtime they are still valuable because the code will fail sooner rather than later. Plus you can probably disable them completely, should you experience problems with performance in production.

They also serve as documentation for other developers, documentation that you’re forced to keep in sync. This documentation is not about the actual business logic, that ends up being laid out in tests, but rather about interface specifications and invariants.

So there you have it – testing serves a different purpose.

[1] https://en.wikipedia.org/wiki/Design_by_contract

My own response:

Unit tests have to rely on sample data that you yourself create. For data that truly is 100% generated from within your system, unit tests can be a reasonable approach, but whenever you consume data from outside of your system, then runtime assertions are much more useful, since 3rd party data is constantly changing, which will cause your app to crash for mysterious reasons. If you have unit tests, they will still 100% pass, because they are testing against out-of-date sample data that you created. I had this problem when I was working with the Ticketmaster API, and also, later, the Booking.com API. In both cases, those companies, without warning, decided to change the data structures in their API. Apps consuming those APIs crashed. The unit tests still passed. If there were no runtime assertions then we would have to go through a long and painful process of debugging. But with runtime assertions enabled, testing against the actual APIs of Ticketmaster and Booking.com, we got detailed error messages that told us precisely what had changed.

And again, one can get the compiler to turn off the assert statements, so they don’t run in production. The JVM supports compiler flags that make it easy to strip out the pre and post conditions when you don’t need them. I use the pre and post conditions in development to help with debugging, and they also serve as documentation for future programmers. I sometimes push them to production, when we need to debug a problem that only exists in production.

The person who suggested Haskell was perhaps mislead by seeing only one example. To see the full pattern of my usage, you have to realize that I have type assertions on some function, but not on others. In that way, the assertions make clear which functions I am confident about, and which I am still ignorant about.

[ [ UPDATE 2018-05-12 ] ]

Defending this idea on Hacker News I wrote:

To take a blob of JSON and ram into MongoDB doesn’t reveal much bias. If we later decided “This JSON needs to have, at a minimum, 4 keys, including user_id, import_id, source, and version” then that is the first layer of runtime checks we can add, or type hints, or Schema with Clojure. And that becomes version 1. If we later say “We also need to add created_at and processed_bool” then that becomes version 2. The lack of the 4 keys in version 0 reveals my ignorance, just as the lack of the extra 2 keys reveals my ignorance in version 1. There will always be ignorance, there will always be things I don’t know, the important thing is to make that as explicit as possible. Adding explicit types in version 0 suggests that I have a confidence that I do not have, and in fact, I eagerly wish to communicate the opposite of confidence in that early code. It’s important that I communicate my ignorance, so that others can see exactly what progress I am making towards Enlightenment.

[ [ UPDATE 2019-09-05 ] ]

See “I test in prod” which offers this list of things which might be different in production, relative to your testing environment:

Many concurrent connections

A specific network stack with specific tunables, firmware, and NICs

Iffy or nonexistent serializability within a connection

Race conditions

Services loosely coupled over networks

Network flakiness

Ephemeral runtimes

Specific CPUs and their bugs; multiprocessors

Specific hardware RAM and memory bugs

Specific distro, kernel, and OS versions

Specific library versions for all dependencies

Build environment

Deployment code and process

Runtime restarts

Cache hits or misses

Specific containers or VMs and their bugs

Specific schedulers and their quirks

Clients with their own specific back-offs, retries, and time-outs

The internet at large

Specific times of day, week, month, year, and decade

Noisy neighbors

Thundering herds

Queues

Human operators and debuggers

Environment settings

Deaths, trials, and other real-world events

Source