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 calculus the core issue is that the concept of a "function" was undefined but generally understood to be something like what we'd call today an "expression" in a programming language. So, for example, "x^2 + 1" was widely agreed to be a function, but "if x < 0 then x else 0" was controversial. What's nice about the "function as expression" idea is that generally speaking these functions are continuous, analytic [1], etc and the set of such functions is closed under differentiation and integration [2]. There's a good chance that if you took AP Calculus you basically learned this definition.
The formal definition of "function" is totally different! This is typically a big confusion in Calculus 2 or 3! Today, a function is defined as literally any input→output mapping, and the "rule" by which this mapping is defined is irrelevant. This definition is much worse for basic calculus—most mappings are not continuous or differentiable. But it has benefits for more advanced calculus; the initial application was Fourier series. And it is generally much easier to formalize because it is "canonical" in a certain sense, it doesn't depend on questions like "which exact expressions are allowed".
This is exactly what the article is complaining about. The non-rigorous intuition preferred for basic calculus and the non-rigorous intuition required for more advanced calculus are different. If you formalize, you'll end up with one rigorous definition, which necessarily will have to incorporate a lot of complexity required for advanced calculus but confusing to beginners.
Programming languages are like this too. Compare C and Python. Some things must be written in C, but most things can be more easily written in Python. If the whole development must be one language, the more basic code will suffer. In programming we fix this by developing software as assemblages of different programs written in different languages, but mechanisms for this kind of modularity in formal systems are still under-studied and, today, come with significant untrusted pieces or annoying boilerplate, so this solution isn't yet available.
[1] Later it was discovered that in fact this set isn't analytic, but that wasn't known for a long time.
[2] I am being imprecise; integrating and solving various differential equations often yields functions that are nice but aren't defined by combinations of named functions. The solution at the time was to name these new discovered functions.
> If you formalize, you'll end up with one rigorous definition
Can't you just formalize both definitions and pick the one to work with based on what you want to do? Surely the only obstacle here is the time and effort it takes to write the formalization?
Or, alternatively, just because you've formalized the advanced calculus version doesn't mean you need to use the formalization when teaching basic calculus. The way we've proven something and the way we teach that something don't have to be the same.
> the concept of a "function" was undefined but generally understood to be something like what we'd call today an "expression" in a programming language. So, for example, "x^2 + 1" was widely agreed to be a function, but "if x < 0 then x else 0" was controversial
Good answer, but not the best example. In many programming languages, the latter is easily written as an expression:
“a closed form expression or formula is one that is formed with constants, variables, and a set of functions considered as basic and connected by arithmetic operations (+, −, ×, /, and integer powers) and function composition. Commonly, the basic functions that are allowed in closed forms are nth root, exponential function, logarithm, and trigonometric functions”
and
“For example, if one adds polynomial roots to the basic functions, the functions that have a closed form are called elementary functions”
That would put the goniometric functions in the basic set allowed in elementary functions.
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.
> there is no general specification for correct translation from English to Code.
that's an interesting point. Could there be?
COBOL was originally an attempt to do this, but it ended up being more Code than English.
I think this is the area we need to get better at if we're to trust LLMs like we trust compilers.
I'm aware that there's a meme around "we have a method of completely specifying what a computer system should do, it's the code for that system". But again, there are levels of abstraction here. I don't think our current high-level languages are the highest possible level of abstraction.
No, there can’t be. Code keywords are tied to concrete mathematical concepts. Human languages are not. and even if you tried, the more languages you add to the LLM’s pool, misinterpretation chances increase exponentially. You can’t just choose English to be the programming language either, because then you would be asking every non-English speaking developer in the world to first learn the entirety of the English language which is way harder than just learning a programming language. Why are programmers so scared of code and math??
I guess you could pick a subset of a particular natural language such that it removes ambiguity. At that point, you're basically reinventing something like COBOL or Python.
Ambiguity in natural languages is a feature, not a bug. While it's better not to be an unintentional pun or joke instruction that might get interpreted as "launch the missile" by computer.
However, each project error tolerance is different. Arguably, for an average task within the umbrella of "software engineer", even current LLMs seem good enough for most purposes. It's a kind of similar transition to automatic memory managed language, trading control for "DX".
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.
The first is an attempt to provide a semantics for activity diagrams as constraints on a state machine and thereby allow folks to specify correctness properties for the state machine using a visual language. Existing work on semantics for activity diagrams already exists but doesn’t come with tooling in the way that temporal logic does (https://arxiv.org/pdf/1409.2366)
The second is an attempt to fix a long standing problem with state machine specification languages. While many support composition operators (parallel and/or nesting) none of them come with strong theorems about when temporal properties proven about constituent elements will remain valid in the composite.
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.
Yes, this article is junk. The motivating story in it is an actual REAL ID and a genuine US citizen; no evidence is presented that the REAL ID is actually unreliable for its purpose other than the claims of an agency that’s bungling its own illegal operations.
In what way do those states not match DHS requirements? I had to produce proof of legal status (citizenship doc/passport), proof of social security, and proof of residency in person in order to get my Real ID in Oregon.
My guess is that these are states where someone (a mayor, a governor) spoke out in opposition to recent escalations in immigration enforcement, or declared themselves sanctuaries, or simply voted the wrong way in recent elections.
Whatever the criteria, it's political and tribal and emotional and not real.
As an aside, any Freudians out there like me who have an urge to explore a new analysis and interpretation of America's real id?
Can you explain what you mean by “defying Federal law”? I just checked the NY DMV, and they require proof of citizenship and/or lawful status for a REAL ID. I don’t know about other states, but I would be surprised if any state were to try to issue REAL-specific IDs without complying, given that they can always issue non-REAL IDs anyways.
I wouldn't be surprised if they tried to use this as justification for a national ID, even though (to my knowledge) that would require amending the Constitution (or just ignoring it).
yes. you get it. They want a national id system that is weak enough that they can arbitrarily deny or revoke based on appearance or demeanor.
Most US citizens couldn't prove they are citizens, at least without a fingers-crossed records search IF they can remember the county they were born in. Stats say only around 10% of americans could easily put their hands on their birth certificate. Almost no one can produce one at a checkpoint if demanded, and its rare for people to even have one in their possession at home.
A passport proves citizenship, but its absence doesn't disprove it.
Voting cards and social security cards aren't identification. State issued cards like drivers licenses, state ID cards or even realID cards do not prove federal citizenship (although they do prove identity).
I think you misread your cited article. It does not say only around 10% could easily out their hands on a birth certificate. It says “9% don’t have proof of citizenship readily available” while traveling. It properly indicates nearly every US citizen has their birth certificate.
Of course you are right, basically no one carries their birth certificate around. Which is probably countered by the fact that birth certificates are pretty easily falsifiable because there is no standardization of them.
> It properly indicates nearly every US citizen has their birth certificate.
"Nearly every" is a bit of a stretch, given that black americans were still denied access to hospitals during childbirth in some states/counties as recently as the 1960s (or later). Children born via midwives often never ultimately get a birth certificate.
I think categorizing around 90% (from the cited link) as “nearly every” is accurate.
The sixties were over 50 years ago, I know as I am a child of the sixties :-)
Given how necessary driving is to living in nearly all of America, and that a with certificate is the primary point of ID to get one, there is a very strong motivation to get a birth certificate.
As the article says, the Real ID is very much a version of national ID compatible with the US’s strong tradition of federalism. Immigration authorities don’t want a reliable form of identification, they want to detain lots of people, because Stephen Miller gave them a target of 3,000 arrests a day.
Right up until it becomes clear that they will only be issued to ubermenschen, who are identified by capricious processes meant to both obscure corruption and instill fear due to their apparent randomness.
It's debatable as to whether it's technically required or not, but "the Tenth Amendment, establishes that powers not granted to the federal government nor prohibited to the states are reserved for the states or the people. This means states have the authority to create and enforce their own laws as long as they do not conflict with federal laws."
There used to be a fig leaf of truth to the idea that the supreme court would interpret things and it would generally stick. That has changed with today's court reinterpreting many settled legal ideas, one obvious one being the recent "kava augh stop" turning America into a "show your papers please" country. It didn't used to be this way.
>> US law has always relied on interpretation and precedent,
Isn't the key here that an interpretation sets the precedent, and then we don't get continual "reinterpretation"? That's what seems to be happening these days.
here's what we have: a way to identify every almost every American by their face, identify almost every American by their name and birthdate, identify every American invasively (like via a blood draw), lots of documents at the national level that we can compel people to have for various activities that are practically required for living. we don't, narrowly, have a document, that you can force everyone to have, in a very peculiar interaction, where someone can be like, "you're going to jail unless you produce this document," and you're not driving, you're not crossing a border, you're not etc. etc.
so do we need a constitutional amendment? i guess if enough people perceive that we do.
In the new world, the Supreme Court can change basically any policy or old decision and make up things not in the Constitution. One example is Trump's immunity that they created out of whole cloth and that was nowhere to be found. At the same time they invented a reason why Trump's attempted rebellion against the US did not violate the constitutional amendment that was designed to keep someone like that from running for president
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.
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.
reply