geek of programming languages, operating systems, and hypermedia platforms
- Tweets 5,264
- Following 1,662
- Followers 4,932
- Likes 13,829
Manuel Simoni retweeted
So, a lot of people are merely comparing modern PLs to ancient assembly languages instead of contemplating what assembly could be, or what it would have been if we had chosen assembly + metaprogramming over interpreters + compilers.
4
27
654
The last program I vibed is a Lisp compiler.
It does work in practice, but I need it to work in theory, too.
For that I find models not a help at all.
The only thing that works is loading the whole program into wetware, and writing it statement by statement, just like before LLMs
Good programmers state they use models like GPT 6 Astra without obtaining good results: it makes me feel I live in a parallel universe. But the explanation is not that hard: good programming in the past and now requires a different skill set, even if there is some overlap.
4
3
35
1,414
Manuel Simoni retweeted
You see how this looks like some senior developer's wet dream side project, right? How was Steve Jobs the guy who greenlit this?
7
2
169
4,980
If code is only read but never written by humans, there are some interesting changes to PLs ahead.
E.g. import statements are only used so you can write `x` instead of `long-package-name:x`.
But it's much simpler to have no import statements, and just hide the long package name.
4
6
723
"If we don't know how to express a system property as a logical formula, we can't verify it. 99% of the properties we care about fall under this."
I'm seeing a lot of euphoria about how Opus 5.5 is good at TLA+, and this means that all software will soon be formally verified. As a person who loves TLA+ so much he wrote a book on it, I want to throw a particular cold shower on people's enthusiasm by talking about the limits of what you can actually verified with it.
The high level simplification is that TLA+ sees a system as a set of "behaviors", or possible sequences of states. For example, the pseudocode "pick a random number from 1-3 and decrement it to 1" has three behaviors: `{3 -> 2 -> 1, 2 -> 1, 1}`. From here, there are two basic kinds of TLA+ properties:
- `[]P` means that `P` is true in *all states* of *every behavior*.
- `<>P` means that `P` is true in *at least one state* of *every behavior*.
`[]P` is immediately useful as an **invariant**, or something that always be true of your system. This is things like "your data is never corrupt" or "there's always at least one server online." `<>P` is a little more abstract, but for technical math reasons I won't get into here, can be stacked with `[]` to create really complex and useful properties. `<>[]P` represents things like "the algorithm eventually converges on the right answer", `[]<>P` things like "if two data stores desync, they will eventually resync", and `[](P => <>Q)` things like "If a message is put on the queue, it's eventually processed by a worker".
Really cool stuff!
These primitives were chosen to make a wide array of properties useful. And if we're clever, we can do all sorts of more complex properties, like bounded time constraints and history properties. But we're always constrained to 1) define a logical formula 2) over individual behaviors, and 3) check that all behaviors satisfy that formula.
So some things that we *cannot* express in TLA+:
- Possibility and reachability properties: that it's always possible to *make* P true, even if you don't actually decide to. Things like "I can always shut down the computer" or "A user can always change their password". These can't be expressed with `<>P` because that's "for all behaviors, P happens at least once", we actually want "for all behavior prefixes, there is at least one behavior where P happens at least once".
- Hyperproperties: properties that are defined over two or more traces. These are things like "painting a car red doesn't make it faster" or "users cannot infer secret data by observing public data". We can't do these because TLA+ only looks at one behavior at a time.
- Statistical properties: 95% latency is 1ms. Impossible because most of these are hyperproperties.
- Properties about if a system is robust against code changes. Impossible because, uh, you have new behaviors now.
Some of these are solvable in different logical formalisms. CTL can do reachability, PRISM can do statistical properties, etc. Those have their own tradeoffs and limitations, though, and no system can do everything. Others are solvable with a lot of cleverness tailored to the specific spec, like lifting a model into a hypermodel. But these are insanely inefficient and make your "clever spec" diverge significantly from the real world system, so introduce a lot more opportunity for things to go wrong.
The core problem, though, is (1): properties are logical formula. If we don't know how to express a system property as a logical formula, we can't verify it. 99% of the properties we care about fall under this. The information on the site is easy for a user to find. Our LLMs behave as we expect them to. Our application can't be used to break the law. TLA+ (and Quint and Lean and Rocq) are near-useless here, no matter how clever you are.
Don't get me wrong: `[]P` and `<>P` represent a huge range of useful properties and TLA+ is incredible at finding awful concurrency bugs. But there's a lot it fundamentally can't do and we shouldn't believe that it will solve all our worries about software bugs. And the same goes for all other formal verification languages, too.
1
10
100
6,315
Sorry to burst your bubble, but you can't verify your way out of slop.
The only way forward is the old way forward: simplicity, clarity, generality.
(LLMs are very helpful for that, duh.)
2
5
35
769
This line of thinking is incomprehensible to me.
Take high-assurance software: Will it be favorable to use something like Ada vs writing it in raw machine code for the foreseeable future? Yes.
Can an LLM come up with Ada? No.
What's the point of open source? Why build on top of anything or publish anything when agents can just one-shot it?
3
1
19
1,407
Mindmap-like outline that flows to right might be interesting (and space-saving) way to display code?
3
9
1,324
> read source code of Nanopass Framework, one of the pearls of Scheme programming
> uses caddr
4
30
1,287
The best way to treat nullable types is probably like (non-nestable) option types:
A `nullable string` is _not_ a `string`, just like an Option<String> is not a String. You need to explicitly unpack it first.
6
2
27
2,050
I will not get memed into trying out Omarchy, no matter how thrilling and edgy its detractors make it appear.
10
57
2,963
The red-black tree in my new language for Wasm GC is as fast and has roughly the same memory consumption as the native C one I ported it from.
Need to unvibe this codebase and publish.
5
3
90
3,977
Hash table code from my new language for Wasm GC.
It's completely static, and you must write all types manually (there isn't even generic argument inference).
This means I can get decent performance with a toy compiler.
6
2
68
2,892
Finally grokked how tuples in @TitzerBL's Virgil work - it's cool:
You can create a tuple like (1,2,3), and store it in variables, and pass it to functions, but it has no identity.
What happens under the hood is that the tuple actually stands for 3 local variables holding 1,2, and 3.
When you call a function with the tuple as argument, three actual arguments are passed, with 1,2,3 as values.
If you put tuple (x,y,z) into a struct, the struct gets three actual fields x,y,z etc...
So tuples let you program memory-latency--consciously. A tuple does not need an indirection to load, it always exists locally on the stack or in the structure you already have.
1
1
11
1,233