That’s a great write-up. One potential improvement would be moving the example of why one needs fully-abstract computation to the beginning. Many people don’t know why they’d need it in the first place. They might skip the article if it takes too long to figure that out.
They wrote a compiler from F* to JavaScript and proved full abstraction in Coq. It is kind of amazing, considering that full abstraction means it is secure and immune from changes to Object.prototype, etc.
Just a minor correction – that paper is for a language called “f*” (a little f, not a big F), which is a much much smaller language (no dependent types, for example) than F*. It’s an unfortunately close name, as it can be confusing!
Are you looking for industrial / “large” compilers? The answer to that is no (or, not yet… there didn’t used to be any realistic correct compilers either, so…).
As yet, most of the fully abstract compilers that exist are for small languages, in addition to the f*->JS one you mentioned, Devriese et al built one from the simply typed lambda calculus with recursion to the untyped lambda calculus (pdf), and people in my group have built a couple – e.g., from a lambda calculus with recursive types to a language with exceptions (pdf), from a language with information flow properties into F omega (pdf), etc. And of course there are probably others that I don’t know about!
That’s a great write-up. One potential improvement would be moving the example of why one needs fully-abstract computation to the beginning. Many people don’t know why they’d need it in the first place. They might skip the article if it takes too long to figure that out.
Do people know of any fully abstract compiler? The only one I know of is Microsoft Research’s Fully Abstract Compilation to JavaScript.
They wrote a compiler from F* to JavaScript and proved full abstraction in Coq. It is kind of amazing, considering that full abstraction means it is secure and immune from changes to Object.prototype, etc.
Just a minor correction – that paper is for a language called “f*” (a little f, not a big F), which is a much much smaller language (no dependent types, for example) than F*. It’s an unfortunately close name, as it can be confusing!
Are you looking for industrial / “large” compilers? The answer to that is no (or, not yet… there didn’t used to be any realistic correct compilers either, so…).
As yet, most of the fully abstract compilers that exist are for small languages, in addition to the f*->JS one you mentioned, Devriese et al built one from the simply typed lambda calculus with recursion to the untyped lambda calculus (pdf), and people in my group have built a couple – e.g., from a lambda calculus with recursive types to a language with exceptions (pdf), from a language with information flow properties into F omega (pdf), etc. And of course there are probably others that I don’t know about!