Type checking is a symptom, not a solution
104 comments
·September 5, 2025jameshart
xlii
And I'll recommend Turing Complete game on Steam if someone wants to have full journey.
It's a puzzle focused on creating electronic components (with the goal of creating a running computer). Since it's more educational than competitive it's rather smooth journey.
But in the end there's not only assembler but there are actual electrons in the system that take time to reach CPU. It took me 2-3 days to finish during Holiday period and it made me much more aware of what is happening under the hood.
delta_p_delta_x
When I was taking my compilers class at uni, I realised very quickly that the most irritating part was the sheer volume of book-keeping.
Things like the ABI itself, which includes register saving/restore, function call stack setup, to the linker and loader, ensuring the right sections go to the right places and are correctly sized, and then at load time ensuring relative addresses are correctly relocated, all branch target labels are resolved to these relocated addresses, it was such a pain.
All of this book-keeping was a genuinely the most time-consuming part of the assignments; the actual compiler ideas and implementation being relatively manageable.
Funnily enough the compiler implementation was done in OCaml.
wazdra
Note that this is not incompatible with the author's view. The function abstraction does solve something: a problem we faced in the 20th century.
While I don't know whether I agree with their view, I do see that, once we've used the function abstraction to build a C compiler, and used this C compiler to build a proper OS, there is possibility for such an OS to provide entirely new abstractions, and to forego (almost) completely with functions.
actionfromafar
A very weird counter point was when I learned how to do COM / OLE calls in assembler instead of C++.
It was easier to get right, there was no wizard behind the typed curtain, just a bunch of arguments.
ratelimitsteve
https://computersystemsbook.com/
If anyone is interested in learning assembly, this was the book and simulator I used as an undergrad. It's not exactly bytecode that will run on an actual processor but it will help you understand the bare metal things a CPU has to do in order to actually operate upon data and it's kinda eye opening when compared to what modern coding is actually like nowadays.
jameshart
I’ll always recommend Ben Eater’s YouTube series - one where he constructs a CPU and then one where he builds a working system around a 6502. Full of amazing insights into the things that a computer has to do just to accomplish the simplest tasks. And if you work your way up from the very bottom you have such an appreciation for why 6502 assembly language is the way it is when it’s introduced.
mnahkies
> make complexity manageable: strict isolation between components, explicit timing constraints, and simple, well-defined interfaces.
Maybe I'm missing something, but those simple well defined interfaces are the types?
I've worked with large javascript codebases before typescript came on the scene, and functions with a single params object were rife, which combined with casual mutation plus nested async callbacks made for a mess that was very difficult to get confidence on what was actually being passed to a given function (presumably easier if you'd written it instead of joining later)
A type system so that you can define those interfaces (and check they're adhered to) feels pretty essential to me.
null
kelnos
I don't really get what the author is trying to say here; it sounds like they don't really know what they're talking about.
They talk about how electronics engineers use "isolation, explicit interfaces, and time-aware design" to solve these problems as if that's somehow different than current software development practices. Isolation and explicit interfaces are types. There's no strict analogue to "time-aware design" because software depends on timing in very different ways than hardware does.
Electronics engineers use a raft of verification tools that rely on what in software we'd call "types". EEs would actually love it if the various HDLs they use had stronger typing.
Where they really lost me is in the idea that UNIX pipelines and Docker are examples of their concept done right. UNIX pipelines are brittle! One small change in the text output of a program will completely break any pipelines using it. And for the person developing the tool, testing that the output format hasn't changed is a tedious job that requires writing lots of string-parsing code. Typed program output would make this a lot easier.
And Docker... ugh, Docker. Docker has increasingly been used for isolation and "security", but the original purpose of Docker was reproducible environments, because developers were having trouble getting code to run the same way between their development machines and production (and between variations of environments in production). The isolation/security properties of Docker are bolted on, and it shows.
mcswell
"UNIX pipelines": Yes, this is where I stopped reading. The author claims that
> UNIX pipelines routinely compose dozens of programs into complex
> workflows, yet they require no type checking at the transport
> layer. The individual programs trust that data flowing between
> them consists of simple, agreed-upon formats—usually lines of
> text separated by newlines.
The transport layer is not the relevant layer; it's the programs in between that matter. If you're just looking for words or characters or something, that's straightforward enough--but the equivalent in programming is passing strings from one function to another. You run into problems when program 1 in the pipeline uses tab delimiters, whereas program 2 was expecting space characters or commas or something, and program 3 is expecting tokens in the pipe to be in a different order, or program 4 doesn't know what to do when some records have three tokens and others have four or two or something.
suspended_state
A few points:
- the explicit interfaces for modules used in hardware design _are_ types. - hardware design requires extensive testing and verification, and formal verification (using types) is a valuable step in hardware design.
I think the author conflates the use of types with structural complexity - at least at the introduction of his article, hence the term "symptom" used to qualify type checking in the title (actually _lengthy_ type checking, this is implied, but without context the title of the article becomes clickbait-y).
Indeed, by the end, the author admits that types are useful, without conceding that the initial idea was an error of judgment.
wrs
> you can reason about each component in isolation
> you can focus on the explicit contracts between components
> you can design systems where problematic interactions are structurally impossible
In other words, exactly what a strong type system gives you?
My impression from doing my own amateurish hardware projects and knowing some real hardware engineers is that they would KILL for something like the type systems we have in software. In fact there are plenty of hardware description language projects that try to strengthen the type system of the HDL to catch errors early.
If you think a Rails test suite is bad, look at a Verilog test suite sometime.
lambdaone
What I find most amusing in this article is that its author states with great confidence that electronic systems designers don't use anything like rule checkers or typing, when the EDA industry is well-known for its extensive use of validation tools, and the design of large-scale complex modern electronic systems is almost impossible without it.
zamalek
For the uninitiated, one popular example is SPICE: https://en.wikipedia.org/wiki/SPICE
toolslive
>functional programming languages ... break down when you try to coordinate between components, especially when those components are distributed ...
I think the exact opposite. Having spent more than a decade in distributed systems, I became convinced functional programming (and pure functions) are essential for survival in distributed systems.
Back then I wrote down my insights here (amazed that the site still exists)
https://incubaid.wordpress.com/2012/03/28/the-game-of-distri...
ndriscoll
And part of why functional programming works so well is exactly that you don't need to care about things like control flow and interactions. You're just expanding definitions. Those definitions are local/isolated, and compose in regular ways.
zamalek
Even with my limited knowledge about FP I am pretty sure I would only grow more in agreement as I learn more. My only exposure to functional is via Nix and Rust (I promise I'll learn OCaml soon). One thing that I've really come to appreciate is the concept of "making invalid states unrepresentable," a trick that is harder than it should be (though not impossible) in "less functional" languages. Coming back to distributed systems, I have wondered what a functional database would look like. Mutations as pure functions, DUs in tuples, could we store a function, etc.
addaon
> "making invalid states unrepresentable," a trick that is harder than it should be (though not impossible) in "less functional" languages
The flip side of this is to "make representable states valid." If you have an enum that doesn't fill a bitfield, values of the bitfield outside the enum are representable -- and the behavior of the system must be defined in that case. (Most often, this is done by mapping the behavior of undefined states to a chosen defined state, or using it to trigger an abort -- the key is that it must be an explicit choice.)
toolslive
regarding databases, you get quite far using purely functional data structures and zippers.
c2247946
[dead]
nonethewiser
>The standard answer is scale. “Small programs don’t need types,” the reasoning goes, “but large programs become unmaintainable without them.” This sounds reasonable until you realize what we’re actually admitting: that we’ve designed our systems to be inherently incomprehensible to human reasoning. We’ve created architectures so tangled, so dependent on invisible connections and implicit behaviors, that we need automated tools just to verify that our programs won’t crash in obvious ways.
A few thoughts...
1. Some things are complicated. Of course we should elminate needless complexity - but not all complexity is needless.
2. If your system has huge thing 1 connected to huge thing 2, then you have to understand 2 huge things and a little glue. If you instead have a system comprised of small thing 1 connected to small thing 2, ... connected to small thing 100, you now how to understand 100 small things and 99 connections. The nature of these things and connections matter but you can't just keep dividing things to simplify them. John Carmack's email about inlining code springs to mind: http://number-none.com/blow/john_carmack_on_inlined_code.htm...
3. "A complex system that works is invariably found to have evolved from a simple system that worked. The inverse proposition also appears to be true: A complex system designed from scratch never works and cannot be made to work. You have to start over, beginning with a working simple system." - https://en.wikipedia.org/wiki/John_Gall_(author)
I would love to see the author take a complex system where Typescript (for example) is "necessary" and refactor it to JavaScript.
valcron1000
> that data flowing between them consists of simple, agreed-upon formats
> HTTP servers and clients, email systems, DNS resolvers—they all interoperate based on simple protocols
Yeah, massive disagree with this. There is absolutely nothing "simple" about these protocols. Try to compose 3/4 UNIX programs together and you necessarily need to run it to see if it even makes sense. Don't get me started on HTTP.
It boils my blood to read "simple" in the context of software engineering
andrewstuart
>> Instead of worrying about how changes in one module might ripple through dozens of dependencies, you can focus on the explicit contracts between components.
So, typing.
Smaug123
> When components are designed as genuine black boxes—where what happens inside stays inside, and communication occurs only through explicit input and output ports—systems naturally become easier to reason about.
"How do you specify the shape of the input and output ports?" shouts the goose as it chases me away.
Rohansi
Text goes in and text comes out - simple! Works perfectly for shell scripts. /s
tshaddox
This might be the worst argument against type checking I've ever heard, in a strong field!
This author would apparently also argue that, because I rely on handwritten labels for the dozen or so storage bins in my garage, I must have created a system so intricate and interconnected that human reasoning fails, then declared the tools that help me navigate this complexity to be essential.
The author would surely make similar arguments against clocks, calendars, and calculators.
Of course, what's actually happening in all of these situations is that humans are relying on tools to handle tasks which the tools are designed to handle, so that the humans can focus on other things.
All programmers need to try assembly programming just once.
Just a program counter, a stack, a flat addressable block of memory, and some registers.
You’ll very quickly learn how hard it is to program when you have complete responsibility for making sure that the state of the system is exactly as expected before a routine is called, and that it’s restored on return.
Every language tool we’ve built on top of that is to help programmers keep track of what data they stored where, what state things should be in before particular bits of code are run, and making it harder to make dumb mistakes like running some code that will only work on data of one sort on data of a totally different structure.
Of course types are a solution. You just have no idea what the problem was.