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.

Finally, some of my own thoughts. I firmly believe that the value that #chatGPT and similar models deliver to society is negative. Being able to generate at the press of a button plausibly and smart sounding content that might be wildly but subtly incorrect, with no citations, no sources, no indication of providence, is a recipe for poisining the information environment.

I see programmer types concluding that this will "replace programming" and "make us obsolete". I find it shocking that folks have such a low view of their own profession. The worst, most dangerous code isn't code full of bugs. It's code that "works", but that is incorrect in ways that are pernicious but not obvious.

The job of a programmer also isn't to reproduce some algorithm, it's to understand and model the world, to understand and anticipate user needs, it's to collaborate and shepherd a code base over a prolonged period of time. No language model will do these things.

To quote someone who's very dear to me: "PEOPLE AREN'T USING THEIR BRAINS". Please, use your brains, and be grateful for all the things it can do that a pattern matching model can't.

Show thread

i bought a whiteboard and it's great! i can leave little thoughts for later
sadly later-me usually judges the thoughts to be garbage

my most productive procrastination of the year: finally finished the translation of EGA II. this means that EGAs I and II, along with the corresponding chapters of EGA 0, are now fully available online*

*if you're really early seeing this, then you'll have to wait until the next o'clock in order for the PDFs for EGA II to autobuild

p.s. as you might see in the picture, I've only proofread the very first section — I'll come back to do a full proofread eventually!

That one meme of Mr. Incredible getting uncannier, but it takes just one step; the normal one is labelled "functor composition" and the screwed-up on is labelled "profunctor composition"

Okay maybe this should be done automatically though

Show thread

nvm you can do this by naming the where module and putting the display pragma outside

Show thread

... I also want a way to, when you have something like

foo = bar where
... bar ...

have bar DISPLAY as foo

My kingdom for a way to make case-split introduce as many variables as there are pis after a copattern split

screenshot without description 

Recovering from type errors is totally doable actually

Implementing the rest of "unifiers as equivalences" is on that latter bucket, for now. Injectivity and especially higher-order unification terrify me. I guess it might be a bit easier since we're only really worried about "unifiers as retractions" 🫠🥴

Show thread

Always very happy when I see a new bug and think, "that's an easy bug" — and the bug turns out to be easy! Conversely it's bittersweet when I think the bug will be a nightmare and it actually is...

I'm sure I had a use-case for it apart from lossy unification for projections

Show thread

Oh right I'm thinking about the FIRSTORDER pragma again. or maybe LOSSY or something

No working on Agda on the weekends no working on Agda on the weekends stop thinking about metavariables and simplifying interval expressions

Really the thing is making it lazy. It should be possible to request only the exported names by a module (in a fast way!), and then when the names are needed, block on the decoding/checking of the definitions in that module. Really I'm thinking of

Show thread

Once again plagued by thoughts of how to make Agda parallel

Show older

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