We had a fun, AI-focused Ada SPARK Office Hour on Friday. I think we had about 12 people or so in the meeting, however, as I learned, a Google Meets Recording does not show who all attended, unless they spoke.
Thanks for everybody that joined and asked questions. I have a recording and am working through uploading it to YouTube, I’ll post it as a comment to this post when done.
In the meeting I walked through my personal workflow on how I have ‘conversations’ with different roles in my AI powered ‘organizaton’, all working from git worktrees. I work mainly by conversing with different AI instances that each have a different scope.
Gongalez asked a question as to how will we learn if we let the AI do everything.
Fernando walked through his experience of using more open models, which he says have improved very much. He mentions that Ada and SPARK are good languages to use with AI as they provide more trust.
The AI summary is below.
-
AI Agent Orchestration Strategy: Mark Hermeling introduced a workflow separating AI responsibilities into three distinct roles: manager, worker, and tester, each with specific configuration files to prevent the AI from straying or modifying tests inappropriately. By assigning clearly defined constraints and responsibilities, they aim to improve reliability, utilizing a custom Python orchestrator to manage Docker containers for these roles and interact with a GitLab repository.
-
Availability of Infrastructure and IDE Integration: Mark Hermeling confirmed that their infrastructure for containerized AI workflows is available, noting that projects can utilize defined development containers or default to vanilla ones. During the discussion, Mark Hermeling clarified that their current setup does not integrate directly with an Integrated Development Environment (IDE) but relies on command-line interactions and manual review of merge requests within GitLab.
-
Code Review and Approval Workflow: Olivier Henley challenged the efficiency of a non-IDE workflow, expressing concern over the overhead of reviewing code via GitLab merge requests rather than editing directly in an IDE. Mark Hermeling explained that their preference for GitLab-based reviews is a personal choice, emphasizing that the AI manager handles the bulk of the process, and they maintain control by approving or rejecting merge requests, though they acknowledged the debate regarding the necessity of IDE-based editing.
-
Hardware Bench Testing Synchronization: Mark Hermeling addressed the challenge of hardware bench testing, explaining that they use GitLab Device Cloud to manage access to hardware benches when running parallel pipelines. This system acts as a scheduler, ensuring that multiple pipelines do not conflict when accessing hardware resources, and Mark Hermeling noted the potential to integrate visual verification methods, such as camera-based monitoring, in the future.
-
Impact of AI on Skill Development: Gonçalo Caselhos raised concerns regarding the potential loss of low-level skills when relying heavily on AI for thinking and problem-solving. Mark Hermeling agreed with these concerns, noting that while they operate at a higher level of abstraction, they are worried about the impact on the next generation of engineers who may not develop foundational low-level understanding, despite being able to leverage AI to identify and address complex issues like memory allocation problems.
-
AI Control and Quality Expectations: Olivier Henley offered a perspective on controlling AI output, comparing the process to building a house where rigorous specifications are necessary to ensure the AI generates high-quality results rather than suboptimal ones. They emphasized that as users become more advanced, they demand greater control over the generated code—such as preferring specific memory handling or structural choices—and suggested that users should start by getting comfortable with available tools to find their own architectural balance.
-
Transparency in AI-Generated Reasoning: Mark Hermeling demonstrated how they utilize merge requests to review not only the code changes but also the AI’s reasoning and suggestions for verification. They noted that current frontier models have significantly improved in their ability to reason and understand complex tasks, making it easier to track the history and logic behind AI-generated modifications to files and Docker configurations.
-
Deterministic Code Generation with Ada and Spark: Fernando Oleo argued for the use of Ada and Spark to mitigate the nondeterministic and nontraceable nature of AI-generated code. They explained that because Ada is declarative and readable, it allows for better transparency, while Spark provides formal, exhaustive proofs for data dependencies and correctness, which helps build trust in the AI’s output by ensuring it does not miss edge cases or suffer from non-exhaustive error detection.
-
Building Trust via Formal Proofs: Fernando Oleo shared that their opinion on AI has shifted positively due to the ability to use Spark for generating proofs, which addresses the lack of determinism and exhaustiveness often associated with AI models. Mark Hermeling added that they use the GNAT proof tool to help the AI improve its code, suggesting that breaking down proof responsibilities into smaller, manageable tasks for individual agents significantly enhances scalability and trust in the system.
-
Spark Specification and Versioning: Fernando Oleo clarified that Spark 2014 was the final major specification, and the technology has since been incrementally improved upon rather than released as frozen versioned products. They recommended consulting the AdaCore documentation, user guides, and reference manuals to stay updated on the continuous improvements made to the Spark language and its provability capabilities.
-
Shift Toward Specification-Oriented Development: Alejandro R. Mosteo inquired about the trend of moving away from writing implementation code toward focusing on writing specifications. Mark Hermeling and others discussed how they increasingly rely on AI to generate implementation bodies from high-level requirements while retaining human oversight to review specs, acknowledging that while implementations are not always perfect, this spec-driven approach is becoming increasingly viable.
-
Integration of Model-Based Systems Engineering: Fernando Oleo contextualized their work within the broader industry movement of Model-Based Systems Engineering (MBSE), where systems are described in a central model or database of knowledge, and everything else—including code and documentation—is derived from that source of truth. They highlighted that this methodology is deterministic and mirrors practices used in other industries, such as Building Information Modeling (BIM), providing a robust foundation for AI-assisted engineering.
-
Long-Term Perspectives on AI-Assisted Programming: Mark Hermeling posited that while Spark and Ada are crucial for current trust and safety, the long-term trajectory of Large Language Models (LLMs) might eventually lead to direct generation of assembly code or other languages, though the timeline remains uncertain. They emphasized that the industry currently requires the dynamism and safety checks provided by tools like Spark to manage the inherent unreliability of AI models.
-
Demonstration of an IDE-Based AI Workflow: Olivier Henley demonstrated a primitive, IDE-centered approach to using AI, utilizing a Visual Studio Code plugin called “RU” and the Claude API to perform specific, narrowly focused tasks like porting a Microcontroller Unit (MCU) crate. They explained that this method allows them to manage costs by controlling the context window and provides direct control over the code generation process, ensuring that the AI adheres strictly to the desired technical requirements without generating unnecessary files or dependencies.
-
Evaluation of AI Models and Reasoning: Olivier Henley and Mark Hermeling discussed the multi-language capabilities of AI agents, noting that they can interact with support systems in various languages. When discussing specific models, Mark Hermeling noted they have primarily evaluated Frontier models for customer projects, while Fernando Oleo highlighted that the landscape for open models is evolving rapidly, with significant improvements in reasoning capabilities for complex specifications.
-
Generating Idiomatic Ada Code: Fernando Oleo noted that while reasoning capabilities in AI models have improved, they still struggle with generating idiomatic Ada code, often creating verbose and non-optimal structures. Mark Hermeling and Fernando Oleo concluded the discussion by acknowledging the need to create specific skills or approaches to improve how AI agents generate idiomatic code, with Mark Hermeling planning to continue the discussion in the community forum.