Hey @joey, what's your opinion on the fully abstract embedding criterion that these guys proposed? iris-project.org/pdfs/2021-pop
It's surely tough to scale to e.g. python, but it also surely seems like the criterion one may want to have.

I finally installed a TeX language server thing. Even though it's nothing compared to language servers for e.g. C++, Rust, or whatever, it's still an immense improvement in terms of quality of life:

Honestly, I wanted to type out some kind of list that shows what the killer features are, but the only two things I could come up with are:

  • abilty to go to a label's definition!
  • if parantheses are unmatched, i get a squiggly line

Still, much better living conditions. :')

types.pl

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