Hi, the SPARK is an industrial-grade toolsuite around an actual specified language, used in actual real-world applications. Since it's a subset of Ada, it's com

Hi, the SPARK is an industrial-grade toolsuite around an actual specified language, used in actual real-world applications. Since it's a subset of Ada, it's completely integrable in an Ada project. The idea is that you'd have parts of your project in Ada (with all its static and runtime guarantees) and parts in SPARK (and here you also have latitude in which level of proof you want in which part of your code: absence of runtime errors, functional properties, full spec proof...). The SPARK people really thought about the adoption path from Ada (even C) to SPARK. And they are purely pragmatic: the subset of Ada that constitutes SPARK is the actual subset that is actually tractable to proof. So they're adding pointers and proofs with pointers using a rust-like ownership model, the SPARK subset will be updated to pointers (yay that was missing). This is actually an incredible achievement. I also think all these 'ownership' checks might trickle into Ada later on, and improve static checks without going to proof. Exciting time to be working with Ada!