behold the quality of my commit messages

Functional programming couples functional dependency (for fixed x, y there's at most one z = x + y) with input-output directionality (supply x,y to get z). Logic/constraint programming decouples them: what are the x, y such that x + y = 5?

1000xresist is a helluva game

It is easy to point out all the evil and misfortune in the world. It is also easy to believe in a good so abstract that everything must first be razed to the ground to realize it. Neither is sufficient. You must find something real to cherish, to treasure, to earnestly love, and you must expose it.

I want to merge N sorted arrays in rust (for small N, eg N=8, but not statically known) and I'm having trouble actually making this faster than the dumb obvious thing of just repeatedly merging two of them until done, from small to large.

dreaming of a moderately fast query language

the atreus keyboard layout I've landed on as a {emacs,mac,latex,lisp} user

are enclose.horse puzzles getting easier or am I just gitting gud?

It's well known that set intersection is associative. Unfortunately: import Data.Set n = 20_000_000 evens = fromList [0,2..n] odds = fromList [1,3..n] ends = fromList [0,n] fast = evens `intersection` (odds `intersection` ends) slow = (evens `intersection` odds) `intersection` ends

repost (boosting reach) repost (moral agreement) repost (aspirational) repost (compliment) repost (mockery) repost (cat pic) repost (i got rickrolled)

modal dialogs delendi sunt

there is a direct correlation between how anxious I get about <waves hands> and how many james hoffmann videos I watch

Sophic is to Sophomoric as Sapphic is to Sapphomoric, obviously

More evidence supporting this really neat paper doi.org/10.1111/ajps... (JSTOR version: www.jstor.org/stable/45295...)

My latest for @bostonglobe.com analyzes the killing of #ReneeNicoleGood, and explains why no amount of video footage -- regardless of the angle or quality -- will put to rest the polarization over the tragedy and it's implications. 🧵

Some people, when confronted with a problem, think “I know, I’ll use dependent types.” Now they have several open research questions.

Bidirectional typing can be implemented with two functions, check: term → type → bool synth: term → maybe type I like to merge them, elab: term → maybe type → maybe type elab x None infers; elab x (Some t) checks. This makes it easy to handle eg let-binding, which can either infer or check.

Chuck Tingle's new Booker-prize-winning historical fanfiction, Lincoln in the Birdo

a diptych: 1. oh my god I love NYC 2. I am so tired oh my god

IIII'm John Ronald Reuel Tolkiën John Ronald Reuel Tolkiën-iën (to the tune of "I'm Henry the VIII, I am", natch: www.youtube.com/watch?v=GisC...)

unexpectedly stranded in NYC b/c my flight out rejected me at boarding for not having travel insurance (?!?). Anyone in NYC either/both a) wanna meet up tomorrow (Dec 28)? b) happy to put me up for 1-2 nights until I find a flight?

every corner — I have cut it — nevertheless! Í háve submítted

writing about direct & smash products in pointed sets in a paper draft and desperately trying to find a smash bros joke to sneak in

I have decided to have fun with the section titles in my paper-to-be, at least while I'm writing it.

This is part 4 of subpart 9 of our 15-part (I, II, III, IV, V, VI, VII, VIIIa, VIIIb, VIIIc-1, VIIIc-2, IX, IX with clusters, IX with honey nut clusters, X, XI, XII: Tokyo Drift, XIII, XIV, XV) series that lists all the other articles on this blog. If you donate I will buy the Pentagon.

Engagement KPIs have been responsible for infinite scroll UI traps, RecSys radicalization spirals, public shame brigades, and basically every modern ailment novel to the past decade. At some point, you have to recognize that the problem isn't any one technology, it's the metric.

everything good is bad. everything strong is weak. what you want you don't need; you need just what you don't want.

Doctor says, 'Dont worry, parser design is simple. Great programmer Kate Compton has written the parser you seek’

a geometric visualization of factorized delta queries by @jcreed.bsky.social, representing Δ(R ∧ S ∧ T) = (ΔR ∧ S ∧ T) ∨ (R' ∧ ΔS ∧ T) ∨ (R' ∧ S' ∧ ΔT) where R' = R ∨ ΔR etc.

today I thought "hm, maybe I should reread the Count of Monte Cristo". but you know what they say: vita brevis, ars longa.

My miniKanren 2025 paper, "Fair intersection of seekable iterators", about an efficient, compositional way to implement relational joins on sorted data structures, and how it (sorta) requires "fairness", is now on arXiv: arxiv.org/abs/2510.26016 talk slides: www.rntz.net/files/minika...

The product manager posting implies they have something called a "Brick Foundation model"?

anyone have a good mnemonic for "pushout = quotiented/glued sum; pullback = subset of product"? I have trouble remembering pushout ~ sum ~ colimit and pullback ~ product ~ limit. (Bonus points if it helps me remember pushouts glue and pullbacks subset.)

do we give talks to communicate ideas? we publish in conferences: places where talks happen. but w/ so many papers, conf talks are short & can't explain–only advertize. so workshop talks are miles better. how perverse! our strongest, peer-reviewed results–the worst explained!

I've joked re all SIGPLAN confs being ~the same before. But now I'm at icfpoopsla, picking which talks to see, I'm ~50/50 on ICFP talks vs workshop talks; but almost entirely preferring workshops to OOPSLA talks. Convergence? Not yet!

Slides for my HOPE 2025 presentation, "Finite Functional Programming via Graded Effects & Relevance Types": www.rntz.net/files/hope-2...

why am I calling my secret project "Finite Functional Programming" when I could be calling it "Lambda: the Ultimate Relation"

why is writing (anything) so much like squeezing water from a stone? approximately the most important thing in my profession. I have done it repeatedly. I wrote a whole thesis. it is no easier now than ever. perhaps harder. ughhhh

i go halfway around the world for a conference in a famous tourist city and first day what do I do? go to a bookstore

Does anyone here know a lot about monads & applicatives & such? I'm curious about how to make spreadsheet-style data-flows "monadic". If that sounds interesting please look at my scattered notes at typst.app/project/rnf1... and lmk what's going on. Quick motivation in thread...

Analytically, we differentiate via limits/epsilon-delta. Synthetically, we use infinitesimals - artificial infinitely small quantities. Analytically, we handle dirac deltas with distribution theory. What's the synthetic account? Is it artificial infinitely big quantities?

guess the subject of the paper

productivity of co(inductive)-programs fairness of concurrent scheduling completeness of search strategies these three seem deeply related to me, but I can't yet precisely articulate how. Is there existing work on connections between them?

where did the term "fairness" in concurrent programming originate? is there a canonical definition? a canonical citation? I've found references in Owicki & Lamport 1982 & Andrews & Schneider 1983, but neither originated the term or concept.

what's the equivalent of nicotine patches, but for social media addiction?

imagine an inverse h-index (a ɥ-index?): not how widely an author is cited, but how widely an author cites. do they cite from other subfields? other fields? other centuries? other languages? etc. who do you know who'd have a high ɥ-index?

typing out Haskell code from a paper by hand while listening to Trail of Dead like it's 2005