shachaf
@shachaf.net
What's the simplest proof of false using type-in-type? I see examples that construct Russell's paradox by modeling set theory, but that seems a bit roundabout -- is there something more direct?
October 29, 2025 at 2:47 PM
What's the simplest proof of false using type-in-type? I see examples that construct Russell's paradox by modeling set theory, but that seems a bit roundabout -- is there something more direct?
Reposted by shachaf
this is imo one of the most elegant results in distributed computing and this is a great presentation of it!
I wrote a short summary of the proof of the FLP theorem (an impossibility result about consensus). shachaf.net/w/flp
The FLP theorem
shachaf.net
September 23, 2025 at 5:20 PM
this is imo one of the most elegant results in distributed computing and this is a great presentation of it!
I wrote a short summary of the proof of the FLP theorem (an impossibility result about consensus). shachaf.net/w/flp
The FLP theorem
shachaf.net
September 22, 2025 at 4:46 PM
I wrote a short summary of the proof of the FLP theorem (an impossibility result about consensus). shachaf.net/w/flp
I knew about the trick for a queue with amortized-constant-time enqueue/dequeue/monoidal product, but I don't think I knew the deamortized version hirzels.com/martin/paper... . It's simpler than I expected (maybe because I haven't really seen deamortizations much).
hirzels.com
August 9, 2025 at 8:19 PM
I knew about the trick for a queue with amortized-constant-time enqueue/dequeue/monoidal product, but I don't think I knew the deamortized version hirzels.com/martin/paper... . It's simpler than I expected (maybe because I haven't really seen deamortizations much).
What are the biggest new things in computer science since say 2010?
August 9, 2025 at 4:29 PM
What are the biggest new things in computer science since say 2010?
Reposted by shachaf
Vague thought: Could the kinds of heuristics used in branch predictors apply to SAT solvers for choosing a literal assignment on (frequent) restarts? "phase saving" (just use the last value) is a common strategy, but does it make sense to do something more sophisticated?
July 6, 2025 at 1:05 AM
Vague thought: Could the kinds of heuristics used in branch predictors apply to SAT solvers for choosing a literal assignment on (frequent) restarts? "phase saving" (just use the last value) is a common strategy, but does it make sense to do something more sophisticated?
Vague thought: Could the kinds of heuristics used in branch predictors apply to SAT solvers for choosing a literal assignment on (frequent) restarts? "phase saving" (just use the last value) is a common strategy, but does it make sense to do something more sophisticated?
July 6, 2025 at 1:05 AM
Vague thought: Could the kinds of heuristics used in branch predictors apply to SAT solvers for choosing a literal assignment on (frequent) restarts? "phase saving" (just use the last value) is a common strategy, but does it make sense to do something more sophisticated?
Exciting news: I'm moving to London at the end of this month!
July 2, 2025 at 5:54 PM
Exciting news: I'm moving to London at the end of this month!
Is there a rank-select bitmap algorithm that I should have in my mind as "canonical" (reasonably simple and practical)? I know there are a bunch of them but I don't really know how any of them work in detail, and I vaguely remember seeing some pretty complicated constructions.
July 1, 2025 at 4:54 AM
Is there a rank-select bitmap algorithm that I should have in my mind as "canonical" (reasonably simple and practical)? I know there are a bunch of them but I don't really know how any of them work in detail, and I vaguely remember seeing some pretty complicated constructions.
I recently learned this trick to compute the modular inverse x of a mod p: Write the two equations
ax = 1 (mod p)
px = 0 (mod 0)
And then solve by subtracting multiples of one from another until you get something of the form "1x = x (mod p)", in Euclidean-algorithm-style steps.
ax = 1 (mod p)
px = 0 (mod 0)
And then solve by subtracting multiples of one from another until you get something of the form "1x = x (mod p)", in Euclidean-algorithm-style steps.
June 10, 2025 at 11:42 PM
I recently learned this trick to compute the modular inverse x of a mod p: Write the two equations
ax = 1 (mod p)
px = 0 (mod 0)
And then solve by subtracting multiples of one from another until you get something of the form "1x = x (mod p)", in Euclidean-algorithm-style steps.
ax = 1 (mod p)
px = 0 (mod 0)
And then solve by subtracting multiples of one from another until you get something of the form "1x = x (mod p)", in Euclidean-algorithm-style steps.
Reposted by shachaf
NULL BITMAP: How to Understand that Jepsen Report buttondown.com/jaffray/arch...
May 5, 2025 at 6:03 PM
NULL BITMAP: How to Understand that Jepsen Report buttondown.com/jaffray/arch...
Apparently when machine learning people say "convolution" they usually mean "cross-correlation"? It was confusing trying to make sense of the expression I was seeing!
May 4, 2025 at 10:04 PM
Apparently when machine learning people say "convolution" they usually mean "cross-correlation"? It was confusing trying to make sense of the expression I was seeing!
I really liked this perspective on atomic commit from @jaffray.bsky.social!
April 29, 2025 at 12:02 AM
I really liked this perspective on atomic commit from @jaffray.bsky.social!
What a clause in the new East coast dock worker union contract.
April 28, 2025 at 12:51 AM
What a clause in the new East coast dock worker union contract.
Reposted by shachaf
There are many concurrent systems that aren't non-blocking in a typical formal sense (e.g. obstruction-free), but are non-blocking in the sense that a thread never blocks waiting on a lock -- it can keep processing other work while it waits for things. Is there a name for that?
April 23, 2025 at 11:16 PM
There are many concurrent systems that aren't non-blocking in a typical formal sense (e.g. obstruction-free), but are non-blocking in the sense that a thread never blocks waiting on a lock -- it can keep processing other work while it waits for things. Is there a name for that?
There are many concurrent systems that aren't non-blocking in a typical formal sense (e.g. obstruction-free), but are non-blocking in the sense that a thread never blocks waiting on a lock -- it can keep processing other work while it waits for things. Is there a name for that?
April 23, 2025 at 11:16 PM
There are many concurrent systems that aren't non-blocking in a typical formal sense (e.g. obstruction-free), but are non-blocking in the sense that a thread never blocks waiting on a lock -- it can keep processing other work while it waits for things. Is there a name for that?
I was reminded of @jaffray.bsky.social's great exposition of the CVM cardinality-estimation algorithm: buttondown.com/jaffray/arch...
The CVM Algorithm
Everything you need to know about query planning can be understood from this query: SELECT * FROM xy WHERE y = 3 ORDER BY x Imagine we have two indexes, one...
buttondown.com
April 22, 2025 at 7:59 PM
I was reminded of @jaffray.bsky.social's great exposition of the CVM cardinality-estimation algorithm: buttondown.com/jaffray/arch...
I'm trying to model a distributed protocol in TLA+, and finding it kind of awkward. The basic setup seems straightforward: There are a few nodes, which have some persistent state and some in-memory state. They can't become unavailable but they might restart arbitrarily.
March 13, 2025 at 7:47 PM
I'm trying to model a distributed protocol in TLA+, and finding it kind of awkward. The basic setup seems straightforward: There are a few nodes, which have some persistent state and some in-memory state. They can't become unavailable but they might restart arbitrarily.
I wrote a somewhat meandering question about writing programs that do a lot of asynchronous operations without callbacks. I'm curious whether anyone has thoughts on this sort of thing! shachaf.net/tmp/asynchro...
shachaf.net
March 10, 2025 at 1:52 AM
I wrote a somewhat meandering question about writing programs that do a lot of asynchronous operations without callbacks. I'm curious whether anyone has thoughts on this sort of thing! shachaf.net/tmp/asynchro...
Reposted by shachaf
Sea Magic, a puzzle game about moving to cast spells, is out now!
epicpikaguy.itch.io/sea-magic
epicpikaguy.itch.io/sea-magic
Sea Magic by Ethan Clark (EPICPIKAGUY)
Move to cast spells, optimize your score
epicpikaguy.itch.io
February 22, 2025 at 5:05 AM
Sea Magic, a puzzle game about moving to cast spells, is out now!
epicpikaguy.itch.io/sea-magic
epicpikaguy.itch.io/sea-magic
Reposted by shachaf
@haroldaptroot.bsky.social after @instlatx64.bsky.social pointed me to your blog post about histogramming I showed a coworker. He was so impressed, (as was I) that he wrote his own blog post about it. github.com/JoernEngel/j...
github.com
February 15, 2025 at 2:07 PM
@haroldaptroot.bsky.social after @instlatx64.bsky.social pointed me to your blog post about histogramming I showed a coworker. He was so impressed, (as was I) that he wrote his own blog post about it. github.com/JoernEngel/j...
