Untyped programs don't exist: https://www.williamjbowman.com/blog/2018/01/19/untyped-programs-don-t-exist/
Demonstrates a simple theorem, but has a nuanced notion of types as invariants. It discusses the important questions of when we should check types, allowing escape hatches, and whether type checking should be decidable.
Related Posts
Playing with optional type signatures in Python, I realise that the return type is the most important to me.
I'd much rather have a function with only a return type instead of a function with only parameter types. It's often quick to add too.
I'm implementing an interpreter, and wondering how often I should check for interruptions (e.g. Ctrl-C).
I don't want to spend too much CPU time checking whether I've been interrupted, but I also want slow programs to stop promptly. It's tricky.
Bootstrapping a language can be immensely satisfying.
I've added the ability to define stub types in the Garden stdlib and suddenly I don't need to special-case Int or String! They're just normal type declarations.