me: i love type theory
me: *uses a proof assistant*
me, through pained breath: man

oh my god

can you seriously not eliminate prop into set

fuck you *one-point compactifies your space*

hazel boosted

i could solve the halting problem easily, but certain people have been a bitch to me, so i wont

"Secret sigma they keep locked away" - @ionchy

hazel boosted

@hazel "oh look at me I'm half the base of base 10 I'm easy to do arithmetic with and I'm a prime number" ass little bitch. Gonna shove 5 into a locker

i just. i just want the fucking squimsher. give me the fucking Set -> Prop squimsher.

"how do I do X?"
"solve the halting problem"
"god damnit"

a conversation I have had on 5 separate occasions this month

hazel boosted

sorry but if you make it to year 3 of CS and your take is that anything is computable you're a complete fucking moron. it's like being a year 3 geologist and thinking the earth is flat

I think that less numbers should be prime

hazel boosted

Q: what is the loneliest number

A: 5 because it's a dipshit idiot loser. lol

#conservativecomedy

-- Quotient types:
-- I don't entirely understand what these do.

If I leave then Jonathan gets full control of types.pl, or I find a replacement for myself.

This isn't a commitment to leaving, but it's possible.

I really appreciate the community I've built here, thank you all for sticking with a random undergrad's rented Ubuntu server.

If you want to talk, my contact info's public. If I want to talk to you, though, you should already have that information somewhere.

I might leave Mastodon entirely. If I do, I'm not going to shut down types.pl, and I'll continue paying for its hosting.

quick note to all: I haven't posted here in a while because I've pretty much felt exclusively like human garbage for about a week.

It's only been amplified lately because uh. circumstances. whatever.

indiana university bloomington fun facts

our CS2 is an irredeemable burning hell

$\varphi$ bouba. $\phi$ kiki

Show older

#### hazel 's choices:

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