HN user
github: https://github.com/johnbender
twitter: https://twitter.com/johnbender
writing: http://johnbender.us
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.
Sure!
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.
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.
https://ghc.gitlab.haskell.org/ghc/doc/users_guide/exts/line...
Experimental and of course one can debate whether Haskell is mainstream but I figured it merits a mention.
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
There’s decades of research in this vein fwiw, usually referred to as symbolic execution and it’s descendants like concolic execution.
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).
If you view a file system as running concurrently with another instance of itself where it could be preempted at any time indefinitely and where your algorithm for ensuring your crash protocol invariant must be lock free (two threads helps here) then you get a good sense for the complexity of the problem.
Fwiw we have at least some reason to hope in this general context that between clever systems work and tightening theoretical bounds via additional assumptions and clever reasoning we might get to practical implementations for some applications.
As (maybe weak) evidence the progress on practical implementations of PCPs/SNARGs
Learning whether the button should change colors is different from actually changing the colors.
I agree that the learning part is interesting but at google I suspect those are two different jobs.
As an aside Madoff Industries did employ people who earnestly worked outside the Ponzi scheme. I know because I met a few of them when I worked on a database architecture audit for them around 2008.
To follow on this sentiment at a slight tangent, I am happy for the enthusiastic attempts from all quarters but folks seem to misunderstand that incremental progress in academia is often due to the problems being very hard. Formal verification in the presence of weak memory models is an ongoing problem that only recently has seemed tractable thanks to the hard work of the folks at MPI etc over more than a decade of publications and iterating on logics like Iris
I think this depends on the spec language and the target system. I’ve never encountered a spec more complicated than the program as the goal is always abstraction but I don’t mean to discount your experiences and complexity is affected by tooling familiarity and quality.
Separately the spec can often have its own properties which can be verified as a means to interrogate its correctness. For example state machines as spec, temporal logic properties and model checking where the state machine is the abstraction for a concrete system. Worth noting that proving state machines are an abstraction of a concrete system is a going research concern though.
I think this sharply discounts the value of the step before the proof which is writing the specification in a formal language/logic. This often surfaces these misunderstandings before a proof is even necessary.
That doesn’t guarantee that the spec will be the right one (as you say) but it’s astounding how often just writing it down formally improves the implementation through rigorous thought.
In general you can't prove a program will or won't terminate.
As a point of clarity for folks who come to this (the commenter clearly knows this) one can’t _automatically_ prove for an arbitrary program whether or not it terminates. It’s definitely possible to prove this manually per program and most dependently typed languages will do the work for you as a matter of sound over approximation as long as one of the arguments is shrinking in an obvious way.
Raft has been manually verified which was the hurdle here that makes the result interesting:
More likely we’re looking at codesign/correct-by-construction for fully general purpose verification.
In many cases it’s possibly to refine a state machine based specification to an imperative implementation (and thereby carry safety properties down to the implementation) but at present the implementation usually looks like the state machine (thus codesign)
In Coq the user generally writes meta programs to generate proofs as programs at varying levels of automation (Ltac scripts). Here they used IC3 to automatically produce proof that their state based model of paxos satisfies the invariant.
In principle one could build an automated proof system for a state machine-esque formalism written in Coq using Ltac but that would be a nightmare in practice.
This is an important observation!
If the properties of concern for your thread or program are only safety properties (“never does a bad thing”) then the fact that the program may never do anything at all is just fine!
Then, if you want some liveness properties (“eventually does something good”) you’ll need to embed some assumption about fairness/scheduling/progress just as you’ve said!
This appears in early concurrency literature (TLA etc which I can’t be bothered to look for)
Worth noting that the ISA is more than a set of instructions it’s also a semantics for those instructions. For example the concurrent semantics of ARM processors permits a much larger array of optimizations on the per thread level which is good for performance.
The thing I love most about mechanized proofs is that my questions about the reasoning always have tangible answers, even if the answer is “we axiomatized this thing”.
The availability of the intermediate proof state as a part of the published object makes those answers that much easier to find. This is a really great project!
Formal specifications aren't only useful for proving properties of programs. They can also be useful for providing definitive answers to questions about example program behavior which is useful for regular programmers.
For example the Herd tool kit can take small concurrent programs with some constraints and a memory model and then answer whether any executions are possible.
http://diy.inria.fr/doc/herd.html
Alternately there is the online tool for the same purpose for ARMv8:
For the memory model you can take a look at some of the best research in the subfield: