researcher @Bloomberg. 📜 somehow a computer doctor. tweets about formal verification, compilers, types, metaprogramming, linguistics. 🇹🇷
New York City
Joined February 2010
- Tweets6.1K
- Following988
- Followers3.9K
- Likes26.6K
Pinned Tweet
can't find a topic for your next programming languages paper? worry not! type system idea generator: type.systems/
no one wants to see your AI generated slides.
they all look similar, and they lack a good narrative. take the time to make them; it'll force you to think harder about your audience and the story you want to tell. AI is decent for making visuals for slides, but not the structure.
seeing that this tweet is making the rounds, I'm happy to invite any mutuals here for the small price of talking to me about the cool thing you're working on
Everyone wants to tell me how great their office pantry is but after the Bloomberg pantry nothing can surprise me. The Bloomberg pantry is the size of a small regional airport. The Bloomberg pantry has a fresh peanut butter machine and matcha on tap. The Bloomberg pantry makes the Thrive Capital pantry look positively soviet. Its memory will drive you to tears whenever you visit another newsroom
joomy retweeted
Verified core (the cube), unverified shell (the renderer).
Formal verification is not all or nothing.
playing around with writing a Rubik's cube solver verified (to produce valid solutions) in Rocq, extracted via Crane to C++, uses Raylib for 3D graphics and animations). joomy.korkutblech.com/rubik/
joomy retweeted
VB6 is back this week and not how you would imagine, RAD is back, let’s celebrate HTML/JS 😎 wieslawsoltes.github.io/VB6/
in Oakland from Sunday to Thursday for SPLASH (and to give talks at HATRA and REBASE industry track). 🌉
mutuals in the Bay Area, let me know if you want to meet up!
I've never read/studied Proofs and Types but I looked at its PDF after seeing this tweet and it's crazy how much of it I already ingested through courses, summer schools, lectures, etc.
anyway, there are probably other combos of books that would also work but this is decent too.
joomy retweeted
cute semantics :) It's a shame it's buggy though :\
I hope you haven't used it to prove anything big yet!
It's kinda hard to trust vibe-coded semantics IMO even testing isn't enough to catch all the bugs
ALT pathleak2.c next to the Lean theorem pathleak2_every_outcome and two terminal outputs. cerberus-lean runs the program to Defined, value Specified(0), with empty stdout. The same program compiled with gcc prints hunter2 and fails the assertion n == 0.
We built a Lean port of Cerberus, a highly realistic C semantics. If you want to model and reason about C code in Lean, now you can github.com/OathTech/cerberus…
> i ask Claude if the program is verified
> he says yes
> i ask if he verified the program or a smaller, better-behaved program he imagined
> he laughs and says “it’s verified sir”
> i use the program
> it has a bug
I used Opus 5.5 to formally verify the Claude Agent SDK using Lean. A couple short prompts = 16 PRs fixing various bugs and race conditions. Video attached.
TLA+ also works well. I sometimes combine Lean and TLA+ to look for issues around data flow, concurrency, and state mgmt.
I don't know either language well, but Claude is excellent at both. This approach is super useful for formally modeling your code and finding bugs that a human probably wouldn't have spotted.
Is formal verification the future of coding (or at least, bug finding)?
joomy retweeted
⚡️ A lightning talk on Kip the Turkish programming language by @joomy at the Haskell symposium at @icfp_conference! youtube.com/watch?v=6bam-Z6J…
> there's just one catch though, which is that the published implementation drifted from the formalization so *can* contain bugs
but that's the whole point! 🤷♂️
you can have a neat formal model, but it's only a model! it's not the real thing; doesn't give you strong guarantees.
...
so, I'm offering $10k to whoever proves Bend is inconsistent
that's my actual response to these attacks
if Bend is "flawed", go ahead. show it, and take my money
the challenge is simple: write a Bend file that parses, checks, and outputs "All terms check.", with no unsafes / holes, that contains a top-level definition of type Empty (the empty type). this would show that Bend proves a falsehood, and you get 10k from me
(also, a friendly reminder that Lean's implementation was shown inconsistent. several times. I wish I didn't need to point this out, as I deeply respect all the people involved in the project. but that's the truth. Lean is big, and we're far from its *implementation* being formalized and proven consistent. Bend is small, and formalized.)
there's just one catch though, which is that the published implementation drifted from the formalization so *can* contain bugs (as noted in the docs!). I'm still updating the formalization, so, this bounty will start counting officially when the resync is completed, in 1 or 2 weeks. I'll post here
sorry for being angry, I'm not going anywhere. but I definitely need to log off. I guess I should spend some time in a place less toxic than X and Reddit. like League of Legends!
meanwhile, open issues and send PRs. I'll be looking
see you
playing around with writing a Rubik's cube solver verified (to produce valid solutions) in Rocq, extracted via Crane to C++, uses Raylib for 3D graphics and animations). joomy.korkutblech.com/rubik/
🌶️ "Why Rocq is better than Lean for program verification": A write-up on why I don't give in to the hype and switch to Lean for formal verification of programs. joomy.korkutblech.com/posts/…
I will talk about it some more at the Lean NYC meetup on Sunday, for those of you in the city (see lean.nyc for details) xitter.cf/TechAtBloomberg/status…
At this Sunday's NYC Lean #Meetup (8/2 @ 2 PM EDT), @Joomy Korkut delivers a talk outlining the design, implementation challenges, and early lessons learned in integrating verified programs into real-world C++ systems with Crane
bloom.bg/4woGws3
#opensource #FormalMethods
