Name: Building High Integrity Applications with SPARK
ISBN: 9781107040731

What Hacker News says

eggyApr 2026

Some related good books I have been studying the past few years or so. The Spark book is written by people who've worked on Cube sats:

  * Logical Foundations of Cyber-Physical Systems

  * Building High Integrity Applications with SPARK 

  * Analysable Real-Time Systems: Programmed in Ada

  * Control Systems Safety Evaluation and Reliability (William M. Goble)

I am developing a high-integrity controls system for a prototype hoist to be certified for overhead hoisting with the highest safety standards and targeting aerospace, construction, entertainment, and defense.

thread

tgvMar 2026

It's ok, but not more than that. I dabbled a bit in Ada, and while that link has a lot of information, it's far from complete. Unfortunately, there isn't much more information on the internet. It can be difficult to find answers.

One thing that document doesn't mention is alire, which is a rather complete tooling. If you want to try out ada, check out https://docs.adacore.com/live/wave/alire/html/alire/index.ht...

I also learned a bit of SPARK, and there the situation is much worse. The Adacore link shows less than the bare minimum: I couldn't get my simple programs (AoC) to the "silver" level, where it passes all checks, let alone "gold", where you actually prove correctness. The rest of the internet is practically barren when you search for SPARK. I got a second-hand copy of Building High Integrity Applications with SPARK; John W. McCormick, Peter C. Chapin. It contains complete examples, and explains the concepts pretty much in depth. Unfortunately, the book is expensive, and since I was just dabbling, I got the cheapest, which was the 2015 edition, which lacks later changes.

There's an Ada forum (https://forum.ada-lang.io/), but it is not very active, and questions may not be answered.

thread

eggyJul 2025

Yes, but a qualified compiler is but one of many pieces in having an ecosystem/tooling for creating, testing, and having high-integrity applications reviewed and certified. A couple of the industries we are elbowing in on, are already familiar with the type of reports generated by the AdaCore tooling. Ada has a decades-long history in safety-critical systems (e.g., Boeing, Airbus, NASA), with proven reliability in real-time, embedded applications.

AdaCore’s GNAT Pro suite includes qualified tools (e.g., GNAT Pro, CodePeer, GNATcheck) that support traceability, code coverage, and certification evidence for standards like MISRA, DO-178C, and EN 50128. These are battle-tested in aerospace, defense, and medical applications.

Ada is defined by an ISO standard, specifically ISO/IEC 8652. The latest revision, as of 2025, is Ada 2022 (ISO/IEC 8652:2023), which includes updates to the language features. Ada is also recognized as an ANSI standard through its adoption by the American National Standards Institute, aligning with the ISO specification. The standard defines the language’s syntax, semantics, and features, ensuring consistency across implementations including compilers.

Rust’s safety guarantees prevent many runtime errors, but its approach relies more on programmer discipline vs. Ada/SPARK2014's "correct by construction" methodology. Ada is designed for real-time systems, with built-in features like tasking, protected objects, and precise control over timing (e.g., Ravenscar profile), optimized for cyber-physical systems.

Excuse my verbosity, but I pulled a few things from our tech pitch deck, and a little of the above is in our business plan as well that I copy/pasted.

Two great books if you're interested:

Analysable Real-Time Systems: Programmed in Ada (2016)

Building High Integrity Applications with SPARK (2015)

thread

nickpsecurityJul 2024

Building High Integrity Applications with SPARK

https://www.amazon.com/Building-High-Integrity-Applications-...

That will be more practical than most works on formal verification.

thread

eggyAug 2023

I always recommend this book, "Building High Integrity Applications with SPARK" as an introduction to how SPARK can be used for high-integrity, safe programs for mission-critical applications. SPARK has a legacy of large, high-integrity applications over the past two decades. This puts it ahead of Rust in real-world usage for such applications. SPARK2014 the latest, is a formally verified PL along with verification tools/ecosystem made for these type of uses.

I am trying to write show control software in SPARK2014 at the moment. Show control are critical since it is used to power lifts and stage machinery as well as performer flying systems where safety and high-integrity software is critical. I like Rust, but I feel it is not quite there yet especially in terms of the number of real-world systems in this niche. I also find SPARK2014 easier to write and read. I have been programming since 1978, and although I gravitate towards terse, functional languages like Haskell, APL/BQN/J, I experience a lot of friction whenever I dive back into Rust. SPARK2014 is very verbose and Pascal-like, but this is tedium vs. confusion or confidence in what I am writing. I know AdaCore is working with Ferrous Systems to bring Rust more up to the features of Ada/SPARK2014, but for now I needed to make a pragmatic choice based on real-world usage and ease of use and understanding.

thread

eggyJul 2023

Still waiting on Rust. I have attempted to use it beyond toy programs, and it wasn't clicking for me.

I am using SPARK2014[0], a big subset of Ada, that has a 25-year track record in high-integrity, safety-critical applications in civil and military applications in many fields. It's also very easy to pick up with integrated tooling and a package manager called Alire.

I used to despise verbose syntax, and when I first tried learning Ada over 12 years ago, I now see SPARK2014's syntax and methods as much easier and to work with especially with the surrounding and supportive ecosystem.

I worked through the book, "Building High Integrity Applications with Spark"[1] that is a very nice summary and intro to SPARK based on its use in the CubeSAT program.

Here's a cute little article on how SPARK2014 was used to replace some low-level stabilization routine in a bigger C program for a specific consumer drone:

https://blog.adacore.com/how-to-prevent-drone-crashes-using-...

[0] https://www.adacore.com/about-spark

[1] https://a.co/d/fgtRXxt

thread