Pinned toot

Driven out of Cantor's paradise and thrown into setoid hell.

Pinned toot

I do math because it means I need to do less annoying garbage than when programming. I do Proof Theory because I'm still an annoying garbage doer at heart.

Pinned toot

Here's the quote justifying my weird username. It's from Dedekind's "Was sind und was sollen die Zahlen" ("What are numbers and what are they good for?").

"But I know that, in the shadowy forms which I bring before him, many a reader will scarcely recognize his numbers which all his life long have accompanied him as faithful and familiar friends; he will be frightened by the long series of simple inferences corresponding to our step-by-step understanding [ger. Treppenverstand], by the matter-of-fact dissection of the chains of reasoning on which the laws of numbers depend [...]"

The term thus characterizes our capability of reasoning to be restricted to discrete steps and is meant to contrast the rather informal, intuition-based proofs that were the norm back in 1888 when the paper was written.

It is also a very funny sounding word.

Do conferences involve lots and lots of drinking for everyone or is that just me?

You know what sucks? Research. You know what I love? Research. You know what I wanna do? Research. You know what I don't wanna do? Research.

On a conference all alone and it is *scary*. Sleeping alone in the forest at night has nothing on this lol.

“Put a computer in everything” is one of those decisions that people 100 years from now will bring up to show how backwards we of the past were, the way we do with decisions like “make water pipes out of lead” and “put cocaine in cough drops”

re: POPL review commentary 

Mechniazation != formalization I will die on this hill.

Show thread

I wish people would stop saying stuff like "the set X is recursive" and instead say "X is in Sigma_1". But that's probably super taste dependent.

An excerpt of the last Haskell meetup:

Haskeller 1: So the data structure became to complex, there was too much redundancy, and it just wasn't ergonomic to use anymore! We started using GADTs and overloaded records!
Haskeller 2: You should use lenses! Prisms! Traversals! Template Haskell!
Newcomer: Hey, what do you guys use for databases? ORM?
*crickets chirping*

I'm barely halfway through creating the presentation and already at 20 slides! I only have 1 hour for my talk so it might get tight!

Effective altruists not downplay the existential risks of climate change in order to claim their pet interest is the most moral problem to work on challenge (impossible difficulty)

Also, it seems if I don't have to fight TeX my layouts get pretty unhinged. Not sure how easy this will be to follow...

Show thread

Like, drawing pictures is *much* faster than tikzing but writing is also much slower than typing. The idea was to have many pictures and little text, so maybe it will work out?

Show thread

Trying out hand-drawn slides for my next talk. Not yet sure of they're more efficient to create...

Show older
types.pl

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