I see quite a bit of overlap, particularly around specification, nondeterminism, and leaving implementation choices open. MAGE advocates using as many models as are needed to make the relevant assurance case, rather than requiring a single complete specification. What remains unspecified may reflect a model that is still tacit, or a deliberate "degree of freedom" left to an agent to resolve during realization.
Is there any software that comes even close to meeting your expectations?
Given the current success of Lean 4 in the field of mathematics, do you think that Lean 4 or Roqc has a chance of achieving similar success in the realm of software verification?
What language would you use as implementation language when generating software? Roqc, Lean4, OCaml, Rust, Zig, Go, etc.?
Now, see, as a researcher who does commercial stuff only part-time, I get to answer by saying the best is yet to come, and my research group is working on it. :-D
I definitely didn't meant to point to readily available tools of today.
One of our projects is building a superior replacement for Lean and Rocq; stay tuned for more here in the coming months!
Your SQL example is very similar to how I came up with a similar language for addressing insecure cloud configuration problem. I took a different approach. I saw how pilots created a CNL. It was driven by the need to remove ambiguity in English language. The motivation was to prevent accidents due to pilots and air traffic controller communication. Controlled natural language has a subset of the language, they have constraints and meaning is pre-defined.
Prompts and ways to overcome the problem swith GenAI is addressing the symptoms of the problem which is not the right approach and will not survive in the long term.
It seems like you are assuming the spec and the code are always two separate things, so you always need a translation step. But if you pick a spec language that already runs such as SQL, CEL, Datalog, then what we write executes. No translation or regeneration required. This is how my open source tool works. The specification is just an YAML file that is capable being executed without any translation step.
One thing you are not addressing is that if you deploy the regenerated code to different environments, it is going to behave in different ways which complicates troubleshooting and fixing problems in different environments. It will be like API versioning problem but more severe.
Also the interaction of these regenerated code modules will explode in state space in different environments. The spec guarantees each component is correct. It does not guarantee correctness about the composition.
Good points, which maybe I should address in some still-further article!
Every programming/configuration language has an implementation. Such an implementation can be an interpreter or a compiler. The latter often brings a payoff in performance by paying some time cost up-front. In practice, SQL is almost always implemented with some compiler step, though it is called query planning. The target is also often (but not always) an internal virtual machine, rather than CPU machine language. In any case, I don't agree with the characterization of SQL (the central example of the post) as not canonically involving a translation step.
I tried to address the concern about environments by emphasizing that accurate formalization of external components typically remains as a major if not *the* major challenge in specifications. The fact that it's a challenge doesn't mean we can't solve it! The most satisfying way is to broaden the scope of proofs to cover more parts of a large system.
In the questions that are open, is there a way to create prototypes to answer them? This will be good for students to work on to produce some results to contribute. The problems will become concrete and it will be easy to learn and apply them.
I do think the broad formal-methods research community is working on such things, but it remains hard for most students to choose impactful projects on their own.
Adam,
If a book is afoot, I would be delighted for it to engage with my own thinking on this topic -- Model-Based Agentic Software Engineering (MAGE).
TL;DR: https://davisjam.medium.com/model-based-agentic-software-engineering-mage-856c2bf22e45
Book: https://davisjam.github.io/model-based-agentic-software-engineering/book/index.html
I see quite a bit of overlap, particularly around specification, nondeterminism, and leaving implementation choices open. MAGE advocates using as many models as are needed to make the relevant assurance case, rather than requiring a single complete specification. What remains unspecified may reflect a model that is still tacit, or a deliberate "degree of freedom" left to an agent to resolve during realization.
Cheers,
~Jamie (Drop me a line at davisjam@purdue.edu if you'd like to talk more)
Is there any software that comes even close to meeting your expectations?
Given the current success of Lean 4 in the field of mathematics, do you think that Lean 4 or Roqc has a chance of achieving similar success in the realm of software verification?
What language would you use as implementation language when generating software? Roqc, Lean4, OCaml, Rust, Zig, Go, etc.?
Now, see, as a researcher who does commercial stuff only part-time, I get to answer by saying the best is yet to come, and my research group is working on it. :-D
I definitely didn't meant to point to readily available tools of today.
One of our projects is building a superior replacement for Lean and Rocq; stay tuned for more here in the coming months!
IMO, none of the programming languages you listed are adequate, because they all expose concurrency idioms that are hard to scale. (See https://stng.substack.com/p/the-expensive-fictions-of-low-level .)
Your SQL example is very similar to how I came up with a similar language for addressing insecure cloud configuration problem. I took a different approach. I saw how pilots created a CNL. It was driven by the need to remove ambiguity in English language. The motivation was to prevent accidents due to pilots and air traffic controller communication. Controlled natural language has a subset of the language, they have constraints and meaning is pre-defined.
Prompts and ways to overcome the problem swith GenAI is addressing the symptoms of the problem which is not the right approach and will not survive in the long term.
It seems like you are assuming the spec and the code are always two separate things, so you always need a translation step. But if you pick a spec language that already runs such as SQL, CEL, Datalog, then what we write executes. No translation or regeneration required. This is how my open source tool works. The specification is just an YAML file that is capable being executed without any translation step.
One thing you are not addressing is that if you deploy the regenerated code to different environments, it is going to behave in different ways which complicates troubleshooting and fixing problems in different environments. It will be like API versioning problem but more severe.
Also the interaction of these regenerated code modules will explode in state space in different environments. The spec guarantees each component is correct. It does not guarantee correctness about the composition.
Good points, which maybe I should address in some still-further article!
Every programming/configuration language has an implementation. Such an implementation can be an interpreter or a compiler. The latter often brings a payoff in performance by paying some time cost up-front. In practice, SQL is almost always implemented with some compiler step, though it is called query planning. The target is also often (but not always) an internal virtual machine, rather than CPU machine language. In any case, I don't agree with the characterization of SQL (the central example of the post) as not canonically involving a translation step.
I tried to address the concern about environments by emphasizing that accurate formalization of external components typically remains as a major if not *the* major challenge in specifications. The fact that it's a challenge doesn't mean we can't solve it! The most satisfying way is to broaden the scope of proofs to cover more parts of a large system.
In the questions that are open, is there a way to create prototypes to answer them? This will be good for students to work on to produce some results to contribute. The problems will become concrete and it will be easy to learn and apply them.
I do think the broad formal-methods research community is working on such things, but it remains hard for most students to choose impactful projects on their own.