Javier Casas

A random walk through computer science

Types and correctness as an afterthought

Disclaimer: this is a big rant. Read at your own discretion.

Today, I had the misfortune to observe something so bad that it deserves its own category. I tend to name the sin and not the sinner, but some sins are so heretical that they deserve an exception to the rule.

The setup

Today, I was checking a shared repository to be integrated into other repositories. This shared repository contains Typescript React components that get compiled down to JavaScript and typings, so that we can reuse them. So far, nothing special.

Well, one of our team members decided to use Babel for that task. So far, nothing special.

Then, another team member committed some more components. And a few more components from the first team member. Everything typechecks, everything seems to be fine.

Well, it isn't. The code actually doesn't typecheck. There are a bunch of anys that the tsconfig.json is forbidding. There are some cases of reading indexes from numbers. But no error messages. So our developers develop, no type error pops up, and then, when I try to compile the components, tsc barfs a gigantic list of type errors. The code has passed reviews and everything because we trust the typechecker, and no type errors have been shown at all during development. A gigantic pile of errors have passed just in front of our eyes, and we have been unable to see them.

How can this happen?

The sin and the sinner

Well, someone at Babel decided that Typescript is not worth the hassle. He, in his infinite wisdom has decided for everyone that typechecking a codebase shall not be done, even if you have explicitly stated (by installing and configuring Typescript) that you want the codebase to be checked. The reason: it's too slow.

Allow me to apply that same principle (slow speed of recompilation) to modern tech principles:

  • We shouldn't TDD or write tests at all because compiling and running tests takes more time than not compiling or running them.
  • We shouldn't use high-level languages because compiling high-level languages to machine code takes more time than not compiling.
  • We shouldn't use low-level languages because compiling low-level languages to machine code takes more time than not compiling.
  • We shouldn't write assembly because using an assembler takes more time than not using it.
  • Therefore, we should write directly machine code in files, or maybe in punch cards if we feel happy to murder some trees today.

This comes from a big group of developers that includes some well-known juniors posing as thought leaders that think that types are an afterthought.

The school of "types are an afterthought"

One of the things that frustrates juniors when starting to use a typesystem are the errors. The compilers have a bad record of showing unreadable error messages. You don't know frustration until you have seen a bad type mismatch. Fortunately, these type errors are there for a good reason. Type 'any[]' is not assignable to type 'number' is an ugly error. But it's also a fair affirmation. An array is not a number, regardless of how some think tanks may want to spin it. So, using a typesystem takes build time and generates ugly (but true) errors.

The problem arises when people start to think that types are not good enough representation of correctness. I understand this if you use Java, because Java has a prehistoric type system that tries to prevent using types to write correct code. But there is a world out there beyond Java in terms of typesystems and typecheckers. I tend to speak a lot about Haskell because it has an awesome type system, but for more mainstream people, there is Typescript, which supports surprisingly advanced features. You also have Scala, Rust, Kotlin, C++, OCaml, Go, and a swarm of programming languages with better types than Java.

Imbuing a complete proof of correctness in code using types is quite hard (but can be done, as the Agda folks claim), but that doesn't ignore the fact that you can use the typechecker to imbue some level of correctness in your code. The same can be said about tests: you can use tests to imbue some correctness into your code.

Because people see tests as a way to imbue some correctness, the school of "types are an afterthought" thinks that, because tests already provide correctness, you don't need any other way to provide correctness. They totally ignore that almost no modern program has been shown to be totally correct using tests, regardless of test coverage. All the fanatics of 100% coverage ignore that they are checking the program with a small list of possible inputs, whereas full correctness requires checking the program with all possible inputs, this includes each and every possible input. Otherwise you would be happy to accept that every number is a prime number, because you have checked with numbers 1, 2 and 3, and they happen to be primes, therefore all tests pass.

This means most programmers, including some "thought leaders" just don't have the least idea of what full correctness means. But they have an opinion. They think that, because they have written a couple of tests, that because their test coverage is some percent, that because they have been writing buggy code for X years, that because they have written some books on opinions on writing code, all their code is perfect as is. Therefore, adding something such as a typechecker to it will do nothing more than wasting time, because the code is perfect because DEITYtoldme.InfactscrewDEITY told me. In fact screwDEITY telling me! I'm $DEITY and I tell myself whatever I want!

And they push their shoddy definition of correctness to everyone, infecting software development with bad practices. And then, someone at Babel decides that typechecking with Typescript is a waste of time because a "thought leader" said it. And then frontend development is hard because we can't use tools such as a typechecker to check our code because Babel has decided to ignore typechecking for everyone. And then everyone laughs at the state of JavaScript development because of this and that, ignoring the fact that there are some actors out there that pose themselves as benefactors, but actually work hard at sabotaging software development. Because, there is no way to hide the fact that writing a parser that reads and strips type annotations from Typescript is way harder than just using the Typescript compiler, that will itself strip the type annotations after typechecking.

These people, these "thought leaders", these "types are an afterthought" people, obviously write type signatures and please the typechecker after all the development has been done because a tech lead or some pointy-haired-boss told them to do it and they have some metrics to fulfill. After all, why do it if the code is perfect without types? The code is perfect, regardless of catastrophic runtime errors, and typechecking is a waste of time. No stinky typechecker ain't stoppin' me from writing int foo = "blah"; in the name of fast iteration, yeehaw!

So what?

Frontend is hard. I mean, we have to deal with the browser, with three languages in a row (HTML, CSS, JavaScript) and the DOM. Then we have to deal with the fact that a frontend application is an application running on the browser getting data from a backend, which combined make a Distributed System, and Distributed Systems are hard. Then we have to deal with the fact that there are different browsers that interpret the W3C standards in subtly different ways, so we have to figure out how to make some code work on the major browsers at the same time. Then we have to deal with the fact that constructing UIs is hard, and that's why we have Designers and UX people and psychologists to understand the user. Then we have to deal with the fact that we don't know yet how to construct great architectures for UIs, and we have to explore Vue, React, FRP, JQuery, Svelte and many others looking for the silver bullet.

And, finally, we have to deal with the fact that some of the people we trust, some of the people that pose themselves as benefactors, are actually saboteurs, and they push upon us Babel, Angular, Internet Explorer, types-are-useless, DRM and ActiveX, and we have to work hard to push them away and go screw somewhere else.

And this is why Frontend is hard.

Back to index
Copyright © 2018-2023 Javier Casas - All rights reserved.