D enters Tiobe top 20

[Doc Andrew]

On Tuesday, 12 November 2019 at 11:31:43 UTC, Walter Bright wrote:
>
> True, but D doesn't have a prover anyway :-)
>

...yet :)

But in one sense, we already do. The run-time behavior of 
disabled assertions and checks basically just assumes you've 
worked through a "proof" of the program using your unit-testing.

>
> I last tried Spark many years ago, and discovered its contract 
> prover was so limited I concluded it had little practical 
> value. (If I recall, it couldn't deduce things like odd and 
> even.) I'm sure it has improved since, but how much, I have no 
> idea.

You might be asking too much from some of the solvers. It's worth 
slogging through some manual proofs with a proof assistant like 
Coq (highly-recommended resource: 
https://softwarefoundations.cis.upenn.edu/). After that, what an 
SMT solver is able to do on it's own seems very nice :)

Having said that, SPARK still requires a frustrating amount of 
hand-holding at times. You're able to do things like this now:

```
-------------------------------------------
-- double.ads (specification)
-------------------------------------------
package double
     with SPARK_Mode => On
is
     type SomeArrayType is array (Positive range <>) of Natural;

     function doubleArray(arr : in SomeArrayType) return 
SomeArrayType
         with
             Global => null,
             Depends => (doubleArray'Result => arr),
             -- set arbitrary range here in precondition to avoid 
overflow
             Pre => (for all idx in arr'Range => arr(idx) in 
0..20000),
             -- prove that everything in the return array is even
             Post => (for all idx in arr'Range =>
                      isEven(doubleArray'Result(idx)));

     function isEven(num : in Natural) return Boolean with
              Contract_Cases =>
                  (num rem 2 = 0 => isEven'Result = True,
                   num rem 2 /= 0 => isEven'Result = False);

end double;

-------------------------------------------
-- double.adb (implementation)
-------------------------------------------
package body double is

     function doubleArray(arr : in SomeArrayType) return 
SomeArrayType with
         SPARK_Mode => On
     is
         doubled : SomeArrayType(arr'Range) := (others => 0);
     begin
         for i in arr'Range loop
             doubled(i) := 2 * arr(i);

             pragma Loop_Invariant(for all j in arr'First .. i =>
                doubled(j) = 2 * arr(j));
         end loop;

         return doubled;
     end doubleArray;


     function isEven(num : in Natural) return Boolean with
         SPARK_Mode => On
     is
     begin
         if num rem 2 = 0 then
             return True;
         else
             return False;
         end if;
     end isEven;
end double;

-------------------------------------------
-- main.adb
-------------------------------------------

with Ada.Text_IO;
with double; use double;

procedure Main
     with SPARK_Mode => On
is
     arr : SomeArrayType := (3, 7, 8, 0, 1);
     result : SomeArrayType := doubleArray(arr);
begin
      for i in result'Range loop
         Ada.Text_IO.Put(Integer'Image(result(i)) & ", ");
     end loop;
end Main;
```

The lame thing is the pragma Loop_Invaraiant. In order to be able 
to
make any conclusions about the array as a whole, you've got to 
explain how
the array looks at each point in the loop. Without that, the 
prover can't
prove that your post-condition is true. My understanding is that 
SPARK needs
a lot fewer of these than it used to, but it's still annoying.

Still, I think it's kind of neat that you can prove that kind of 
behavior at compile-time, no run-time checks or unit-tests 
required!

-Doc