Missed this office hour as I was away for a bit. Looking forward to the next one, I have some stuff I which believe could be discussed though I would have to take some time to collate my thoughts.
Summary:
Flare language extensions and AI integration discussion with asynchronous runtime presentation.
Introductions
Participant 5 introduced their history with Rust and current work developing a formally proven Spark async runtime.
Participant 6 identified as an Ada Core customer with 30-plus years of experience.
Flare Extension Framework
Participant 2 and Participant 1 defined “Flare” as an RFC-driven project for post-2022 Ada and Spark extensions to improve safety and ease of use.
Flare extensions will be open-source, backwards compatible, and configurable via compiler flags.
The team clarified that while Flare covers both Ada and Spark, some new features may not translate to the restrictive Spark subset.
Proposed syntax changes include “finally” blocks, record aggregates, and improved loop control flow.
GNAT Foundry Intersection AI Demo
Participant 2 introduced an upcoming open-source demonstrator showcasing AI-driven development with deterministic verification boundaries.
The demo features full traceability from Concept of Operations to high-level requirements, code, and tests.
The framework incorporates non-AI deterministic tools to verify that AI-generated artifacts meet safety requirements.
The system requires an LLM to execute modifications and generates formal verification reports.
Async Runtime Development
Participant 5 demonstrated a Spark-proven async runtime inspired by Tokio, utilizing IOuring for Linux-based async syscalls.
The architecture uses fixed thread shards to maintain compatibility with Spark constraints, avoiding dynamic task spawning.
Participant 5 noted the challenge of maintaining formal proofs when interfacing with assembly and C-level code.
Participant 1 recommended reviewing Participant 7’s work-stealing implementation and Participant 8’s “Concurrent and Realtime Programming in Ada” for architectural best practices.
Implementation of stackful coroutines in Spark
Participant 5 implemented stackful coroutines in Spark using assembly.
Discussion highlighted fundamental architecture differences between Rust’s state machine-based await execution and Ada’s tasking models.
The current codebase supports Windows systems utilizing IOCP.
Project licensing and access
The codebase remains private due to significant AI-generated content.
Participant 5 offered access to the repository for interested developers via the community forum.
Language evolution and tasking support
Limitations in Spark tasking stem from proof technology and engineering capacity constraints.
Participant 3 recommended directing coroutine or await keyword proposals to the Ada Rapporteur Group.
