gotta love staring at informative error logs. i don't care if it's jibberish, it's still better than "Exit Code: 1"

Show thread

been getting more error messages from my mac recently, which is getting me kind of excited because

(1) the error messages actually seem kind of interesting, not the usual ones i've seen

today the exception note (from Apple Music) was
EXC_CORPSE_NOTIFY

the other day i got an (from Signal)
Unhandled Promise Rejection

(2) more "reason" to retire this mac for an m1

man undergrads are awesome, fresh lil' sprouts (and a captive audience who won't mind me rambling away, or at least too nice to show it)

*Rabbit is Rich. fuck, why isn't there an edit button. this is not a civilized platform

Show thread

new city, new books

(as my mother reminds me at times, i have a problem)

i must try to ignore that i already have a copy of Rabbit of Rich in philly

Clocks/watches at museums are so cool. (Above is at the British Museum)

Speaking of which, the Patek Philippe Museum at Geneva is incredible, would recommend visiting for anyone near Switzerland (houses around 2500 watches, and also has singing(!) automatons)

Show thread

a cannon-blasting clock

"Automaton in the form of a ship, about 1585

This spectacular machine, in the form of a medieval galleon, was intended to announce banquets at court. The entertainment began with music from a miniature organ inside the hull, drumming and a procession. Afterwards, the ship would travel across the table. When it stopped, as a grand finale, the front cannon would automatically fire, lighting a fuse that would fire the other guns.

By Hans Schlottheim, Augsburg, Germany
-----------------------------------------------------

The time indicator is at the base of the main mast."

what the fuck writing ocaml has no business being this fun

i got tainted by writing too much coq during the past 3.5 years.. just stunned how easy it is to typecheck ocaml...... and the typechecker is FAST

my personal grievances with some social medias --

(1) twitter: too much noise. keep getting things i didn't sign up for regardless of how much i try to tell it to not do the thing for the 500th time (browser extensions, account settings, unfollowing, muting, blocking, .... nothing works)

(2) reddit: people tend to form a uniform "subreddit culture" that can get cultish, and depending on the subreddit if you say the wrong word or phrase the subreddit mob might find you and stone you. also for some special interest subreddits people don't seem to post interesting things that diverge much from their wiki

(3) mattermost: seems difficult to find people but i'm not sure if that's actually a disadvantage

(4) zulip: i can't read all the messages that pop up. the thread organization is nice but there's no way to filter out the feed (or is there?)

Show thread

wait types.pl mattermost is actually kind of fun and wholesome.... i'm not used to this kind of ""social media experience"" and i feel reverse bamboozled

Irene Yoon boosted
Irene Yoon boosted

One of my professors during PhD used to say “You can drive a truck through the holes in any given paper. So you look for what you *can* learn instead.” And being the smartass grad students we used to think driving that truck was fun. After so many years, I now appreciate her wisdom more than ever. All scholarly work has limitations but it’s refreshing when people critically evaluate what’s the actual value of the research. It's about humility, honesty, rigorous intellectual work.

we don't deserve proof assistants exchange. the answers are so good

Show thread
Irene Yoon boosted

bidirectional typing 

pigworker.wordpress.com/2018/0

which begins

I like my type systems to be bidirectional. Different people mean different things by the word “bidirectional”, and I’m one of them. Some people relate the notion to “polarity”, and I’m not one of them.

weirdly enough i think grad school helped with my anxiety because folks are supportive of anxious beans. thank you for looking out for local anxious bean

Show thread

anxiety is down enough to nerd out again. whew, fuck anxiety

Show older
types.pl

A Mastodon instance for programming language theorists and mathematicians. Or just anyone who wants to hang out.