Hey @joey, what's your opinion on the fully abstract embedding criterion that these guys proposed? https://iris-project.org/pdfs/2021-popl-fae-gradual-final.pdf
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:
Still, much better living conditions. :')