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.

Gaining some good insights from writing down these proofs. Will I finish in time for the movie night?

Lecture quote of the day:

In 1968, computers did not mostly work.

I have a vague idea using ordinal annotations that might be less weird than this?

Show thread

My source does the other half of the proof using some extremely cursed looking intersection types? And I'm not sure even sure they prove something analogous to what I need?

Turns out, the proof the authors referred to ended up being useful after all...

Show thread

All these masks putting their bacteria or dust filtration rates on the package in big, bold letters are falsely advertising IMO. Obviously they put it there for people to think they somehow protect them from the virus.

The political compass, but it's typed vs untyped and imperative vs functional instead.

Every tree without infinite branches is well-founded!!! (Assuming dependent choice on finite paths in the tree)

I'm not sure I can just throw NBE at this because the syntax is so weird...

Show thread

Haha, simply compute the bound of the depth of the reduction tree. Surely that can't be that hard... :tinking: :tinking: :tinking:

Show thread

I might have stumbled ass-backwards into having to do a normalization proof. Turns out, just throwing lambdas into the syntax of your logic is kind of a big deal?

in other maths u have to explain ur proofs to the reader who can think, but agda is brain empty

Show thread

Actually, I can constructivize parts of it. Probably enough to get the things I actually care about to be constructive...

Show thread

I have awoken to the startling realization that even though I thought I was doing proof theory, I need classical logic for my result already? That's fucked up!

Show older
types.pl

A Mastodon instance for users who like the study of programming languages, formal semantics, types, or linguistics.