It's kind of nice tuning into a Zoom call without actually participating, it's like sitting in the same room as other people who happen to be having an interesting conversation

To answer a question people sometimes ask: type-driven.org.uk/edwinb/why-

In which I explain several bad design decisions I made several years ago...

I've seen three ppl write "à la" as "ala" now
Is this an American thing

Alternative wishlist course: HoTT. That's it, it's just teaching HoTT directly from the book

Show thread

When I visited McGill I got to drop in on a course and that class was discussing a paper on temporal type theory and it was big confusing, but I think if I understood the logic part of it I could've more easily grasped the typey part of it

Show thread

If I could wish up a course it'd probably be a logic/type theory course
Probably half lecture, half seminar style
Start with lectures on nonclassical logics (modal, linear, temporal, whatever) and then read the big papers (assuming there are any) that establish the corresponding type theories

Show thread

I wonder if I can take grad courses outside of CS... I probably just have to ask
If I have to take eight (!) courses or whatever with a set amount of them for a "breadth" requirement I might as well take something I'm actually interested in, like quantum mechanics, instead of a random AI/ML course to arrange my timetable
Pity there are only so many PL courses to take

It's kind of hard to tell how many puzzle pieces you want to provide the reader with when writing a paper proof
I'm glad I don't need to meticulously put all the pieces together though, unlike a mechanized proof

Show thread

The list is in a weird order because I typed them out in the order I followed the derivation tree in my head depth-first lol

Show thread

Same energy as "Therefore, Equation 9 clearly holds", just with more words

My entire face was itching and I kept sneezing despite having taken two allergy pills, until I left the house and I gradually stopped sneezing, so I think I'm allergic to quarantine

There's a _≡˘⟨_⟩_ operator that does that, it applies `sym` to the proof

Show thread

Neato
I wish `rewrite` could try applying either of the provided proof or its `sym` though, I can never remember which way `assoc` is defined

Show thread

pleas... I just want to do some induction... why won't things load properly by themselfs...

Show thread

stocks are FAKE
property value is FAKE
the economy is FAKE
the only REAL thing is: cat

Oh I love Agda input mode so much. I possess the power of all the Unicode symbols

Show thread

They need an Agda Tutorial For Abosolute Dunces, because I have no idea how to do anything

Show thread
Show more
Scholar Social

The social network of the future: No ads, no corporate surveillance, ethical design, and decentralization! Own your data with Mastodon!