dasnacl @dasnacl@types.pl

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:

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

Still, much better living conditions. :')

@maxsnew fair. care to elaborate the general idea? Because I don't really get it, but I like the scheme of somehow encoding the calling convention in the type signature :)

@maxsnew do you have any reference to this (CBPV++) or how exactly should one parse this? I'm unsure what exactly CodePtr is.
Also, should I read `A' →_eax` as `A' \rightarrow_{eax}` or `A' \rightarrow _eax`? What's the purpose of `X`?

Yeah, it's pretty neat to do regalloc at SSA level. Just make sure when destructing that you actually realize the ϕs as parallel moves and don't just add moves in the predecessor blocks, make it "on the edge" (by introducing another block)
Arguably, SSA sucks as a representation due to the "magic"ness of ϕ-functions. CPS, JWA or BWA forms are much neater in that regard, because they show you exactly how ϕs should behave