[Yoric]

I will give you a few examples. My knowledge of Ada is insufficient, so I'll let you tell me whether Ada can solve that without using an external prover (note: being able to use an external prover is great and I haven't seen this done in Rust yet :) – but that's not the topic at hand).

1/ Consider a file `f` (or a socket, etc.). Using the standard library, Rust will statically ensure that, once the file is closed, you cannot attempt to, say, read from it. This is nothing special to files, just an aspect of the borrow checker.

2/ Consider a communication protocol. You need to send a message `HLO`, expect a message `ACK`, then send something else, etc. It is pretty easy to design your objects such that the operations of sending the message, receiving the message, etc. will change the type of your protocol object, ensuring statically that you never send/expect a message that you're not supposed to send in the current state.

If you're curious, I wrote a blurb last year on the topic: https://yoric.github.io/post/rust-typestate/

3/ I quickly googled "Ada spark phantom types" and didn't find anything. Does Ada support phantom types?

[pjmlp]

SPARK is a subset of Ada 2012.

Your examples are possible with contracts.

[Yoric]

I'm interested, do you have examples somewhere on how to implement that kind of properties with contracts?

[yannickmoy]

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);