Pinned toot

Every boolean in the Agda codebase can actually be one of True, False, or An internal error has occurred. Please report this as a bug.

herculean, heroic, other h-adjectives that mean of daunting size and commanding respect for having been undertaken

Show thread

after yesterday's scare i'm back on the grind. today: getting the annotated printing PR mergeable and merging @totbwf's herculean rewrite of everything co/limit for the 1lab

We're going home now that she's been doing better for a couple hours

Show thread

doctor seems to think it's just dietary which is gonna be really "funny" when her bp is 21 over 16 again

Show thread

I'm doing some anxiety scrolling and wow. [gestures at everything], huh?

Show thread

Had to accompany my mum to the hospital so pretty-printing can take the L on this one

(She's stable)

Not gonna look at my github notifs on Sunday

CVE-2023-21036 / acropalypse is absolutely bonkers.

Apparently for 5+ years the cropping / editing tools for screenshots on Google Pixel phones was only overwriting the start of the screenshot PNG file, but not truncating.

All screenshots shared for the past 5+ years might have data recoverable from them. Demo available at

Google still hasn't communicated anything on this.

(h/t ItsSimonTime on Musk's site)

Agda developer me and Agda user me are sometimes at odds in funny ways

Agda developer me: Not using the provided built-in modules is unsupported

Agda user me: [doesn't use those, code breaks literally every other commit]

Why do I do this to myself?

i even did a thing yesterday! a minor refactor, but a thing nonetheless!

Show thread

two(?) days in a row now i slept through the entire day and woke up in the morning!

Based path induction is such a funny term to me, now. If you point it out it's implicitly a compliment, like "hey, based path induction! 😎"

Category theory is sometimes taught to computer scientists in a way that makes the most simplifying aspects of category theoretic thinking look like they are making things much harder. An example is the idea of "preserving XX up to isomorphism".

Taking products for example, we are often a bit sloppy about the difference between products as a chosen structure and as a property. Part of the reason for this sloppiness is that conventional mathematical foundations do a bit of violence to the view of products-as-property, so we need to switch between the viewpoints more often than we would ideally do.

Anyway, the point of my example is that if we tell students "This functor preserves products up to isomorphism”, what *we* mean is that “you just have to check that the image of any product cone under the functor is also a product cone" (which is usually easy and non-gnarly to check).

But because of our sloppiness, many students (and professionals!) will think we mean something like “We take it for granted that there are distinguished product cones on either side of the functor; what we want you to do is construct an explicit isomorphism between any cone in the image of a distinguished product cone with the corresponding distinguished product cone on the right side."

I'll paypal you five dollars if you can find these constraints documented anywhere in the cabal-install documentation

Show thread

I Love to find out that cabal-install will just silently add constraints to your build plan and then fucking attribute them to you. I love it when my build tool gaslights me!!!

Though the question is whether this would be worse than using valid-hole-fits in the Agda repo 🤔🤔🤔🤔

Show thread
Show older

A Mastodon instance for programming language theorists and mathematicians. Or just anyone who wants to hang out.