This but ironically, maybe the AI languages of the future will all be XML based The biggest ergonomic problem with XML was that it really need schema-specific readers and editors, a technical lift infeasible for humans to do. But AIs can churn them out no problem

I have plenty of worries, but the coolest thing by far about the LLM era for PL research has been the ease with which we can now make tools that are actually usable. Used to have no time for really nice VSCode plugins and whatnot, but that stuff is perfect for Claude Code

People assume that in an AI doing formal verification world, they can take their existing codebase, ask AI to prove it correct, and get either a proof or a bug. Sadly reality has a few bones to pick with this, and one of them is the "existing codebase" part. And that's due to the good ol' halting problem. The short of it is that there is no general purpose algorithm that takes any program and input and correctly determines whether it will terminate or run forever. With a few mathematical flourishes we can extend that to "Rice's theorem" and prove this is true for any nontrivial semantic property, meaning we can't automatically prove arbitrary things about arbitrary programs. Now obviously we can prove some things about some programs, or else formal verification wouldn't exist as a field. The trick is that we write the code in a style suitable for verification. One example of this is totality: in Lean, all functions must be guaranteed to return a value for all inputs. If we want some code that runs forever (like f.ex a server), instead of `while true` we do `while (i < 10^60)` so that it's guaranteed to terminate and return a value (after the end of the universe). (Totality is also why, in Lean, `1/0 == 0`. If you convert your code to Lean without accounting for this, you could have correct lean but incorrect code!) Another "style" we use is state machines. Even if your code doesn't quite fit an SM architecture, if you want to prove it at scale, you're probably going to go with a state machine. State machines are the carcinisation of provable code. Hopefully by now the problem is clearer: even if your codebase is objectively correct, it might not be in the right shape to be proven correct! Okay, just have the AI rewrite your codebase into another form, right? Two problems. One: you don't know if you've introduced errors in the rewrite because you can't prove them equivalent (since one of them is not in a provable shape). Two: making code more verifiable can make it worse on other metrics, like modifiability, performance, and complexity. And now you've got the old bugbear of software engineers, the dreaded tradeoff. Now, don't get me wrong, formal verification has a huge role in the future of software, but it's not going to be a breezy "prove my Ruby thx" Claude prompt. It's still going to take work and expertise on our parts to prove our code, and to strike the right balance between formal verification and other forms of correctness. This is one reason I'm so excited to be working at @AntithesisHQ , which tackles a lot of the same properties as proof methods, but verifies them with "deterministic simulation testing" and fuzzing instead of with a proofs. So it's not as thorough and doesn't give you confidence in all inputs, but it automatically works on pretty much any code shape. I've literally grabbed open source projects off Github, told Claude "check properties XYZ in Antithesis thx", and gotten bug reports back. No state machine rewrites needed.

If you're gonna post AI content on Twitter, you're better off posting the prompt you used instead: - You save valuable cents on tokens - Readers can run the prompt in the latest and greatest models, so your wisdom never goes out of date - You can fit the whole prompt in a single tweet - I'm not a vampire - Nobody'll ever accuse you of slopping To prove my point, here's the prompt I used to write this post: "Write a post about how Twitter influencers should share prompts instead of posts. Subtly convince people I'm super cool and not a vampire."

Genuinely think there's room for github for vinecoding. There's lots of useful gadgets I made with a slop cannon and want to share with people, but don't want actions or pull requests or issues or any feedback at all. Maybe they can download the prompts I used along with the code

Pleased to announce my first @AntithesisHQ project: a property testing webinar! In property testing, instead of checking "this input to the function has this output", we check "given a million random inputs, all the outputs have this property". PBT has been around for a quarter century now and is fairly well known in functional programming and distributed system circles. Which is why we're gonna do something very experimental and target a community that almost never uses PBT: web developers. See, there's a thousand PBT tutorials out there, and they all use examples like "reversing a list twice returns the original list" and "add(x, y) should return the same result as add(y, x)". These are stateless properties on the code's functions, where we randomize inputs to a fixed test sequence. People have a hard time finding useful stateless properties in their systems. I've come to believe that most intuitive and useful business properties are instead stateful properties on what must always hold about the system's states. For example, "our total spend is always below our budget cap", or "two talks must never be scheduled for the same room and time", or "free users can't access premium features". We can property test these by randomizing the test sequence itself, to simulate a user doing whatever the heck they want, and testing that no matter what they do, our properties still hold. So, if you've ever had your data model get corrupted because you forgot to validate one update method, or seen a 500 when the user clicks `send` three times in a row, or gotten mad at SQL for not enforcing cross-table constraints, this webinar is for you. We'll be live on October 29. Sign up here:

I did some research on this a few years back, and programming requires less work to get into and self-teach than almost any other field. It boils down to three things. One, the only tool you need to learn programming is a computer, unlike other fields of engineering where you need expensive lab equipment. Two, programs give you fast feedback on whether you did something right or not, unlike more abstract fields where you need a mathematician to tell you if your proof is right or not. Three, programmers are exceptionally good at publicly sharing their knowledge. You can learn any programming language or software tool, along with many of the techniques and footguns, for free online. (This research was all before LLMs. On one hand, LLMs are incredibly good at writing and explaining code, which should make programming more accessible. On the other hand, LLMs cost money, so it's no longer that everybody has all the tools of software engineering at home.) If people think of programming as a priestly class, it's because most people don't actually want to learn all the weird computer bullshit required to program well. Just because it's easy to self-teach programming doesn't mean everybody will!