johnbender

A key problem is that compilation operates on an implicit (compiler writers have this in the back of their heads) notion of correctness which is very roughly “preservation of observable behaviors” where “observable” is sequences of system calls and then return value. That is, the final output of a compiler should never add new sequences of observable behaviors.

Security properties on the other hand are very often about the relationship between these sequences. For example we like to say that an external observer/attacker can’t distinguish internal state by the external observations (confidentiality) which requires that two observable traces given different hidden values don’t have different observations from the same starting observable state.

If you’re an LTS nerd you know this difference as trace properties vs hyper properties. Compilers try to preserve the former but not the latter.

Separately there is the problem of “what is observable?” For example, if you include timing in your observable behaviors suddenly the kinds of compiler passes that are able to preserve observations tends to zero rather quickly.

It depends on what “confirmed identical” means. Most compilers (or translators as you like) only guarantee that the output program represents a subset of the behaviors of the input program so it could be that subset is the “safe as in Rust” subset.

I’m confused by the calculus example and I’m hoping someone here can clarify why one can’t state the needed assumptions for roughed out theory that still need to be proven? That is, I’m curious if the critical concern the article is highlighting the requirement to “prove all assumptions before use” or instead the idea that sometimes we can’t even define the blind spots as assumptions in a theory before we use it?

In principle (and we hope in practice) the person is still responsible for the consequences of running the code and so it remains important they can read and understand what has been generated.

You have identified the crux of the problem, just like mathematics writing down the “right” theorem is often half or more of the difficulty.

In the case of digital systems it can be much worse because we often have to include many assumptions to accommodate the complexity of our models. To use an example from your context, usually one is required to assume some kind of fairness to get anything to go through with systems operating concurrently but many kinds of fairness are not realistic (eg strong fairness).

Compilers don’t do this error free of course BUT if we want them too we can say what it means for a compiler to be correct very directly _one time_ and have it be done for all programs (see the definition for simulation in the CompCert compiler). This is a major and meaningful difference from AI which would need such a specification for each individual application you ask it to build because there is no general specification for correct translation from English to Code.

FM day job:

Interpretation of SysML activity diagrams as temporal logic for use with state machine specifications.

Module system for state machine with scoping, ownership type system and attendant theorems to carry proofs of LTL properties about individual parts forward after composition.

At the outset the article rather bizarrely casts the subject circumstances as a matter of government incompetence in its design and execution of an identification standard as opposed to the reality it then reports on which is DHS tripping over itself to justify unlawful detention of US citizens without cause.

Formal methods like TLA provide the highest value when you have a property of the system that is subtle but should be comprehensive, which is to say you need to know it’s true for all the behaviors of the system. (Aside: this is true even if you never model check the system because modeling is a good forcing function for clarity in understanding of the system)

With that in mind you don’t have to model your whole system as long as you’re comfortable with the boundaries as assumptions in any property/theorem you prove about it! For example, unconstrained variable in a TLA spec do a reasonable job of modeling an overapproximation of inputs from the outside world, so that’s one boundary you could potentially stop at supposing the your proof can go through in that chaotic context.

Minor nit:

> The job of a compiler error message is to prove to the user that their code is invalid

The job of the compiler error message is to convey why the compiler couldn’t demonstrate the code is correct. The code may be valid but the compiler just can’t prove it (analyses are sound but not complete unless the language is strongly normalizing)

> Besides, gotta start somewhere. It's probably a PoC, for a platform that will eventually handle all sorts of things.

I agree and I think we should give folks leeway to make progress but this seems to be the qualifier for nearly every GenAI demo I’ve seen