> 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.
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.
> 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.
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),
> 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.
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.