https://typesanitizer.com/blog/6-programmers.html * * About * Blog (RSS) Six programmers and the type system Not so long ago, six programmers worked at a tech company in the valley. Each had been programming for many years using a particular dynamically typed programming language. Since the codebase was basically written in the one language that they all were familiar with, they had to imagine what programming in a statically typed language was like. They would sometimes attend conferences and hear speakers talk about it, and they were curious to learn what the programming experience was really like. They had heard that statically type systems could solve complex math problems, drive large performance improvements, and aid working with hundreds to thousands of other programmers on humongous codebases. But they also knew that statically typed languages were used for teaching programming to students at universities. They wondered, how could professors let students use such complex languages at the start of their programming journey? The programmers argued over lunch and over coffee breaks. "Programming with static type systems must let you prove very complex properties of programs," claimed the first programmer. He had heard stories about formally verified software such as kernels and compilers. "No, you must be wrong," argued the second programmer. "A static type system is there to provide additional linting-like checks which give you red squiggles in the editor, so as to help students learn." "You're wrong! I have heard that a static type system can be used to model domain entities and their relationships such as hierarchies, possibilities and so on," said the third programmer. "Please," said the fourth programmer. "You are all mistaken. A static type system is nothing more than some machine-checked documentation. This is a number, that's a string, that's all. You know how people exaggerate. We already have documentation comments for that today." "I am sure that a static type system is pretty magical," said the fifth programmer. "I've heard about programmers enforcing various kinds of invariants through the type system, removing certain classes of bugs by design." "I don't believe static type systems exist at all," declared the sixth programmer. "I think we are the victims of a silly joke. After all, when you get some JSON from the wire, the data you get is determined when the program runs, and is not under your control." Finally, the manager of the team grew tired of all the arguments, and arranged for the programmers to visit the university to learn the truth about static type systems. The intern on the team was selected to take the programmers there, because the manager himself didn't want to go. The intern got assigned the menial tasks of scheduling the visit, getting approval from finance, and so on. When the programmers reached the computer science department, they were greeted by a former colleague who was currently doing a PhD there. The ex-colleague led them to the classroom. The classroom had several blackboards and projector screens filled with math and code. The programmers squinted and spent some time staring at the various symbols and sentences scattered around. The first programmer pointed to the first blackboard, which had a bunch of greek symbols on it. "See it says here, this kind of type system was used as part of proving the correctness of a complex program" he observed. "Static type systems are for doing proofs!" The second programmer picked up the laser pointer from the podium and pointed it at the left projector screen showing a sophisticated integrated development environment. "Look at all the squiggles and refactoring functionality for automatically fixing the code. Static type systems are more powerful linters," he announced. The third programmer tapped the blackboard adjacent to him to get everyone's attention. "I was right," he decided. "Static type systems are for domain modeling. See how this code example allows modeling concepts like different kinds of users and permissions in an authentication system." The fourth programmer squinted at various type signatures and proclaimed "What we have here, is basically a way of writing comments which use a somewhat rigid syntax, and are checked by the computer." The fifth programmer gesticulated at yet another blackboard. "See! This diagram is showing a deadlock. But it's crossed out, with this sentence 'Well-typed programs do not go wrong'. Clearly, static type systems are meant for making programs safer." All this while, the sixth programmer has been staring at the right projector screen, which shows some benchmarks. "Ah! It seems like this statically typed code runs much faster than the dynamically typed code we generally write at work. So static type systems are really for performance." Bemused, the ex-colleague led the programmers to the cafeteria. "Take a look at the menu and decide what you want to order," he said. "I'll go grab some utensils and paper napkins." While they waited, the six programmers talked about type systems. "Static type systems are for doing proofs," said the first programmer. "Surely, we can all finally agree on that." "Doing proofs? Static type systems are used for improving developer experience" answered the second programmer. "Domain modeling is the main benefit, I tell you," insisted the third programmer. "I'm certain it's basically just a form of machine-checked documentation," said the fourth programmer. "I can see how that can help with on-boarding someone onto a new codebase. But it hardly seems like a game changer." "Safety is really the number one thing, I thought the example I showed made that pretty clear, no?" said the fifth programmer, mildly exasperated. "Don't you see?" pleaded the sixth programmer. "It's really just a performance optimization. It's not really that special. Nowadays, most of our code is plenty fast." The back-and-forth continued with increased adamance, leading to some staring from the nearby tables. "Proofs!" "Developer experience!" "Domain modeling!" "Documentation!" "Safety!" "Performance!" "Stop shouting!" called a very angry voice. It was the computer science professor, who was just out on a lunch break. "How can each of you be so certain that you are right?" asked the professor. The six programmers considered the question. And then, knowing the professor to be very wise, they decided to keep their mouths shut. "Static type systems are all across the spectrum," said the professor kindly. "Each of you focused on one particular facet. Perhaps if you put all the parts together, you will see the truth. Now, let everyone here finish their lunch in peace." When the ex-colleague returned to the table with utensils, the six programmers finally decided their order, and lined up at the counter, all thinking about the professor's advice." "She is right," said the first programmer. "To learn the truth, we must put all the parts together. Let's discuss this back once we get to the office." After they had lunch, the intern called a large cab, and took everyone back to the office.