Code is Engineering, Types are Science

But like many things, I think type systems tend to encourage the thinking "if a little bit of medicine is good, it's best to drink the maximum possible amount of medicine". I think types make good handrails, it's crazy not to provide a little support from falling 16 stories because you tripped on your shoelace. But they don't necessarily need to keep people from intentionally jumping off the stairs, or walking up the stairs backwards, or taking two stairs at a time. Eventually you end up with something so contrived you don't even recognize it's a staircase at first sight.

I never heard anyone say “let’s rewrite this in Node” unironically.

A simple concrete example: a language can use a static type system to make it impossible to encounter a null-dereference error at runtime. That guarantee is a very practical benefit for any codebase.

What is the value of tests?

If requirements are going to shift every five minutes then sure, tests hold you back. Tests in an inherited codebase defined how the system needed to work, not how the system will adapt to changing requirements. Often, particularly for small-enough and simple-enough systems, a human eye is much more flexible than any tests you could write in code.

But the fact of the matter is that the utter majority of software that runs in production (note that qualifier - excluding code that never makes it into production for a variety of reasons), stays in production. It's a corporate cash cow of one kind or another. Software in production needs to be maintained. Software vulnerabilities are reported, old versions hit end-of-life. Java 4 -> Java 5 -> Java 6 -> Java 8 -> Java 11 -> on and on and on. So the business case is very simple. You're forced to make changes and you want to make sure those changes don't kill your cash cow.

Tests check your application at run-time. Types check your application at compile-time. As a result they can provide both more dependable and quicker guarantees than waiting for a run-time test suite to finish running.

If you don't understand the value of tests, you haven't worked on a large enough, mature enough system, where the original engineers have all long left the company.

Faster: depends on what you’re used to. Personally I find strongly typed languages faster to work with evolved code bases. Where you’re refactoring code or dealing with unfamiliar API you get very clear compiler warnings and that becomes as powerful an aid as code coverage in your test suites. When writing new code, it does take marginally longer. But so does many other best practices in software development that are skewed towards maintainability (like writing tests in the first place).

Better: my favourite example of this is when you need to store a serial like “012345”. Without telling the compiler/runtime that it’s a string you run the risk of all sorts of uncaptured bugs. So personally I think typed code is better code. You don’t need to be scientific with how you use type systems either. This specific bug is captured just using a string instead of an integer.

P.S. I'm not saying dynamic types are always bad. There's certainly a time and a place for them. But there's a reason demanding systems software like browsers, databases, networks are being written in Rust these days.

In the practice of software engineering, I would really hope we move away from the attitude of 'move fast'/'get things done' and more towards 'do it right', because I sure am tired of seeing these silly avoidable type errors continue to mess with people's work and lives day after day.

Most people, especially the ones who think typing everything is a great idea, don't understand the difference between types and constraints.

Constraints, for some reason, are incredibly easy for humans to understand. Simple constraints and types match well enough that pretty much all tutorial examples can be done in either without too much difficulty. That gives people the misplaced confidence that everything that can be done in constraints can be done in types. Which is simply not the case.

For the simplest example: what is the type of the identity function? You get into polymorphic types and type variables to get a satisfactory answer, which is by no means obviously true, and fall down the rabbit hole of having your type system be Turing complete too. Which kind of defeats the purpose of types since now you have to deal with all the goodness of undecidability not only horizontally in your code, but vertically in your types.

That is not to say that types are useless, they aren't, but when you start really dealing with higher order functions they are not worth the hassle as defined in any language today.

So have your dynamic language functions you have to document (you do document your code right?), why not just use types instead? I'd far rather see

    def frob(data: np.ndarray) -> float:
      <code with no docstring>

    def frob(data):
      """takes an array and frobs it to give the frobitude score"""

This is what all programming and software engineering is - logical operations within constraints. Types make those constraints more explicit, and make them work for you rather than against you.

They make refactoring of large-scale systems more tractable and less painful, which is invaluable when requirements are shifting. And they can eliminate entire classes of errors, bugs, and security vulnerabilities at compile time, which is invaluable in a day and age when everything is getting hacked.

As type systems become increasingly sophisticated, those benefits become even more true. And when you take into account all the man hours spent on a system, not just in building the quick and dirty initial prototype, but in debugging it for production, and then maintaining it over a long period of time with eventually 100% turnover of the initial dev team, then types reduce time and effort spent too.

You should read the famous paper Out of the Tarpit. Type systems are one of the best solutions to the tarpit of complexity that large systems inevitably incur.

http://curtclifton.net/papers/MoseleyMarks06a.pdf

there's some sort of phenomenon for this, but I can’t recall the name atm.

In the beginning types were useless and hard.

Then we made typeless languages so we didn't need to bother with useless and hard types.

Then we figured out how to make types easier and useful.

1. C - types represent memory layout, which the programmer doesn't care about, are not useful for error handling and control flow and you have to type them out and remember which one is which.

2. Python - Yolo, nothing matters, everything goes. eZ. Shit, why does this code break after refactoring?

3. Rust - Types are inferred, IDEs and the compiler basically tell you what to do and the types are safeguards, rails and handle logic.

Best thing: most of this stuff goes back to the olde languages as well. I.e. IDEs make types in C easier, type hints in Python help with refactoring and so on.

So I think w won't even need to manipulate people out if untyped languages. The academic research that helps make programming better will reach all popular languages.

(Please don't every example to verbatim - it's just a rough outline of an idea not meant to be an in depth analysis. Of course types in C weren't usesless, Rust want the first to introduce all if these ideas, ...).