iiinova — where your digital self keeps evolving

joomy @joomy.bsky.social · 16/09/2026

I took a dist sys class with him in 2016 and really enjoyed it! he allowed us to use whatever PL we want, and I asked him "even Haskell?", trying to be a smartass, not knowing that his background. I think we both surprised each other: github.com/joom/distrib... last I heard he was teaching at NYU.

github.com

GitHub - joom/distributed-hash-table: A Haskell implementation of distributed hash tables with two-phase commit.

A Haskell implementation of distributed hash tables with two-phase commit. - joom/distributed-hash-table

020

joomy @joomy.bsky.social · 11/09/2026

I'm particularly upset for >>=, which is reserved bitwise right shift and self assignment, and now cannot ever be used for anything else :(

030

joomy @joomy.bsky.social · 28/07/2026

🌶️ "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/2026-0...

joomy.korkutblech.com

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.

1152

Reposted by joomy

Joe @doscienceto.it · 04/06/2026

Wrote a little #haskell quiz doscienceto.it/extension-or... Can you tell the valid Haskell Language Extensions (based on the GHC docs), from the Impostors?

doscienceto.it

Extension or Imitation?

Can you tell the real Haskell Language Extensions from the Imitations?

0174

joomy @joomy.bsky.social · 23/04/2026

related: en.wikipedia.org/wiki/Axiom_o... (they're pretty good too!)

en.wikipedia.org

Axiom of Choice (band) - Wikipedia

120

Reposted by joomy

vaibhav sagar @vaibhavsagar.com · 22/04/2026

Compiler goes to programmer. "Programmer, I am in rough shape. Mutable references abound and the tiniest changes break API compatibility." Programmer replies, "The treatment is simple! Rewrite in Haskell and GHC will sort you right out." Compiler bursts into tears: "But I am GHC!"

012720

joomy @joomy.bsky.social · 15/04/2026

this, but conservatively?

1261

joomy @joomy.bsky.social · 31/03/2026

Rocq is Pacman complete! see Rocqman, a Pacman implementation (with some proofs!) in Rocq, extracted to C++ via Crane: github.com/joom/rocqman

181

Reposted by joomy

boarders.bsky.social @boarders.bsky.social · 26/02/2026

“If formal verification becomes vastly cheaper, then we can afford to verify much more software. […] AI also creates a need to formally verify more software: rather than having humans review AI-generated code, I’d much rather have the AI prove to me that the code it has generated is correct.”

martin.kleppmann.com

Prediction: AI will make formal verification go mainstream — Martin Kleppmann’s blog

173

Reposted by joomy

Jenny with a Green Ribbon Around Her Neck @readingtheend.bsky.social · 02/02/2026

one thing that would be cool, when prominent creators turn out to be terrible people, would be if we didn't have to go through this performative dance of insisting that their work was never good in the first place.

734042964

Reposted by joomy

Satnam Singh @satnam6502.bsky.social · 23/01/2026

At Harmonic we've just announced $1,000,000 of sponsorship for Principal Investigators and Rising Mathematicians. Significant O($100K) funding for high-impact projects. Early access to next-generation Aristotle models. Please apply! aristotle.harmonic.fun/sponsorships

aristotle.harmonic.fun

Aristotle API

073

joomy @joomy.bsky.social · 23/01/2026

number guessing game (courtesy of @fka.dev) in Kip's now interactive playground. see for yourself at kip-dili.github.io

041

Reposted by joomy

Mehmet Hakan Satman @jbytecode.bsky.social · 22/01/2026

Kip Programming Language by @joomy.bsky.social The language is based on a natural language: Turkish 🇹🇷. Not only one-to-one translations of keywords but the whole language is based on the Turkish grammar. Here is an example of `isodd` function.

131

Reposted by joomy

Sedat Kapanoğlu @ssg.dev · 17/01/2026

fantastic project. i always wanted to explore turkish grammar in programming because it’s so suitable for fluent constructs. glad to see others thinking the same.

github.com

GitHub - kip-dili/kip: A programming language based on grammatical cases of Turkish.

A programming language based on grammatical cases of Turkish. - kip-dili/kip

2176

joomy @joomy.bsky.social · 18/01/2026

thank you both, for your kind words :)

020

Reposted by joomy

Julien Vanegue @jvanegue.bsky.social · 02/12/2025

This Friday, the New Jersey Prog Lang & Systems seminar hosted at @princeton.edu will feature our own @bloomberglp.bsky.social researcher Matthew Z. Weaver presenting new research done with @joomy.bsky.social on extracting certified C++ code from @CoqLang. Full program: njpls.org/dec2025.html

njpls.org

NJPLS Dec 2025

031

Reposted by joomy

Kiran @kirancodes.me · 08/10/2025

it's interesting bridging colloquial terminology between domains - as a verification gal, I'm very used to intrinsic/extrinsic to classify verification styles, but surprised my co-authors weren't aware of it, so had to look up if I had just made it up lol joomy.korkutblech.com/posts/2024-1...

joomy.korkutblech.com

Intrinsic vs. extrinsic verification

Tracing the origin of the terms

101

Reposted by joomy

DEI Speedwagon @myrrlyn.net · 07/09/2025

“c gets you close to the machine” is the kind of sentence that lands very differently after working in a factory you’re not supposed to be close to the machine! that’s where the finger munchers are!

1342158

joomy @joomy.bsky.social · 18/06/2025

excited that my team at Bloomberg is supporting PhD students in certified programming (and other infra/sec topics too!) through a fellowship. 💻🛡️ includes stipend, tuition, and internship. timely for Rocq and proof assistant folks as science funding tightens. please apply by July 18th! 📬

bloomberg.com

Bloomberg Infrastructure & Security Ph.D. Fellowship | Bloomberg LP

Apply now for the Bloomberg Infrastructure & Security Ph.D. Fellowship program. Applications are due by Monday, June 30, 2025 for the 2025-2026 academic year.

0136

joomy @joomy.bsky.social · 29/04/2025

there are two lines of research I'd take a look at: 1. bidirectional predicates in the Prolog world (I think someone already mentioned logic programming) 2. bidirectional lenses. maybe too domain-specific, but probably a good start: www.seas.upenn.edu/~harmony/ dl.acm.org/doi/10.1145/...

010

joomy @joomy.bsky.social · 25/04/2025

PLUM folks should be made honorary New Jerseyans...

110

joomy @joomy.bsky.social · 25/04/2025

hey, I’m going to be the last talk of the upcoming NJPLS! now I really have to prepare a talk… 🎙️ njpls.org/may2025.html

njpls.org

NJPLS May 2025

121

joomy @joomy.bsky.social · 16/04/2025

NYC folks, come hear me sing on May 31! tickets available here: www.eventbrite.com/e/new-york-a...

New York Ataturk Chorus Summer Concert flyer. Saturday, May 31, 2025. 2:30pm.

020

joomy @joomy.bsky.social · 12/02/2025

I'm writing a paper and I once again found myself explaining intrinsic vs. extrinsic style of verification. I never know what to cite for this, so I decided to dig a bit deeper to find the origin of these terms. please lmk if you find anything else: joomy.korkutblech.com/posts/2024-1...

joomy.korkutblech.com

Intrinsic vs. extrinsic verification

Tracing the origin of the terms

041

joomy @joomy.bsky.social · 04/12/2024

I see your cinnamon and raise you a cinnamon

030

joomy @joomy.bsky.social · 27/11/2024

bound copies of my dissertation arrived and they are so pretty ☀️

1141

joomy @joomy.bsky.social · 22/11/2024

thank you! though to be fair, there is a lot of existing work on reasoning about C programs: softwarefoundations.cis.upenn.edu/vc-current/P... in the paper, we are using one of them (VST) to reason about C foreign functions linked to CertiCoq-compiled Coq programs.

000

joomy @joomy.bsky.social · 20/11/2024

We didn't go the full ITree route in the paper since the tree is parametrized by a stack of event types, which complicates how the execution function has to be written. (can also have a runtime cost so we have to be careful) But I imagine the ITree approach would organize the proof+program better.

010

joomy @joomy.bsky.social · 20/11/2024

The path is less clear for other effectful programs. There is work on proving effectful programs correct: * github.com/search?q=rep... * doi.org/10.4230/LIPI... * doi.org/10.1145/3293... Expressing the program with an ITree and writing an execution function for it in C is probably the way to go.

121

joomy @joomy.bsky.social · 20/11/2024

Thank you! I don't foresee a huge challenge for the mutable array example: We have a purely functional model that computes the same result; VST is good at such proofs. We also now have proofs about how the GC deals with mutation.

110

joomy @joomy.bsky.social · 19/11/2024

if I misunderstood and you were asking about dynamic checks for safe FFI, there's some work on that too: www.cs.princeton.edu/~appel/paper...

120

joomy @joomy.bsky.social · 19/11/2024

thank you! can you clarify what you mean by dynamically changing models? do you mean based on input from the outside world? I think you would have to model that as an effect, like in section 12.2.

110

joomy @joomy.bsky.social · 19/11/2024

"A Verified Foreign Function Interface between Coq and C", by me, Kathrin Stark and Andrew W. Appel will appear at POPL 2025! www.cs.princeton.edu/~appel/paper... this is the culmination of years of research (and most of my grad school work), so I'm excited to see it finally published! 🎉

24419

Reposted by joomy

JMCT @jmct.bsky.social · 18/11/2024

Is it cool if I post one of my favorite creations from the other place? #functionalprogramming #math #programming

5269

joomy @joomy.bsky.social · 14/11/2024

i’m prob too old to dare to explain, but in my understanding “cooked” is bad. “cooking” (as in “let him cook”) is good.

000

joomy @joomy.bsky.social · 02/07/2023

though the Twitter Circle was a decent temporary hack for this. I added some of those personal connections to my circle and exclusively tweeted in Turkish there.

000

joomy @joomy.bsky.social · 02/07/2023

Twitter was really bad at multilingualism. my followers were mostly English speakers (professional connections) and a few hundred Turkish speakers (personal connections). I avoided tweeting in Turkish because it could look unprofessional.

130

Reposted by joomy

plaidfinch @plaidfinch.net · 28/06/2023

if you run haskell on an ibm laptop, call it a thunkpad

085