Pinned toot

$\mathcal{things ~ are ~ just ~ other ~ things}$

Pinned toot

✨ 𝓲𝓽 𝓲𝓼 𝓪𝓵𝔀𝓪𝔂𝓼 𝓪𝓵𝓵 𝓽𝓱𝓮 𝓽𝔂𝓹𝓮𝓼 ✨

Pinned toot

"Computers are rocks we tricked into thinking" is entirely incorrect. Computers are rocks we tricked ourselves into believing they could think

Pronouncing BBNO$ like mathblackboard{NO} missing $ inserted

re: Advent of Code day 1 

(rest (rest (rest input)))... that is cdddr

Show thread

re: Advent of Code day 1 

a b c d
a b c
b c d
1 2 3 4

yeah... first and fourth

Show thread

re: Advent of Code day 1 

Or.. first and third? I can't count

Show thread

re: Advent of Code day 1 

If I take the sum of three elements and then subtract the sum of the three elements one element before it, isn't that just the difference between the first and fourth elements

Show thread

What if I dragged people in the lab into AoC

Advent of Code day 1 

Unfortunately I have done it

no no no I can't do AoC this year. I have applications to finish and a paper to edit

Show thread

Tomorrow's task: make this pretty and hopefully take also makes it clear
Tonight's task: ...well I've already played Minecraft so idk

Show thread

I regret to announce that in an attempt to clarify, I have instead obfuscated

Show thread

Am I suppose to understand the algorithms I use? Haven't understood it for two years I don't think I'll start understanding now

Show thread

I've looked at a few others' statements and for some reason they're full of Things They've Done
Like the first page will just be entirely describing the work they've done
I mean I did the same, but my master's statement was definitely not half full of what I've done

Show thread

Okay took me long enough to add just a little bit of technical material and to finalize the non-technical stuff
I'll print them out, let them sit, and then submit tmrw

Show thread

Furthermore it might be the case that one cannot compile full cubical type theory without some kind of performance overhead, due to the fact that some computation rules involve computation under binders.

Isn't normalization of the body of a lambda computation under a binder? I guess running a program just never does that? ??

Show thread

We restrict certain cubical features: Glue and higher constructors may only be used in code
that will be erased by the compiler.

I guess this is the same as saying no computational behaviour relies on the cubical bits

Show thread

How exactly do you get a dependently typed language compiler that is correct wrt to programs running to equivalent outputs but with erased types

Show thread
Show older
types.pl

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