I hope its going to be useful. I find myself in a particular spot, due to my stroke last year, typing is slow, so I have no choice but to use as much automation as possible. That leads to a increased velocity I couldnt have achieved even when typing with 10 fingers. Its a bit like a lame individual using an exoskeleton. Without it he is slower than an athlete. With it, faster than any athlete could ever hopy to achieve. I keep looking into ways to contribute meaningfully to the ADA ecosystem.
Thank you.
One possibility to consider is this: database-engines and SMT provers both use Unification… it is therefore possible to ‘factor’ this out and do a SPARK-proved “Verified Unification Engine” — then, using this, you could implement a prover-framework designed to be distributed (DSA), hierarchical, parameterizable (ie using the design of Generics as a template so that large portions of the module is proved, and all you have to do is check ‘detail’ “on instantiation”), and able to ‘import’/‘export’ via SMT-LIB 2… which then would allow a SPARK proved alternative implementation of SPARK along with a verified DB engine.
@OneWingedShark Thanks for the suggestion—factoring out the unification engine makes complete sense. I put together an initial implementation based on that idea here:
A quick rundown of what’s in place:
- Core Engine: First-order syntactic unification across variables, constants, and function trees, computing the MGU.
- Occurs-Check: Strict detection implemented to prevent circular bindings and infinite loops (e.g.,
X = f(X)). - Build Cleanliness: Builds with zero warnings under
-gnatwaand-gnat2022. - Testing: Standalone test suite (
make testviatests.adb) exercising term construction, chained substitutions, invariant protection, and edge cases. - License: MIT License.
Feel free to fork, adapt, or build on it however you see fit for the generic/distributed prover framework or database engine ideas.