Alright, I have a hard time following some of these papers because of the wording. Does this basically mean the language is immune via the compiler to failures or attacks from abstraction gaps between what high-level language shows and what low-level target actually does? Or something else entirely?
1. That any two source programs are equal exactly when their translations are equal. So FA is parametrised by two notions of program equality, one for the source, one for the target.
2. That the source and target language are substantially different.
Requirement (2) is vague and is supposed to rule out "term models", eg. translations from a language to itself. There have been many FA results since the concept was introduced in the 1970s (I think). It's close to soundess / completenss of logic.
I mean equal w.r.t. a chosen notion of equality. So for any pair (==s, ==t) of notions of equality, there is a different notion of full abstraction. Here ==s relates programs of the source language and ==t relate programs of the target language.
> Does this basically mean the language is immune via the compiler to failures or attacks from abstraction gaps between what high-level language shows and what low-level target actually does?
You're on the right track here. There's a very intuitive definition for 'compiler correctness':
Take any program in the source language and the corresponding target language program that a compiler gives you. Now run both programs using the semantics for the languages that each program is written in. If doing this gives you two equivalent results for all valid source programs, then your compiler is correct.
Assuming you have a good definition of 'equivalent results', this definition works very nicely for whole program compilers like the original work on CompCert. But what if you want to compile a component on its own, and then link it with a program later? It's not even obvious what correctness should mean if you support separate compilation because you can't 'run' a component.
It turns out there are different kinds of guarantees you might want to make about a compiler that constitute what is referred to as 'compositional compiler correctness'. Full abstraction is one of the strongest such guarantees. The abstract for this paper says that full abstraction means 'two source components are observationally equivalent in the source language if and only if their translations are observationally equivalent in the target'.
The key concept in this definition is the idea of 'observational equivalence'. We can say that two components C1 and C2 are observationally equivalent if for all programs P, there is no way for P to tell C1 and C2 apart; it must behave the same when linked with either one. That is, all of the observations that P can make about the component it's linked with are the same for both C1 and C2.
[1] (mentioned by the LtU post) talks a bit more about full abstraction and shows some issues that can arise when compilers accidentally break full abstraction. On the other hand, there are cases where it's impossible to write a fully abstract compiler. For example, if you have reflection in your target language but not your source language, it's likely that target level programs will always be able to distinguish between components which were equivalent in the source language. [2] is a good overview of many of the issues for those interested in compositional compiler correctness.
