The value of programs going forward will be the collection of decisions and designs that encapsulates "what does it do and how does it do it". There is no more long-term value in a Rust code base than there is in any other. Any migration is but a prompt away.

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.

Code reviews today are mostly about gut checking if the complexity is worth the benefits.

The right architecture for durable execution depends on the size of the state, the cost of unloading and reloading it, the type of state, the duty cycle, and the mutation rate. The right answer could be long-running VMs, local snapshots, remote snapshots, S3, a DB, etc.

The Sutro team has spent the last five years doing deep engineering to build secure and reliable software. They’re now becoming part of Lovable.

Somehow a 100-line SQL query is considered unmaintainable, but splitting the same logic across five services and a message queue is considered architecture.

At some point, developers are going to abstract away their relationship with the programming language entirely. Many already have. You pick the one that gives the best feedback to the model and produces the fewest surprises in production. This is why Rust is rising. The developers now excited about Rust would never have learned it themselves. It's a pain in the ass to write and takes forever to master. Now that LLMs write it well, the calculus changes. Better type feedback, fewer bugs, faster runtime - what's not to like? If you're not really reading the code anyway, who cares what language it's written in?

"openai engineer explains /why/ he didn't need to understand the kernel line by line" 🙃 we're doing compilers 2.0

No one truly talks about the many foundational values in software engineering was about reusability. If reusability doesn’t matter that much, it impacts every fundamental value we’ve been holding for decades.

Why Microsoft didn't have LLMs do their recent Typescript native rewrite in Go Anders Hejlsberg (Creator of Typescript): "If we just let AI loose on, what is it, half a million lines of code that we have in the old compiler? Well, I don't know that that would absolve us from then having go in and carefully examining every line that came out of it to make sure that there were no hallucinations. Right. Unless you have 100% perfect test coverage, you probably still gotta go check all of that. Now I think a better approach, quite honestly, would be enlist AI to write a program that helps you translate from TypeScript to go, because at that point you can park the stochastic ness in that program and then you can get deterministic behavior whenever you run the program, which means you get the same transformation every time you run it. Right. That's always the thing about AI that people forget it's not deterministic. Right. So you can't really trust that it's going to do the same thing twice. For the full conversation, you can search Anders Hejlsberg's name on my YouTube, Spotify or Apple Podcasts (link in bio)

Effect is verbose is an argument that makes no sense, it is verbose compared to code that only cares about the happy path, that is not testable and doesn’t integrate telemetry. Compared to production grade code Effect is terse.

I was thinking about how I recognize AI writing, and one big tell is excessively colorful verbs. A handful of journalists might write that a proposal "drew" 100 votes, but any normal person will just say "got".

The RCA for the outage we had at GitHub yesterday is live. We're sorry it happened and hope this answers your questions about it. The team is already working on the actions listed here to fix it. githubstatus.com/incidents/z…