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.

catching up with recent developments in AI (Automated Inductive proofs), ML (Marxism-Leninism) and CV (Cuantified Variables)

Little attention has been paid to notions of liberty and fraternity in dependent type theory, but the same cannot be said about equality.

ba-dum tss

Turns out people *have* been doing stuff similar to what I am doing.

Show thread

Relearning a lesson I should've already learned from my Bachelor's thesis: I should've done my literature review earlier!

Attended a really cool talk today which makes up for all of the subpar one of the past 2 weeks.

Didn't even finish that proof today. I'll probably have to work over the weekend now :./

To top it all off, this is most likely gonna go into an appendix, never to be seen again.

Show thread

I cannot fathom how people doing pure category theory or algebra enjoy this stuff. This is pure torture to me.

lobste.rs is just hackernews for people who want to think they hate hackernews but don't want to give it up

I've spent like 2 hours today on (what feels like, to me) pure category theory and I hate it. Is this the price you pay for nice definitions?

you, a pedant, a fool: e^x
me, enlightened: exp(x)
god himself descending from the heavens: arcln(x)

LRT: This is what applied category theory sounds like to me.

chess is dark souls. riding a bicycle is the snyder cut of monster hunter. kicking a can down the street is the fight club of pulp fiction meets tetris, and orwellian

I'm looking for a template/document style for a pretty thesis. I don't need a title page (the institute provides that) just nice styling for the actual content.

Today is my first day of thesis writing.. Let us see how it goes, both fun-wise and pages-per-day-wise...

Checking this by hand would've taken me much longer because I would first have to read and understand all of the proofs again.

Show thread

So I had these results about a system (from a project from last summer actually, what is time?) but I needed to change some of the definitions to have a chance at publishing them. Fortunately, I formalized everything in Coq, so this evening, I adjusted the definitions and all proofs went through (with minor modifications). Thank you Coq and thank you past me!

Show older
types.pl

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