This trip is making me miserable. I'm tired, I'm sad, I miss my girlfriend and I want to go home.
I helped design the metavariable handling in Aesop (Lean 4 automation). Maybe that actually ends up being my most lasting contribution, even though it probably won't end up in my thesis. Other than that,,, I've influenced the way we teach logic at DTU??
I've certainly acquired a lot of skills myself, though. Maybe I should focus on that.
Like, the game itself —both intentionally and unintentionally— the make-believe, everything.
Imagine, extreme-case scenario, a disabled, autistic kid with tourettes, social anxiety and schizophrenia. I do not have the energy to support them as they deserve to be supported.
PhD student in logic. Isabelle/HOL user. Lean dabbler. she/her
A Mastodon instance for programming language theorists and mathematicians. Or just anyone who wants to hang out.