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

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

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?

Extension or Imitation?

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

doscienceto.it

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!"

Kip is featured in a post by @dtemkin.bsky.social about natural language inspired esoteric programming languages! esoteric.codes/blog/five-es...

EsoNatLangs Bring the Complexity of Natural Language into Code

The five esolangs discussed in this piece -- Coem, Love Languages, Prāsa, Kip, and Captive -- draw on aspects of natural language usually avoided in code: nuance and ambiguity, complex grammars and mo...

esoteric.codes

Fermat, 1637

Jon Kuperman@jonkuperman.com · 4mo ago

I also cannot ship my work today because it’s too powerful to release publicly

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

“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.”

Türkçe programlama dili Kip (Konuk: Cumhur “Joomy” Korkut) youtu.be/XNJ3CJyGemY?...

Türkçe programlama dili Kip (Konuk: Cumhur “Joomy” Korkut)

YouTube video by hafif programming

youtu.be

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.

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

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

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.

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 - kip-dili/kip: A programming language based on grammatical cases of Turkish.

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

github.com

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

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...

Intrinsic vs. extrinsic verification

Tracing the origin of the terms

joomy.korkutblech.com

“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!

Lucretiel@lucretiel.me · 11mo ago

Whoops I got annoyed at C advocates again

i love c++ mcyoung.xyz/2025/07/14/b...

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 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.

bloomberg.com

Violating memory safety with Haskell's value restriction welltypedwit.ch/posts/value-...

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

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

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...

Intrinsic vs. extrinsic verification

Tracing the origin of the terms

joomy.korkutblech.com

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

"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! 🎉

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

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.

BeijingPalmer@beijingpalmer.bsky.social · 3y ago

one of the things that was interesting about Twitter was that it really was multilingual, there were whole worlds out there that most people never saw. wonder if something of that scale will ever be recreated, or whether we're now in a new age of the splinternet.

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