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.
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*
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...
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?
I'm a real logician now! • recovering computer scientist • interested in proof theory + constructive mathematics + type theory • will only write code that compiles into a pdf document or doubles as proof
trans rights + against all unjust hierarchies