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.
> 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)
Practically the difficulty of generating error messages is one reason why "we can't have nice things". I ran into this problem while trying to write an adventure game (like Zork) in Drools. Drools sucks in a lot of stuff from a Java compiler and mashes it into a production rules framework and the result is I was getting error messages that made no sense at all and thus gave up on the project.
One approach to compiler development is one of successive transformations and it is possible to cut compilers into very thin slices like the original FORTRAN for the IBM 1401. Similarly you can go beyond the methods taught in Graham's On Lisp to do rather complex metaprogramming in Lisp or some other language, trouble is that an error manifests at stage N+5 but the information required to explain what went wrong was elided at stage N so it is quite difficult to figure out what's going wrong.
Sure, but the goal when designing a compiler and its error messages is to prove to the user that their code in invalid. Most practical type systems are going to be either unsound or incomplete (or both), but the goal should be to make encountering those limitations rare in practice.
It seems to me that, if the limitations are encountered too often in practice, then people stop using that language to write that kind of code, because it's too frustrating to use that way.
A distinction without a difference. Perhaps "prove" is sounding too mathematical. I could rephrase it as "the goal...is to demonstrate to the user what is invalid about their code."
To prove is to demonstrate, and the way to do it is to display information about what is invalid about the code. So all these ways of phrasing it are synonymous.
The meaning of "proof" in a computer science context is much stronger than that. A proof does involve demonstration, but it's demonstration via a deductive logical argument that shows that the conclusion is logically guaranteed to follow from the premises.
Compiler error messages would be a lot more verbose if they did that rigorously.
One way of formally defining a programming languages is as the set of strings accepted as programs by the compiler, or by the formally defined algorithm that is implemented by the compiler. By such a definition, a given string is not a valid program of the respective programming language if the algorithm rejects it. And it is useful for the error message to show how the input program fails the requirements of the algorithm. The input program may be sound in type-system terms, but still not valid for the respective programming language.
A minor point. This is more akin to testing because you’re only checking your formulae against a subset of system traces.
Formal methods connotes comprehensive evidence about system behavior. In the case of TLA and similar system that’s a state machine and not the real system but the output for the state machine is a proof that your LTL/CTL/TLA properties hold for all behaviors of the system (traces or trees of traces).
Definitely, I'm playing fast and loose with "lightweight formal method here", thanks for making it clear.
I was mentioning it in the same context as e.g. the Amazon paper on lightweight formal methods [0] where they use property-based testing to test that the implementation conforms to the model specification.
In a similar spirit, linearizability checkers like Porcupine [1] are a nice mix of formalism and usability.
I really like those because they are incredibly powerful, don't require a model and verify the actual implementation - obviously as you mention they are not exhaustive.
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).
reply