← Feed

Posts

• View post

  ✈️SFO➡️LHR

• View post

  book haul book haul (moe's books, berkeley)

• View post

  god bless VLC

• View post

  I am once again asking you to please stop cryptically posting about The Discourse without saying what it is you're talking about. Just as someone's average friend has more friends than them, a post's average reader is Less Online than its author. The web is hyperlinked for a reason! subtooting a person: ok, you don't wanna attract their attention, I get it subtooting current events: WHY

• View post

  chatgpt alone has looked on beauty bare

• View post

  Terence Tao & other Fields medalists have a declaration worth reading on math & ai: https://mathandai.org/ It notes a clash between AI benchmark culture and mathematical understanding, which to me suggests a subtle emendation of Goodhart's law: with enough optimization pressure, aligned goals diverge. Before, solving major open problems required gaining community understanding of it; now, an AI company LLM swarm can demolish a problem without contributing much to the mat...

• View post

  Do any proof assistants expose a way to get the "trust base" of a given theorem (excluding the checker itself)? This means: 1. All definitions transitively used by the theorem statement. (A mistake in a definition means you've proved the wrong theorem!) 2. Any axioms/postulates; anything proved by sorry/admit/etc. Is this standard? If not, why not? Seems essential for proof review.

• View post

  I wish Rust had ML-style modules. Traits/typeclasses are great for the common case of a structure over one type. If there's one main type & some auxiliary ones, fine, ok. But ML modules can save your ass because they don't make you feel like you're holding it wrong if you need to parameterize over lots of types and none of them is "the one main type". You just do it and move on, instead of chickening out or getting into "which thing is t...

• View post

  I was listening to the local classical music radio station and I was like "wait... that sounds like something... ... ... is that SANDSTORM by DARUDE?!" sure enough, the opening of the 3rd movement "Rondo" of Adam Schoenberg's American Symphony has a line of melodic stabs that hits the same note sequence (though with a different rhythm) as the opening of Sandstorm. Compare: 0:00-0:05 Rondo https://www.youtube.com/watch?v=ShVo7-IUCd4 0:09-0:14 Sandstor...

• View post

  VIDEO GAMES I STILL THINK ABOUT, A THREAD If I had to identify running themes in video games I like, I'd say: exploration; puzzles; unique or fitting art direction; and telling a story in a way only a videogame could. But unlike happy families, every good video game is good in its own way, so here are a few of the ones I've liked most. [inspired by @chrisamaphone's great thread: https://recurse.social/@chrisamaphone@hci.social/116890204764652215]

• View post

  Is there standard literature on how to do worst-case optimal queries in the presence of functional dependencies/foreign keys? There are cases where you can use FDs to get asymptotic speedups but I'm having trouble figuring out the right general approach rather than looking at individual queries and saying "oh, obviously you index it this way and then it's fast".

• View post

  romance languages imply the existence of bromance languages

• View post

  RE: https://recurse.social/@rntz/116585751551131492 mastodon continues to be a great place to talk about wild maths ideas; all the replies I got to this were fantastic and illuminating

• View post

  The miniKanren and Relational Programming workshop is accepting submissions until June 5th! You (yes you!) should submit! We accept short or long papers, about miniKanren or relational programming more widely - and, this year especially, about relating the two, and what relational/logic/constraint/etc programmers can learn from one another! :) https://icfp26.sigplan.org/home/minikanren-2026#Call-for-Papers

• View post

  "Loft" is a measure of how much down feathers "puff up" and so how much insulation they provide. Martins are a variety of bird. If I filled a sleeping bag with martin down and measured its puffiness, would that be... Per-Martin Loft?

• View post

  I followed the instructions from https://lean-lang.org/install/ to install lean via VSCode and create a first project with mathlib, and then I ran $ du -hs first-project/ 7.0G first-project SEVEN GIGABYTES what the fuck is going on here? who the fuck thought this was an acceptable outcome?

• View post

  I've heard of "parallel or", (x por y), which terminates with true iff either x or y does, unlike "x or y" which diverges if x does. What about "parallel and": false and x = false x and false = false true and x = x x and true = x Is there a canonical or useful reference for either of these?

• View post

  I have a new paper with @mwillsey! "Finite Functional Programming" (https://arxiv.org/abs/2604.26161) combines functional programming with relational/tensor algebra using functions of finite support: Datalog relations are finite boolean functions; tensors are finite real-valued funs. We ensure finite support of λ-terms using graded effects to check grounding, and relevance types (the "use at least once" cousin of linearity) to check relational/tensor operatio...