If I can’t, I really would like to ask people who work at AdaCore or have used both Ada and Rust about how they compare and contrast when it comes to memory safety.
I’ve been playing around with Ada SPARK a lot more recently since I feel like conceptually SPARK is like Rust’s borrow checker but on steroids. But, as I’ve looked more into it, it seems like SPARK is weaker in some other areas (since SPARK can only be used on certain files in your Ada project, and SPARK assumes things about the external environment that might not necessarily hold true).
I would be interested if anyone has used SPARK to create something that is wholly memory safe and proven to be memory safe from top to bottom (including Ada’s standard library).
Rust can almost do that with its borrow checker, but low level standard library primitives are made using unsafe Rust, and can, in rare cases, lead to memory vulnerabilities if that part of the standard library hasn’t been audited yet.
An interesting overview article by Roderick Chapman and Florian Schanda is:
“Are We There Yet? 20 Years of Industrial Theorem Proving with SPARK”
As well as another paper, from Communications of the ACM, by Roderick Chapman, Claire Dross, Stuart Matthews, and Yannick Moy:
“The SPARK programming language and analyzer. Co-Developing Programs and Their Proof of Correctness”
Could you post the link here to join the online meeting?
When I click the Join button on the above page, all that happens is a .ics file is downloaded but the event is not added to my calendar. Probably a wrong setup somewhere on my side…
Discussions regarding language memory safety and formal verification methods integrated with artificial intelligence for code optimization.
Language Safety and Standards
Memory safety differences between languages were contrasted, highlighting how formal proof reduces testing needs. Standards still mandate comprehensive coverage despite high trust in formal methods.
AI for Code Development
Frontier artificial intelligence models effectively generate contracts and support lifting codebases to Spark Silver levels. Utilizing paid model tiers is required to ensure accurate hardware code translation.
Expanding Academic Formal Verification
Efforts to broaden adoption in universities emphasize industrial applications of formal verification. Dedicated learning resources now pair course material with interactive model assistance.
Anonymized Notes
Comparison of Ada and Spark to Rust for Memory Safety: A participant introduced a discussion comparing memory safety across Ada, Spark, and Rust by referencing a blog post utilizing the Common Weakness Enumeration list published by the Software Engineering Institute. Another participant argued that Spark focuses on formal proof, whereas Rust and Ada feature unsafe elements, though Ada allows developers to isolate unsafe code into a very small, distinct portion of a program, thereby lowering overall anxiety compared to C and C++.
AI-Generated Code, Benchmarks, and Formal Verification for Spark: A participant raised challenges regarding benchmarking and data sets for fine-tuning AI models to generate correct Spark code while managing context and looping variants. A participant shared an evaluation data set link and noted that commercial models excel at generating Spark contracts, whereas models like DeepSeek achieve about 75% accuracy and Qwen struggles with Ada. Another participant suggested leveraging advanced frontier models to frame specifications and development paths.
Memory Safety in Ada, Rust, and C++: A participant resumed the discussion on memory safety, noting that while newer C++ versions offer benefits, backwards compatibility allows unsafe pointer references. A participant summarized that Rust handles memory safety better via static checks, Ada offers superior general program correctness through type expressiveness, and Spark combines memory safety with static proof of runtime checks. A participant outlined Ada 22 efforts to minimize unchecked deallocation and reduce reliance on access types to eliminate major memory safety vulnerabilities.
Formal Proof Versus Testing and AI Codebase Lifting: Participants highlighted that Spark formal proof verifies all execution paths and reduces the need for extensive unit testing, catching problems earlier. A participant offered to run public GitHub or GitLab repositories through AI tools to lift existing Ada codebases to Spark Silver using spare AI tokens. A participant noted that Spark Silver provides an optimal balance of effort and benefit, whereas Spark Gold functional correctness is more challenging for cryptography like SHA-3 implementations, which often rely on traditional test vectors.
Runtime Checks and Functional Safety Standards: A participant used a skiing analogy to describe Ada runtime checks as a gauntlet of hoops that helps validate program behavior when combined with minimal testing. Participants discussed functional safety standards like ISO 26262, noting that while formal methods provide high trust and can sometimes reduce code coverage requirements such as full MCDC to statement coverage, standards still mandate high coverage to verify that all code serves a required purpose.
Expanding Ada and Spark in Universities: Participants discussed initiatives to broaden Ada and Spark adoption in universities through collateral, guest lectures, and capstone projects. A participant suggested that pitching the industrial application of formal verification engages academics more effectively than focusing strictly on specific language names. A participant inquired about overlaying Spark on existing codebases, and a participant reiterated the offer to lift codebases using AI tokens. A participant reported submitting five capstone projects to Penn State Great Valley and offered to present them.
Embedded Development, Hardware Integration, and AI Model Tiers: A participant shared an embedded project experience involving ST Micro, I2C interfaces, and display hardware troubleshooting, noting that AI tools struggled with hardware-specific code translation and required manual translation and reference to working Arduino libraries. Participants emphasized that utilizing paid frontier AI models rather than free or cheap tiers is critical to avoid poor code generation and wasted time. A participant compared software engineering management to overseeing a team of AI agents.
Beginner Resources for Learning Ada and Spark: A participant asked about beginner resources for undergraduates outside of aerospace or nuclear engineering fields. A participant directed them to learn.adacore.com for Spark courses and recommended pairing the material with a capable AI model acting as an interactive learning assistant.
