Alecs P. Hacker
LightNews LightNews
bisimulation.bsky.social
Alecs P. Hacker
@bisimulation.bsky.social
79 followers 60 following 910 posts
liquid type in liquid type connoisseur
alecsferra.github.io
Posts Replies Media Videos
bisimulation.bsky.social
Nine what?
November 9, 2025 at 5:03 PM
bisimulation.bsky.social
I'm going to get killed by the machine god when we make AGI
November 3, 2025 at 12:53 PM
bisimulation.bsky.social
Literally me
Soyjack that loves types
October 20, 2025 at 3:07 PM
bisimulation.bsky.social
I'm cooked
October 15, 2025 at 3:16 PM
bisimulation.bsky.social
Btw just discovered this
Jonathan blow blocked me on twitter
October 8, 2025 at 9:45 PM
bisimulation.bsky.social
Its just fun
October 7, 2025 at 6:02 PM
bisimulation.bsky.social
@haskell.org its time to get a mascot
October 5, 2025 at 7:43 PM
bisimulation.bsky.social
The famous dragon book
October 5, 2025 at 3:02 PM
bisimulation.bsky.social
I love twitter
Twitter thread U1: *screenshot of a GitHub repo by palantir "palantir/palantir-java-format" U2: Unironically one of my favourite pices of software we've made Me: I bet mass surveillance software is also pretty fun U2 blocked me
September 23, 2025 at 8:19 AM
bisimulation.bsky.social
Why is mathpartir adding space at the bottom???
September 18, 2025 at 9:43 AM
bisimulation.bsky.social
Can you please implement rotateCorrect?
{-@ LIQUID "--reflection" @-} {-@ LIQUID "--ple" @-} module TuringTest where import Language.Haskell.Liquid.ProofCombinators {-@ measure length' @-} {-@ length' :: [a] -> Nat @-} length' :: [a] -> Int length' [] = 0 length' (x:xs) = 1 + length' xs {-@ reflect take' @-} {-@ take' :: n:Nat -> { xs:[a] | length' xs >= n } -> { xs:[a] | length' xs = n } @-} take' :: Int -> [a] -> [a] take' 0 xs = [] take' n (x:xs) = x : take' (n - 1) xs {-@ reflect drop' @-} {-@ drop' :: n:Nat -> { xs:[a] | length' xs >= n } -> { ys:[a] | length' ys = length' xs -n } @-} drop' :: Int -> [a] -> [a] drop' 0 xs = xs drop' n (x:xs) = drop' (n - 1) xs {-@ reflect concat' @-} concat' :: [a] -> [a] -> [a] concat' [] ys = ys concat' (x:xs) ys = x : concat' xs ys {-@ reflect rotate @-} {-@ rotate :: n:Nat -> { xs:[a] | length' xs >= n } -> [a] @-} rotate :: Int -> [a] -> [a] rotate n xs = concat' (drop' (length' xs - n) xs) (take' (length' xs - n) xs) {-@ reflect lookup' @-} {-@ lookup' :: n:Nat -> { xs:[a] | length' xs > n } -> a @-} lookup' :: Int -> [a] -> a lookup' 0 (x:xs) = x lookup' n (x:xs) = lookup' (n - 1) xs {-@ rotateCorrect :: o:Nat -> i:Nat -> { xs:[a] | i < length' xs && o <= length' xs } -> { lookup' i xs = lookup' (i + o mod length' xs) (rotate o xs) } @-} rotateCorrect :: Int -> Int -> [a] -> Proof rotateCorrect = undefined
September 11, 2025 at 4:10 PM
bisimulation.bsky.social
I devised my own Turing test
{-@ LIQUID "--reflection" @-} {-@ LIQUID "--ple" @-} module TuringTest where import Language.Haskell.Liquid.ProofCombinators {-@ measure length' @-} {-@ length' :: [a] -> Nat @-} length' :: [a] -> Int length' [] = 0 length' (x:xs) = 1 + length' xs {-@ reflect take' @-} {-@ take' :: n:Nat -> { xs:[a] | length' xs >= n } -> { xs:[a] | length' xs = n } @-} take' :: Int -> [a] -> [a] take' 0 xs = [] take' n (x:xs) = x : take' (n - 1) xs {-@ reflect drop' @-} {-@ drop' :: n:Nat -> { xs:[a] | length' xs >= n } -> { ys:[a] | length' ys = length' xs -n } @-} drop' :: Int -> [a] -> [a] drop' 0 xs = xs drop' n (x:xs) = drop' (n - 1) xs {-@ reflect concat' @-} concat' :: [a] -> [a] -> [a] concat' [] ys = ys concat' (x:xs) ys = x : concat' xs ys {-@ reflect rotate @-} {-@ rotate :: n:Nat -> { xs:[a] | length' xs >= n } -> [a] @-} rotate :: Int -> [a] -> [a] rotate n xs = concat' (drop' (length' xs - n) xs) (take' (length' xs - n) xs) {-@ reflect lookup' @-} {-@ lookup' :: n:Nat -> { xs:[a] | length' xs > n } -> a @-} lookup' :: Int -> [a] -> a lookup' 0 (x:xs) = x lookup' n (x:xs) = lookup' (n - 1) xs {-@ rotateCorrect :: o:Nat -> i:Nat -> { xs:[a] | i < length' xs && o <= length' xs } -> { lookup' i xs = lookup' (i + o mod length' xs) (rotate o xs) } @-} rotateCorrect :: Int -> Int -> [a] -> Proof rotateCorrect = undefined
September 11, 2025 at 10:46 AM
bisimulation.bsky.social
Will cake fix my POPL reviews depression?
Basque cheesecake
September 9, 2025 at 4:32 PM
bisimulation.bsky.social
A two-panel meme. On the left, titled "Strongest Postcondition, with a skinny guy. On the right, titled "Weakest Precondition," the giga chad
September 9, 2025 at 7:35 AM
bisimulation.bsky.social
Overfull hbox experience
September 5, 2025 at 9:38 AM
bisimulation.bsky.social
Has Gen AI peaked?
August 29, 2025 at 10:06 AM
bisimulation.bsky.social
This is what peak typesetting looks like
Worst typesetting ever idk what to put in the alt text
August 28, 2025 at 10:26 AM
bisimulation.bsky.social
What kind of sit is this
August 27, 2025 at 5:30 PM
bisimulation.bsky.social
Temperature check
The glue that keeps my phone together gave up
August 22, 2025 at 2:28 PM
bisimulation.bsky.social
The only good thing about this book is the drawing on the front
August 20, 2025 at 8:01 PM
bisimulation.bsky.social
2 people carrying a third >what happened to him? >He tried to prove logical soundenss
August 18, 2025 at 6:33 PM
bisimulation.bsky.social
Chinese pepsi tastes way different from the European one
A Chinese pepsi can
August 16, 2025 at 8:59 AM
bisimulation.bsky.social
August 14, 2025 at 2:52 PM
bisimulation.bsky.social
Fixixed the names now I need to figure out how to print positivity checker instead of termination checker and the lie is completed
July 12, 2025 at 11:58 AM
bisimulation.bsky.social
Added back support for polarities now I will go touch grass
July 11, 2025 at 7:17 PM