George Pîrlea

@dranov
96 Followers
97 Following
20 Posts
PhD student @NUSComputing. Programming languages, formal methods, distributed systems.
Show threadGeorge Pîrlea22h ago
@regehr @stylus And having external verification tools (Verus, CBMC, etc.) doesn't cut it, in terms of user experience, in my view. I think verification has to be embedded in the language for it to not be a total pain, as per Ranjit Jhala: https://www.youtube.com/watch?v=elHEye-nau4
Ranjit Jhala - Language-Integrated Verification

YouTube
Show threadGeorge Pîrlea22h ago

@regehr @stylus I'd one-up this and say that's the future of software period, not just verified software.

It will be a 10+ year transition, but people will increasingly move to writing software in languages with built-in support for meta-programming & verification. A language like Rust already feels crippling. If it all compiles down to LLVM anyway and you (can) get good performance, why would you use a less powerful language? Even if you don't intend to verify, having the option to is good.

George Pîrlea22h ago
Show threadJohn Regehr1d ago
@stylus yeah... I think the future of verified software is less "write it in C/C++/Rust and then prove it correct" and more "write it in Lean or some other mathematical specification language and then extract an implementation"
George PîrleaFeb 3
Terence TaoFeb 2

IPAM is holding an Industrial Short Course on Generative AI Algorithms on March 5-6, 2026. https://www.ipam.ucla.edu/programs/special-events-and-conferences/industrial-short-course-generative-ai-algorithms/

The short course is aimed at people from industry or government who want to get started in deep learning, apply deep learning to their projects, learn how to code deep learning algorithms, and upgrade their skills to the latest AI algorithms, including generative AI. The course will be taught be Professor Xavier Bresson from the Department of Computer Science at the National University of Singapore (NUS).

The course will be limited to 25 participants. The fee for this course is $2,500 for participants. Registration closes soon (Feb 5); we still have a few spots available.

George PîrleaJan 23
Sebastian UllrichJan 22

Sweet embedding of RISC V asm at Lean Together

https://researchseminars.org/talk/LT2026/37/

Show threadGeorge PîrleaJan 23
@kha Amazing stuff!
George PîrleaJan 12
If you are at POPL, join our tutorial on Veil at 2pm and 4pm in Salle 20 to see the future of distributed protocol verification!
George PîrleaDec 21

I've been using Claude Code with Opus 4.5 to write Lean meta-programs (and small proofs) and am constantly amazed at how good it is.

Leo de Moura recently said that Claude has solved non-trivial bugs in the Lean codebase, but it's still astonishing to see it first-hand.

Show threadGeorge PîrleaNov 27

@alexanderbakst @JonathanAldrich

This was the case in Veil. Every monadic bind introduces an ∃ quantifier in the VC if you use forward reasoning. For backward (WP) reasoning, this is a ∀ quantifier instead.

It’s a big issue, since it’s natural in Veil to quantify over first-order functions — with BigStep we’d get higher-order VCs, which we can’t directly send to SMT.

See §3.1 in our CAV tool paper for an explanation: https://pirlea.net/papers/veil-cav25.pdf

Show threadGeorge PîrleaAug 14, 2025
@joseph314 Unfortunately there is no recording, but I've uploaded my slides with notes at https://pirlea.net/talks/veil-cav25.pdf