Tulip @hazel@types.pl

I would like to emphasize to everyone that I understand literally nothing and none of my word can be taken as authority on anything

thank you

This message was sent from a non-IU address. Please exercise caution when clicking links or opening attachments from external sources.

reposting this from old account so I can pin it

welcome to PL mastodon we have
- nobody

please lord have mercy

doing parametricity proofs with logical relations by hand has me feeling a certain way

bad
the way is bad

she ∀X.∀Y. on my (X × Y) → X til i ΛX.ΛY.λ(p : X × Y).p X (λ(x:X).λ(y:Y).x)

what's up

hey you

hey

she logic on my relation till I observational equivalence

if you think about it type theory is just Homestuck

anyway don't @ me I'm literally just a rabbit

if this generalized passive aggressiveness in the form of moderation policy and defense to it angers you, please consider:

- why does this make me angry?
- am I one of those bigoted figures? how would I know?
- would migrating instances be a good idea, or would it merely cause me to be banned somewhere else?
- if I am a professor, what do my students think about me?
- if I am a student, what would people think about me as a professor?

not only that, but I think it's very important that the moderation team assembled here is entirely comprised of groups in a similar vein who run in contrast with bigoted figures in the programming languages community, because in essence when running types.pl I am creating a space *I* feel safe in, and when mixed with the intersections of other moderators it turns into a space that a large swath of people feel safe in.

I am very okay with the idea of dividing the PL community into an explicitly leftist space being the hill that my entire career dies on.

breaking my month-long depressive silence to state:

this was the plan all along, actually. I am being purposefully inflammatory. the entire idea was to centralize the PL community in one place and irrevocably intertwine it with revolutionary politics via moderation policy that reflects that, ergo creating a schism in the community that needs to be addressed as a whole in order for marginalized groups to find their place within it.

in essence, if you disagree with our moderation policy, you've more or less put yourself on a list of people who marginalized groups interested in programming languages know to avoid.

i think

no this is not a thing that is actually happening

academia win! they say the next bombs they drop on a country you've never heard of will be formally verified to hit with coq

End of lecture today:

"So if anyone doesn't have anything better to do over break, I'm going to eventually assign reading *Towards Observational Type Theory*, by Conor McBride.
Also, all the proofs in *The Little Typer* should now seem trivial, if you need more general examples of dependent types.

"Make sure to have Agda 2.6.2 installed before next lecture.

"Also, if you have nothing better to do over break, you could read Homestuck. I'm not sure why you would. But you definitely could."

Break time!

Just finished up 9 weeks of lecturing about type theory implementation.

Ow.

[thunderous applause]