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.

Organizing Proof and Computation in Fischbachau is dangerous. I've ended up skipping a bunch of sessions to go on hikes so far and there is no sign of this stopping...

Proof and Computation is so much more fun than WoLLIC. Not only are we in the alps (very cool!), there's also tons of super interesting discussions going on around me. If I can just internalize 15% of that, I will have learned soooooo much!

I'm at the Proof and Computation autumn school now and surprisingly, the courses I enjoy the most so far were the ones I thought the lowest of from looking at the program.

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

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”

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.