pounce boosted

also:
I think the heart of free software is really great!! It's just... some of the people....

Show thread

postdoc im reading HoTT with: the best way to connect with other mathematicians outside of school is to make a math twitter

nooooooo

tfw forgot how to homotopy theory when doing homotopy type theory

aaaaa why is the only wikipedia citation to this a website from 2003 archived in the wayback machine with all the links to proofs broken

logic thonk 

ok, so set theory relies heavily on second-order logic to function, and second-order logic/set theory are two main levels on top of which most of mathematics is built, right?

i see type theory as championed by not having this hierarchy by "properties-as-types", however all the type theories i've seen have "judgements" of typing rules and equality that dictate how the type theory function. Is this not also a "two-level hierarchy" on which type theory is built? or am i thinking about the relationship wrong

me: Julia what's typeof(f)
Julia: typeof(f)
me:.... yes that's what i asked

ok while we're talking about go can i complain about how long it takes `vim-go` to update all of its binaries when every other plugin updates instantly
for a language that prides itself on fast compile time it's pretty sad

pounce boosted

if you need to design an entire templating tool for a language solely to work around its shortcomings or eliminate boilerplate, your language sucks

pounce boosted

i am so tired of listening to people designing tools to clean up after Go's failings

ayyy my alpha beta search works on the first time
i win against the executable they gave us 77% of the time

why does it figure out judgemental equality for lambdas but not functions in `where` blocks

Show thread

grrr why is the lean typechecker so dumb

consumerism 

i kinda want a tablet to take notes on since i keep using my partner's during calls
is that a bad idea :thonking:

i have just. done my third talk on lean
i don't even use lean for any reason except it's somewhat easier to write fast code in than agda

why do ppl keep asking me to talk about it 🙃

maybe if i make some hōjicha i'll finally be able to read that Escardó paper that's been sitting on my bedside table since december

i feel like i need to make one of those "we have been played for absolute fools" memes about category theory

HoTT exercises 

hmmm
2.1/2.2 is kinda getting me. So I have to prove equality of these three proofs using path-induction
but clearly they don't use path induction in the same way, so they aren't judgmentally equal.
But each of these are functions, so don't I need funext to prove non-judgmentally-equal functions as equal?

Show older
types.pl

A Mastodon instance for users who like the study of programming languages, formal semantics, types, or linguistics.