Also, statefullness. Baudot has two codes used for switching into one of two modes: figures and letters.
Typewriters have some statefullness, too, like "shift lock". Baudot needed to encode the actions of a type writer to control it, not the output.
1,755 karma · joined January 20, 2015
Typewriters have some statefullness, too, like "shift lock". Baudot needed to encode the actions of a type writer to control it, not the output.
(I find the example of the computational geometry algorithm being a clear case of direct memorization not very compelling, in any case.)
https://randomascii.wordpress.com/2012/02/11/they-sure-look-...
It is a very wide term, IME, that means anything besides "one-shot through the network".
I think the thing about the search formulation, which is amenable to domains like chess and go, but not other domains is critical. If LLMs are coming up with effective search formulation for "open-ended" problems, that would be a big deal. Maybe this is what you're alluding to.
The rules / dynamics / objectives of chess ( and Go ) are trivial to encode in a search formulation. I personally don't really get what that tells us about AGI.
(Not everyone agrees, for sure, but that's different from it being a joke.)
> LLMs have hidden state not necessarily directly reflected in the tokens being produced, and it is possible for LLMs to output tokens in opposition to this hidden state to achieve longer-term outcomes (or predictions, if you prefer).
But what does it mean for an LLM to output a token in opposition to its hidden state? If there's a longer-term goal, it either needs to be verbalized in the output stream, or somehow reconstructed from the prompt on each token.
There’s some work (a link would be great) that disentangles whether chain-of-thought helps because it gives the model more FLOPs to process, or because it makes its subgoals explicit—e.g., by outputting “Okay, let’s reason through this step by step...” versus just "...." What they find is that even placeholder tokens like "..." can help.
That seems to imply some notion of evolving hidden state! I see how that comes in!
But crucially, in autoregressive models, this state isn’t persisted across time. Each token is generated afresh, based only on the visible history. The model’s internal (hidden) layers are certainly rich and structured and "non verbal".
But any nefarious intention or conclusion has to be arrived at on every forward pass.
When you use "hidden state" the way you are using it, I am left wondering how you make a distinction between autoregressive and recurrent architectures.
- the sufficient amount of information to do evolution of the system. The state of a pendulum is it's position and velocity (or momentum). If you take a single picture of a pendulum, you do not have a representation that lets you make predictions.
- information that is persisted through time. A stateful protocol is one where you need to know the history of the messages to understand what will happen next. (Or, analytically, it's enough to keep track of the sufficient state.) A procedure with some hidden state isn't a pure function. You can make it a pure function by making the state explicit.
The "transformer" part isn't under question. It's the "hidden state" part.
Intermediate activations isn't "state". The tokens that have already been generated, along with the fixed weights, is the only data that affects the next tokens.
These LLMs are almost always, to my knowledge, autoregressive models, not recurrent models (Mamba is a notable exception).
https://goosetaco.notion.site/Beware-of-negative-polarity-st... . It links to https://answers.ros.org/question/12230/what-is-ros-exactly-m...
https://lean-lang.org/doc/reference/latest/Basic-Types/Subty...
A crucial difference between type theory (as its known in Lean) and set theory is that an inhabitant/element is of exactly one type.
You might be interested in this podcast Bad Faith: Episode 478 - The Abundance Conspiracy (w/ Sandeep Vaheesan, Isabella Weber, & Aaron Regunberg)
Episode webpage: https://www.patreon.com/posts/130189560
I think there are two primitive sets for dependent type theory. The one with omega, and then the one with inductive types. None of them need axioms like the Peano axioms.
It was interesting because they were asking "is this all you need? What about the Peano axioms? Is there anything more primitive than the inductive data type?"
I bring it up because it's good not to take for granted that the Peano axioms are inherent, instead of just one design among many.
Does anyone store uncompressed video these days? Honest question.
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
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 ;)
To your point, goals can differ.
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.
```
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:
```
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.0imIt’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).
Specifically, the two views of typing.
But my fault for linking to a mediocre blog post.