> Ron's Third Law (*): For any position regarding the proper design of a programming language there exists an authoritative-sounding aphorism to support it.

And let's not forget the Law's corollary:

"For any such position there also exists an authoritative-sounding aphorism to oppose it."

I agree with everything you said, and just wish you'd respond to the strongest points, not the weakest ;)

Specifically, the two views of typing.

But my fault for linking to a mediocre blog post.

> Specifically, the two views of typing.

That was in the other article, the one I didn't comment on at all.

There are two reasons I didn't comment on it. First, I don't actually understand what the author means by things like "only phrases that satisfy typing judgements have meanings" and "a typing judgement is an assertion that the meaning of a phrase possesses some property". I can kinda-sorta map this onto my intuitions about compile-time and run-time typing, but when I tried to actually drill down into the definitions of things like "phrase" and "typing judgement" I got lost in category theory. Which brings me to the second reason, which is that this is very, very deep rabbit hole. To do it justice I'd have to write a whole blog post at the very least. I could probably write a whole book about it. But here's my best shot at an HN-comment-sized reply:

I've always been skeptical of the whole static typing enterprise because they sweep certain practical issues under the rug of trivial examples. The fundamental problem is that as soon as you start to do arithmetic you run headlong into Godel's theorem. If you can do arithmetic, you can build a Turing machine. So your type system will either reject correct code, accept incorrect code, or make you wait forever for an answer. Pick your poison.

Now, this might not matter in practice. We manage to get a lot of practical stuff done on computers despite the halting problem. But in fact it does turn out to matter in practice because in practice the way typed languages treat arithmetic generally imposes a huge cognitive load on the programmer.

To cite but one example: nearly every typed programming language has a type called Int. It is generally implied (though rarely actually stated) that it is meant to represent a mathematical integer (hence the name). But computers are finite state machines which cannot actually represent mathematical integers. So in practice Int generally means something like Int32 or UInt64 or maybe, if you're lucky, a generic numerical type that will automatically grow into a bignum rather than overflow or (if you're unlucky) wrap around if you try to add the wrong values.

Sometimes these details matter and sometimes they don't. Sometimes when I'm adding things I really care about how it's done under the hood. Maybe I'm writing something mission-critical that can absolutely not fail, or maybe I'm writing an inner loop that has to run as fast as possible at the cost of possibly failing on occasion. But sometimes I don't care about any of this and I just want to add, say, two elliptic curve points by writing P1+P2 rather than EllipticCurveAdd(P1,P2) -- or was that EdwardsCurveAdd(P1,P2)? or Curve25519donnaPointsAdd(P1,P2)? -- and I don't care if it takes a few millisecond because I'm just noodling around with something. If I have to take even 30 seconds to read the docs to remember what the name of the function is that adds elliptic curve points, I've lost. It doesn't matter so much if I only have to do it once, but in practice this sort of cognitive load infects every nook and cranny of a real program. Thirty seconds might not matter much if you only have to do it once. But if you have to do it all the time it can be the difference between getting your code to run in a week and getting it to run in ten minutes. And God help you if you should ever have to make a change to an existing code base.

Those are the sorts of things I care about. Those concerns seem worlds away from the kinds of things type theorists care about.

> Those concerns seem worlds away from the kinds of things type theorists care about.

It’s true there’s a tradition, voiced by Dijkstra, that emphasizes correctness at a point in time, sometimes at the expense of long-term adaptability.

> “Unfathomed misunderstanding is further revealed by the term software maintenance, as a result of which many people continue to believe that programs – and even programming languages themselves – are subject to wear and tear. Your car needs maintenance too, doesn’t it? Famous is the story of an oil company that believed that its PASCAL programs did not last as long as its FORTRAN programs ‘because PASCAL was not maintained’. “ (Dijkstra, “On the cruelty of really teaching computer science“, EWD1036 (1988))

As for Gödel, I’d say invoking incompleteness is like invoking Russell’s paradox — important for foundations, but often a distraction in practice. And ironically, type theory itself arose to tame Russell’s paradox. So while Gödel tells us no system can prove everything, that doesn’t undercut the usefulness of partial, checkable systems — which is the real aim of most type-theoretic tools.

Among the “three poisons,” I’m most comfortable rejecting “correct” code. If a system can’t see your reasoning, how sure are you it’s correct? Better to strengthen the language until it can express your argument. And since that relies on pushing the frontiers of our knowledge, then there are times when you need an escape hatch --- that is 50% of how I understand "dynamicism".

The intrinsic vs. extrinsic view of types cuts to the heart of this. The extrinsic (Curry) view — types as sets of values --- aligns with tools like abstract interpretation, where we overlay semantic properties onto untyped code. The intrinsic (Church) view builds meaning into the syntax itself. In practice, we need both: freedom to sketch, and structure to grow.

-----

On the cognitive load of remembering names like `EllipticCurveAdd(P1, P2)` vs. just writing `P1 + P2` --- that pain is real, but I don't really see it as being about static typing. It’s more about whether the system supports good abstraction. Having a single name like `+` across many domains is possible in static systems --- that’s exactly what polymorphism and type classes are for. The most comfortable system for me has been Julia, because of pervasive multiple dispatch, and this focus on generic programming correctness. I don't think this works well unless the multiple dispatch is indeed pervasive (which requires attention paid to performance), and I'm pretty sure CLOS falls short here (I am no expert on this).

The difference between Julia and "static types" here is more about whether you are forced to content with precisely the meaning of `+`. In the type class view, you bundle operations like `+` and `*` into something like "Field". Julia is much more sloppier and simultaneously flexible. It does not have formal interfaces (yet), which allows interfaces to emerge organically in the ecosystem. It is also a pretty major footgun in very large production use cases....

FWIW, I have been a huge fan of "Lisping at JPL" for many years now and it is validating in many ways. I especially enjoyed the podcast with Adam Gordon Bell. This is also validating: https://mihaiolteanu.me/defense-of-lisp-macros (discussed on HN).

I think we are more or less in violent agreement here. Our disagreements are on the fringes, and could well just be a result of my ignorance or misunderstanding. That said...

> invoking incompleteness is like invoking Russell’s paradox — important for foundations, but often a distraction in practice

Yes, but the operative word here is "often". "Often a distraction" is logically equivalent to "sometimes relevant". The problem is that whether or not it is relevant to you depends on your goals, and different people have different goals. For example, one of my goals is pedagogy, and so it's really handy for me to be able to fire up a CL REPL and do this:

    Clozure Common Lisp Version 1.12.1 (v1.12.1-10-gca107b94) DarwinX8664
    ? (expt (sqrt -1) (sqrt -1))
    #C(0.20787957 0.0)

so that I can tell a student, "See? i to the i is a real number! Isn't that cool?" But if your goal is to build a social media site that has no value for you. Different strokes.

> The intrinsic (Church) view builds meaning into the syntax itself.

This is what I don't get. I can't even wring any coherent meaning out of the phrase "build meaning into the syntax itself". Programs don't have meaning, they are descriptions of processes. Programs don't mean things, they do things.

Even for natural language sentences, which do mean things, I don't understand what it could possibly mean to build meaning into the syntax. "The dog ate my license plate" has meaning but "The dog ate my car crash" does not despite the fact that those two sentences are syntactically identical.

(BTW, imbuing syntax with meaning sounds more like Chomsky than Church to me. But what do I know?)

> I’m most comfortable rejecting “correct” code.

Again, one of my goals is pedagogy. Towards that goal I once wrote this:

https://flownet.com/ron/lambda-calculus.html

After writing that, I thought this might be a good time to learn Haskell. If CL is good for showing off the lambda calculus surely Haskell will be even better? I'm guessing I don't need to explain to you why that did not go to plan.

And BTW, thanks for the kind words.

Ah, your example reminds me of a quirk in Julia where some methods are type stable, and others are not. (This is just an aside. I'll provide a response in another comment.)

    ```
    julia> sqrt(-1.0)
    ERROR: DomainError with -1.0:
    sqrt was called with a negative real argument but will only return a complex result if called with a complex argument. Try sqrt(Complex(x)).
    Stacktrace:
    ```

The justification is "type stability". The return type of a function should be constant across different values of the same input type. This is not a requirement, but a guidance that informs much of the design, including the DomainError on `sqrt(-1)`, instead of returning a complex result.

However, the same choice is not made universally:

    ```
    julia> sqrt([1 0; 0 1])
    2×2 Matrix{Float64}:
     1.0  0.0
     0.0  1.0

    julia> sqrt([-1 0; 0 -1])
    2×2 Matrix{ComplexF64}:
     0.0+1.0im  0.0+0.0im
     0.0+0.0im  0.0+1.0im

```

> ERROR: DomainError with -1.0: > sqrt was called with a negative real argument but will only return a complex result if called with a complex argument. Try sqrt(Complex(x)).

This is the sort of thing that drives me absolutely nuts. In no possible world that I can imagine is generating an error a more useful result than returning a complex value. I could forgive it if the system didn't know about complex numbers, but in this case it is clear that the system is perfectly capable of producing a correct and useful result, but it just refuses to do so in service of some stupid ideology. I have zero tolerance for this sort of nonsense.

I'm not sure how familiar you are with Julia, but it is very spiritually aligned with lisp. The reason for the DomainError is "type stability" and it's not stupid ideology unless you consider high-performing numerical code stupid ideology.

To your point, goals can differ.

I know very little about Julia. It is on my list of Things To Look Into Some Day.

> type stability [is] not stupid ideology unless you consider high-performing numerical code stupid ideology.

"Stupid ideology" may have been putting it a bit strongly, and there are times when I want numerical code to be performant. But I don't always want that, and I don't want a language that makes me pay for it even when I don't want it. Almost always I prefer high-fidelity [1] over speed. But even when I want speed, I always want to start with high-fidelity, get that working, and then make it fast if I need to. 99% of the time I don't need to because 99% of my code turns out to be I/O bound or memory-latency bound. It's extremely rare for my code to be compute-bound, and even in those cases I can almost always just find a C library somewhere that someone else has written that I can call through an FFI. So for me, a programming language that forces me to pay for run-time performance whether I want it or not has negative value.

But honestly, I can't actually think of a single instance in my entire 40 year career when the run-time performance of my CL code was a limiting factor. The limiting factor to my productivity has almost always been my typing speed and the speed of my internet connection.

---

[1] By "high fidelity" I mean how well the semantics of the language reflects the domain model, which, in the case of numerical code, is mathematics. Fixnums and floats are a fast but low-fidelity model because they don't actually behave like the integers and reals that they purport to model. Bignums and rationals are a high(er)-fidelity model. A really high fidelity model would let me do something like (* (sqrt 2) (sqrt 2)) and get back exactly 2 by having some sort of exact representation of algebraic numbers. I don't know of any programming language that provides that natively, but some languages, like CL and Python, let me extend the language to add that kind of capability myself. For me, that kind of extensibility is table stakes.

> The intrinsic (Church) view builds meaning into the syntax itself.

I shouldn’t have phrased it that way --- the distinction between syntax and semantics is awkward for me, especially when there are discussions of "static" vs "dynamic" semantics. What I meant is closer to this: in intrinsic systems, the typing rules define which terms are meaningful at all. Terms (programs) that do not type do not have meaning. This is the sense in which "correct programs get rejected".

> Programs don't have meaning, they are descriptions of processes.

Despite my confusion about the previous point, one clear thing I can point to, however, is the funny realization that there are some programming languages where the primary point is not to run the program, but just to type check it. This is the case for many programs written in languages such as Lean and Rocq. In these situations, the programs do have meaning and are not descriptions of processes. A much more common example that makes it clear that programs aren't just descriptions of processes is in the "declarative" languages. In SQL different execution plans might implement the same logical query, and writing down the SQL is less about describing a process and more about assertion or specification.

> depends on your goals

That’s fair, and I agree (perhaps violently??) I focused on your mention of Gödel's incompleteness because it’s often brought up (as I think you did here) to cast doubt on the viability of static typing in practice, but I don't think it does that at all. I think what casts much more doubt is a connection that I have felt is missing for a while now, which is about interactivity or perhaps "live programming".

The Lean and Rocq interactive theorem proving environments are very "live", but not with a REPL. It's fascinating. But it's also because those programs, in a sense, don't do anything...

There is a type theory rabbit hole, for sure. I think there is also a Smalltalk and Lisp rabbit hole. I would like them to meet somehow.

> Lean and Rocq

Yep, I get that. But I don't think of these as programming languages, I think of them as proof assistants. Related for sure, but different enough that IMHO it is unwise to conflate them.

> SQL

Again, a whole different beast. Database query languages are distinct from programming languages which are distinct from proof assistants. All related, but IMHO they ought not to be conflated. There is a reason that SQLite3 is written in C and not in SQL.

> it’s often brought up (as I think you did here) to cast doubt on the viability of static typing in practice

I bring up Godel just to show that static typing cannot be a panacea. You are necessarily going to have false positives or false negatives or both. If you're OK with that, fine, more power to you. But don't judge me if I'm not OK with it.

> There is a type theory rabbit hole, for sure. I think there is also a Smalltalk and Lisp rabbit hole. I would like them to meet somehow.

You want Coalton :-)

https://coalton-lang.github.io/

> But I don't think of these as programming language

I don’t want to get too caught up in what counts as a programming language, but you can absolutely write programs in a language like Lean, e.g. computing factorial 10. The fact that you can also write proofs doesn’t negate a system's status as a programming language. It’s worth noting that the official Lean documentation reflects this dual use: https://lean-lang.org/documentation/.

So there’s no conflation... just a system that supports both orientations, depending on how you use it.

> SQL [...] ought not to be conflated

I agree that SQL isn’t a general-purpose programming language, but you said something to the effect of "I don't understand what meaning a program has beyond what it does", and if you know about SQL, then I think you do understand that a program can have "computational meaning" that is separate from its meaning when you run it through an interpreter or processor.

> You want Coalton :-)

Thanks for the pointer. I am going to read https://coalton-lang.github.io/20211212-typeclasses/ , hoping to eventually achieve clarity on the relation between multiple dispatch and type classes..

That said, my interest in generic programming pushes pretty hard toward dependent types. I’m increasingly convinced that many patterns in dynamic programs, especially those involving runtime dispatch, require dependent types in order to be typed. Coalton might help me understand better the relation also between interactivity and static typing. But it's not going to be a panacea either ;)

> I bring up Godel just to show that static typing cannot be a panacea. You are necessarily going to have false positives or false negatives or both. If you're OK with that, fine, more power to you. But don't judge me if I'm not OK with it.

If you want a static type system that is sound and decidable, it will necessarily reject some programs that would behave just fine at runtime. That’s not really Gödel’s fault. It follows more directly from the halting problem.

But that's a quibble, and I still know what to make of your stance. The thing you're not okay with is having the system "get in your way", which is your false positive (the polarity doesn't matter, if that's what I'm getting wrong). The point is you want to say "my program is correct, now run it for me", and you will hate if the system rejects it.

What you don't hate is runtime type errors.

There is no judgement on my side on the preferences. But I'm confused. If you don't have any static type checking, then it's like having a system that always gives negatives, and some of those will be false (again, assuming I got the polarity right. if not, just swap here and earlier). I'm pretty sure you're okay with this, even though the text of your last message leads me to believe otherwise.

To summarize, there’s a fundamental trade-off:

- If you want a sound type system (never accepts unsafe programs),

- And you want it to be decidable (terminates on all inputs),

- Then it must reject some safe programs.

If you're not okay with that, then... sorry :D

> you want to say "my program is correct, now run it for me"

No. I want to say "Run this program whether or not it is correct because I just want to see what it does in its current state." Sometimes I know that it will produce an error and what I want is the information in the backtrace.

> What you don't hate is runtime type errors.

It depends. I hate "NIL is not of the expected type" errors. So I have a bee in my bonnet about that too, it's just not something that comes up nearly as often as static-vs-dynamic. I think typed nulls are a good idea, but very few languages have those.

> If you don't have any static type checking

I love static type checking. The more information I can get at compile time the better. I just think that the output of the type checker should be warnings rather than errors.