Ilya Sergey

@mboehme_ @HerrDreyer @ShriramKMurthi Programming languages are not “empirical systems”. They have very formal (albeit somewhat complicated) descriptions—compilers—which might ot might not adhere to formally stated properties we want them to have.

@ilyasergey @HerrDreyer @ShriramKMurthi To elaborate: Isn't the key underlying (imo unsolvable) problem of formalization the objective of making formal statements about an empirical system? For instance, Rust is subject to evolution as a consequence of its interaction with a messy real world.

New on "Proofs and Intuitions": Verifying Move Borrow Checker in Lean: an Experiment in AI-Assisted PL Metatheory. proofsandintuitions.net/2026/03/18/mov… The gist: I formalised Move's type system in Lean: 39KLOC, under a month, with Claude. Person-years in PL research are now person-weeks.

@mboehme_ @HerrDreyer @ShriramKMurthi Sorry, I am not sure I understand which concrete interaction example you are referring to (not that I’m opposing this idea in general).

@ilyasergey @HerrDreyer @ShriramKMurthi Then again, isn't precisely this interaction between the formal and the empirical world the crux of the matter?

@HerrDreyer @ShriramKMurthi I am talking about this exactly at the end of the post. :)

@ilyasergey @ShriramKMurthi Of course, the technology you're talking about here still seems like it will be really useful. But I think humans will still need to help figure out what are the right specs to be proven.

@HerrDreyer @ShriramKMurthi That comment was, of course, tongue-in-cheek. Sorry for not making it more apparent. I am well aware that formalising Rust is one of PL moonshots, and I had no intention to diminish the significance of all advances in the field it had stimulated.

@ilyasergey @ShriramKMurthi I don't buy that one can completely formalize Rust in a month, for the simple reason that the problem is not well-defined. People are still trying to just agree on what Rust is, and there are hard problems to sort out there which are not just a matter of pushing through lemmas.

@ShriramKMurthi It probably will. I would not agree that Move is trivial—but to be fair, in this experiment, I was working with a mostly complete, well-thought type system proposal from the very beginning.

@ilyasergey I think it will take longer for non-trivial languages. I think there are also non-linearities here. A student may do a "burn out" sprint for a month, but can't sustain that for a second month, so it may be "if it doesn't finish in 1 month, it'll need 3"?

@ShriramKMurthi Thanks! I'm not sure which way my estimate is off, tho, in your opinion. I've done it in one month, *obviously* not working on it full time. A trained graduate student would likely have accomplished much more in a month of full time work, perhaps, completely formalising Rust.

@ilyasergey This is excellent stuff, Ilya, and I mostly agree with it. Except I think your "one month" estimate doesn't pass my (weak) smell test. Or maybe you mean 1mo of *full time work by a trained grad student*? Or maybe in 3 years, when we have built up enough knowledge/libraries?

@RanjitJhala @kc_srk Thank you Ranjit! Indeed, we can finally use those nerdy proof tools as, what’s the word… assistants!

@ilyasergey @kc_srk Inspiring stuff Ilya! I find your claim that mechanizing-no-longer-slows-you-down very plausible.

@kc_srk This is the way.

Thanks to @ilyasergey for pushing me to use Lean :-)

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…

Had a productive CNY break. A new blogpost is coming soon.

I now honestly think that most engineers who still think that agents will be plopped into existing software development loops - tickets, push to GitHub, run CI, review a PR, merge a PR - aren't thinking far enough ahead.

@ShriramKMurthi Sophia is amazing.

Sophia Drossopoulou went to the trouble of preparing a slide specifically for me with a bunch of the things that I really like, to welcome me to give my talk at Imperial. (-:

@karthik3407 Not at all. One can verify real-world software nowadays. Some prominent large-scale formal verification efforts are CompCert, seL4, and IronFleet.

@ilyasergey aren't formal specifications and proofs only logical verifications ? I think simon is concerned about the verification of code/implementation.

Luckily, we’ve got tools to manage the vibe coding-induced cognitive debt: Formal Specifications and Proofs

Velvet, our automated Dafny-style verifier embedded into Lean, has moved to a new repository as a standalone Lean library: github.com/verse-lab/velv… Give it a try!

@satnam6502 If performance is a concern for your type checker, it’s called an abstract interpreter.

@ilyasergey Performance?

Stages in designing a new type system for a programming language: 1. Make it sound (it's correct) 2. Make it decidable (it's built into a compiler) 3. Make it pretty (it's usable) All that, of course, only if it ensures something useful.

@k0nn0v I'm wearing my type theoretician hat today.

@ilyasergey Are you sure it is how it happens in practice? It looks like 3, 2, 1 is the standard sequence.

@industrieapps No, I didn’t need this, although that is quite feasible.

@ilyasergey Did you really make AI write in TLA+?

New post on "Proofs and Intuitions": Verifying Distributed Protocols in Veil. We take a tour of Veil, a Lean-based verification framework that combines TLA+-style model checking with formal proofs and enables AI-powered invariant inference. proofsandintuitions.net/2026/02/09/dis…