­jonoodle­ @ionchy@types.pl

Blocks as a programming language... pistons that "run" the blocks...

Redstone compiler

just writing it out is so much easier and I can see what I'm doing

he has it all written out nicely like this. I would hate it tbh

wait they work at github??

okay maybe they're not perfect after all

The other day I saw someone had a blog with inference rules that were written entirely using HTML tables and styled with CSS and it wasn't compiled down to that or anything, I took at look at their Markdown files and they just have HTML right in there
I should steal their CSS someday

The P is silent

It's been so long since I've pulled Idris that they changed the branch name to main and I didn't notice

It wasn't interesting so I didn't

We're definitely discussing the same thing
It's just that everything is categoric in his head and everything is syntactic in mine

I'm mentally translating every instance of "coproduct" to "sum type" and "colimit" to "smth smth inductives probably"

We're getting warmer

I'm convinced I'd understand him perfectly if he used different words

The things Jon Sterling says

Thinking about implementing Girard's paradox in Coq

I am simply tired