Andrew Boyton

@damekdavis @tribbloid Isabelle/HOL had a method a decade or so ago that would try find counter examples. Wasn’t perfect but sometimes it was VERY helpful. Based on Haskell QuickCheck IIRC.

@tribbloid Yes

'Proved' something new and had codex formalize it lean. It generated 41000 lines. I initially left all cited theorems that I relied on as axioms, but then I started formalizing them. Codex complained about one particular result. Turns out that result was false as stated.

@AdamRackis We often feel more productive with AI but are actually less. They’re like slot machines. fast.ai/posts/2026-01-… > A study from METR found that when developers used AI tools, they estimated that they were working 20% faster, yet in reality they worked 19% slower.

99% sure I could have just moved all those files, and adjusted the ~12 import paths faster than the 3 minutes 45 seconds it took my agent to do so. Starting to wonder if we might be overusing this shit just a lil

@AdamRackis @fardarter You can disable a specific rule showing in VSCode but leave the rest. I’m AFK but I think it’s something like this. { "eslint.rules.customizations": [ { "rule": "no-console", "severity": "off" }, { "rule": "no-debugger", "severity": "off" } ] }

@fardarter I don’t run ANY lint tools in my editor. I don’t like seeing every console.log / debugger / etc light up red as I’m coding

Looks like I got a lint error on line 69 👀

@kamatsu8 If you train yourself you can hear the “ring” before it feeds back. What you can do if you have a graphic equaliser is find the squeal frequency and remove it, then remove some of the harmonics. Means you can have things louder before it squeals. That or move the mic or speaker.

@boyto_ I think it's mostly the latter. My parish also lately has had problems with feedback loops causing ear-bleeding screeches. It's hard to pin down the exact cause.

It's a highly specific complaint, but I've never seen the microphones/audio system in any cathedral or church work 100% reliably. They seem to require constant maintenance, babying, and expenses. Why is this!? It seems absurd that we can't make this technology reliable.

@johnzabroski @Leonard41111588 And if all you’re verifying is the C code then the C compiler can decode to produce assembly code that’s no longer constant time. And eventually you’re down to the ISA of a chip no? I left the seL4 project before most of their timing work and that was a long time ago.

@johnzabroski @Leonard41111588 It’s been a long time since I’ve formally verified any code but I guess I don’t 100% understand what you mean by constant time. There’s “simple” things like not returning early when comparing equality but ist any branch potentially susceptible to timing attacks like Spectre?

AI is writing a growing share of the world's software. No one is formally verifying any of it. New essay: "When AI Writes the World's Software, Who Verifies It?" leodemoura.github.io/blog/2026/02/2…

@Leonard41111588 You mentioned timing attacks. What type of verification are you doing that supports reasoning about timing? I’m much more used to refinement proofs where you prove the code implements an abstract specification. How do you reason about timing down to the CPU level?

@Leonard41111588 Verifying ZIP is very impressive. That’s a great example where the specification is relatively easy to specify, which I find is rarely the case. I’m not seeing in that repo that it’s written in Lean rather than just bindings to the C. Am I missing something there?

@kamatsu8 Sound is definitely more complex than lights. I do think the move to digital sound desks has made the harder to debug. Are the issues hardware breaking or things just not working? Most of my issues are the latter. Joys of way too many operators and someone changing something.

@boyto_ Now my parish is on a shoestring budget but my parish in Edinburgh is not in financially bad shape, and they recently had sound system gremlins too.

@kamatsu8 Some older or fancier building like cathedrals do have trouble getting them to sound good as they weren’t designed for speakers and you can’t always put the speakers and mics in the best position as people don’t want to destroy the asthetics (for good reason).

@kamatsu8 Not normally had too many issues in churches I go to. The biggest problem for most is that they are run by volunteers of varying skills or with very cheap budgets.

@ajrgd @JustDeezGuy @HSVSphere I’ve not worked on this for over a decade so I’m rusty. I’d say Isabelle, the model of C, the ARM model, the tooling, the proofs and the techniques could all be used elsewhere. Some more reusable/useful than others.

@JustDeezGuy @boyto_ @HSVSphere l4v

Yes, and the verification code is way more than the actual C code. Take a look at the sel4 kernel, the C kernel is tiny whereas the proofs are an order of magnitude larger in a functional language

@JustDeezGuy @ajrgd @HSVSphere All open source last I checked. github.com/seL4/l4v

@ajrgd @HSVSphere Isabelle/HOL and HOL4.

@dcolascione @HSVSphere That work was being automated as the project was being developed. I suspect the original proofs could have been much shorter had they used AutoCorres, but it was only after doing them manually the automation could be built. github.com/seL4/l4v/blob/…

@HSVSphere Makes you wonder why we have to hand compile the proof to C

@JustDeezGuy @HSVSphere I’m not quite sure how any of this relates to how verbose safe code is. If anything verified C can be more terse as it doesn’t need to be defensive to get the same guarantees. I guess you could say the verbosity is in the proofs but that doesn’t seem a fair comparison.

@JustDeezGuy @HSVSphere Also the size of the refinement proof between the different models (abstract, Haskell, and C) is not really the same as how verbose the models themselves are. Proof size is more a measure of Isabelle and the tooling. The models were much smaller than the C implementation.

@kerckhove_ts @JustDeezGuy I was projecting objects from one state space into one which had pieces of objects so I could reason not just about objects separately but also pieces of objects seperaetely. Having invalid states in the pieces world was okay but caused too much pain I found a different encoding

@kerckhove_ts @JustDeezGuy The amount of time I spent trying to create a separation algebra on a state space with invalid states I learned the hard way to not allow invalid states. I don’t remember what they were but a decade or so later I still remember the lesson well.

When people say "Make invalid states unrepresentable", that always sounded like "These a b = This a | That b | These a b" not being able to have neither a nor b, but in reality it's more "Char" not being a Bool, and "Int" not being null.

@jessfraz `Some(Personality::None)` is just beautiful from a type safety point of view. “Remind me, what was that billion dollar mistake again?” At least they’ve added a None of some description.

this is the most frustrating thing of my entire life considering how many people I've told that codex is amazing to.

@MichaelArnaldi @_cristianvr_ @francisco_m001 @IzakFilmalter @shuding @EffectTS_ When I first read about effect and yield I was really hoping things what it would do. I get why it doesn’t automatically lazily fetch everything (or eagerly but allow waiting on arguments) but I wished it had. Would have removed a whole class of performance issues.

@_cristianvr_ @francisco_m001 @IzakFilmalter @shuding @EffectTS_ quickly ending up being a type nightmare

Better Promise.all with automatic dependency optimization and full type inference: github.com/shuding/better…