You can look at this blog post where I used a ghost global variable to hold the current state of the game (see section "Proving Functional Properties of Tetris Code"): https://blog.adacore.com/tetris-in-spark-on-arm-cortex-m4

You can similarly express ghost properties of your types, even though we don't have ghost fields in SPARK. For more on ghost code in SPARK, you can look at this presentation last year from my colleague Claire Dross: https://www.adacore.com/uploads/products/SSAS-Presentations/...

As a more extensive example of a useful library with this kind of contracts for proof, Joffrey Huguet added rich contracts of this kind to the Ada.Text_IO standard library just two weeks ago, as part of his current internship with us. This should be in the FSF trunk in the coming weeks. For example, here are some contracts he added:

   procedure Open
     (File : in out File_Type;
      Mode : File_Mode;
      Name : String;
      Form : String := "")
   with
     Pre    => not Is_Open (File),
     Post   =>
      Is_Open (File)
      and then Ada.Text_IO.Mode (File) = Mode
      and then (if Mode /= In_File
                  then (Line_Length (File) = 0
                        and then Page_Length (File) = 0)),
     Global => (In_Out => File_System);

   procedure Put (File : File_Type; Item : Character) with
     Pre    => Is_Open (File) and then Mode (File) /= In_File,
     Post   =>
       Line_Length (File)'Old = Line_Length (File)
       and Page_Length (File)'Old = Page_Length (File),
     Global => (In_Out => File_System);

   procedure Close  (File : in out File_Type) with
     Pre    => Is_Open (File),
     Post   => not Is_Open (File),
     Global => (In_Out => File_System);

Many planes, trains, rockets and medical devices run on Ada.

There is more to commercial compilers than winning the benchmarks game.

I believe the performance differences on The Computer Language Benchmarks Game is largely due to the implementations themselves. For one, pidigits have been translated from Pascal to Ada using p2ada. I do not think that this is a fair comparison at all.