To answer a question people sometimes ask: https://www.type-driven.org.uk/edwinb/why-is-idris-2-so-much-faster-than-idris-1.html

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

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

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

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

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

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

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

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

- Keybase
- ionathan

- Webbed site
- https://ionathan.ch/

- Pronouns
- he/him

- Birdsite
- https://twitter.com/ionathanch/

- 🌈
- 🏳️🌈

Sometimes, when I press the flat square buttons, the lights from the glowy rectangle look nicer than usual #WaterDrinker

Joined Apr 2020