Best LLMs for ADA (SPARK) - Hobbyist

General
21

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.

22

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.

23

@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 -gnatwa and -gnat2022.
  • Testing: Standalone test suite (make test via tests.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.

24

Ada-Verified-Unification-Engine is Level 2 on main (d4a0c7f).

  • Prove: 176/176 (CVC5, warnings/checks as errors)
  • Tests: 26 PASS
  • Design: bump-allocated term pool (Max_Terms = 32), Term_Id indices, no access/heap; fuel-bounded occurs-check / unify / apply

Repo: GitHub - RobertBoettcherSF/Ada-Verified-Unification-Engine: verified Unification Engine in Ada · GitHub — make test / make prove

25

Hi, I heard about an AI named Workik which is good at Ada, I’ve never test it before

26

“A pitfall when using tools for automating human tasks is to end up “pleasing the tools” rather than working around the tool limitations. Both flow analysis and proof, the two technologies used in SPARK, have known limitations. Users should refrain from changing the program for the benefit of only getting fewer messages from the tools”

That is taken from the below link and surely LLMS can only please the tools and the context we give it with some probabilistic error thrown in. Whilst you can use Ada SPARK contracts to aid in LLM use I will not as although I am far from a SPARK expert I think contract use should be minimised where possible by leveraging the type system. The evidence I have seen is that LLMS produce unmaintainable code bases and technical debt is our number one enemy. I remain open minded but highly skeptical.