Building trust in AI generated artifacts: GNAT Foundry - Intersection

General
,
2

There’s a couple of threads that dovetail directly into this topic:

  1. Best LLMs for ADA (SPARK) - Hobbyist
    1. Where I suggest factoring out unification (used in DB query and SMT-prover) here.
  2. [ANN]: adacovex 1.48.0: Performance improvements, more flags
    (an Ada/SPARK formal verification and compliance toolchain)
  3. Github-repo: DIANA-2022
    (the AI assisted proposed update for DIANA, @charlie5 & I did)
  4. There was a third local thread touching AI, but I can’t find it again…

But, along with some other items, we are afforded some interesting possibilities:

  • If we develop a Indefinite_Graph/Formal_Indefinite_Graph as if part of Ada.Containers;
    • Tie this with the Verified Unification Engine proposed above, and you have the core of a DB.
    • (A possible starting-point would be MNESON; directing it to update from the Charles containers to the Ada.Containers, then working from there… which may or may not be what the MNESON-2022 subdirectory is.)
  • Dogfood ourselves: Use the above VUE to implement an SMT-solver, usable in SPARK.
    Also it needs to be:
    • hierarchical, so that multiple-provers / multiple-instances can work on proofs.
    • DSA-able (distributable), so that you can have a “compute-node” able to churn through the hairy/complex stuff if needed w/o having to change the problem.
    • Parameterizable, so that you could e.g. prove the body of a generic, and like instantiation, check that the supplied parameters ‘pass’.
      (IIUC, this is actually beyond current SPARK’s capabilities; it’s been a few years, but the last time I looked into it, SPARK ran over the instances of instantiation rather than the generic proper — probably due to GNAT’s macro-expansion handling of generics.)
    • Able to use other provers.
    • Able to be used externally (e.g. by GNATProve)
  • Combining the above with an updated DIANA, we get a DB-amiable Ada-IR, running on a formally proven DB-engine…
    • Add in this 1987 paper and we get a VCS which never has the “Oh, be sure you pull last week’s version, Dave broke the build” problem and applying hooks to gate the final root-ward merge solves CI.
  • Combining the above again, say with a formally-verified bittorrent, and we have a distributed DB for distributing DIANA…
    • This means we could eg query projects on compatible licenses, or (assuming an “interface-checker”) query if updating library X impacts my client’s usage.
    • Imagine these capabilities with Alire and/or AURA (see the premise in its documentation).
    • Remember, DIANA is source-recoverable; this means that given a DIANA-reader it will be easy to spit out text-files for systems that use text-files.
  • Given DIANA’s heavy use in the above designs, it may be prudent to consider implementing IDL; though not required, it could be of some use:
    • As DIANA is an instance of IDL, we could define analogs for:
      • SQL — This would make the above VUE-using DB-engine much more familiar, as all your SQL knowledge could be ‘ported over’, the whole of the syntax, DDL, DML, etc. (The SQL spec is a lot, but I got them on sale.)
      • Queries — This would be specifically analogous/applicable to the VUE; being to the mentioned AQRL of Database Research needs an Abstract Relational Query Language what DIANA is to Ada.
      • Other languages, such as VHDL (which did have one, IVAN), or Erlang (I think it would be interesting to see how tasks could be interfaced to Erlang’s entity-model), or as database-schema updators (the input-form would be one set of structures and the output form would be another set; the IDL process would allow setting up the input/output; could possibly automatically output one of the normal-forms).
    • I have the Snodgrass book (hardcopy & PDF), the DIANA manual (hardcopy & PDF), and pdfs of the [earlier] definition and tutorial; using IDL on IDL (that is, something to IDL that is as DIANA is to Ada) and we get the nice feature of being able to compose IDL… add in something like ASIS (let’s call it ISIS, IDL Semantic Interface System), hooking into the DB we would essentially get a metalanguage for IDL and be able to manipulate instances thereof… meaning that we could implement “ASIS-2022” as calls to ISIS.
  • Apply GNOGA to all the above, and you have a distributed, DB-based, Ada IDE… sans object-code generation, which, as is tradition, is left as an exercise for the reader. :wink:

Anyway, those are my thoughts.