Related to the Mars lander software thread.

They have released the slides for the FOSDEM 2014 (1 February 2014) conference about Ada and related things (http://people.cs.kuleuven.be/~dirk.craeynest/ada-belgium/events/14/140201-fosdem.html ).

Two interesting slide packs, one introduction about modern Ada 2012, and the other about SPARK 2014, the latest version of a more formal language based on Ada:

http://people.cs.kuleuven.be/~dirk.craeynest/ada-belgium/events/14/140201-fosdem/01-ada-introduction.pdf

http://people.cs.kuleuven.be/~dirk.craeynest/ada-belgium/events/14/140201-fosdem/03-ada-spark.pdf


The slides contain many interesting examples, the first ones are Ada, the last two about Spark.

The "safety and correctness" given by Ada/Spark type systems, semantics and syntax are quite different from the "safety" given by Haskell. They share some qualities, but they are also based on quite different principles, and they have quite different purposes. I have seen lot of people write about the correctness and safety of Haskell programs, but they usually don't even keep in mind the existence of Ada/Spark. I don't fully understand this situation.

I think regarding "safety and correctness" D is midway between C++ and Ada.

One important thing that should be kept in mind when you think about the "success" of D contract programming (beside the current lack of old/pre-state in D) is that there are many kinds of D code: small script-like programs, GUIs, video games, heavy numeric software, large applications, and so on. Some of those kinds of code don't need much contracts. But in larger programs or in programs where you need a partial integrity (where you can also use Ada), it's useful.

--------------------------------------------

Integral ranges and strong types:


type Age   is range 0..125;
type Floor is range -5 .. 15;
My_Age  : Age;
My_Floor : Floor;
...
My_Age   := 10;       -- OK
My_Floor := 10;       -- OK
My_Age   := My_Floor; -- FORBIDDEN !

--------------------------------------------

Ranged not-integral value with optional delta:


type Density is delta 1.0/256.0 range 0.0 .. 1.0;

(So Density is represented with a single byte, despite it looks like a not integer number.)

--------------------------------------------

Discriminated types:


ype Major  is (Letters, Sciences, Technology);
type Grade is delta 0.1 range 0.0 .. 20.0;
type Student_Record (Name_Length : Positive;
                     With_Major  : Major)
is record
   Name    : String(1 .. Name_Length); --Size depends on discriminant
   English : Grade;
   Maths   : Grade;
   case With_Major is     -- Variant part, according to discriminant
      when Letters =>
         Latin : Grade;
      when Sciences =>
         Physics   : Grade;
         Chemistry : Grade;
      when Technology =>
         Drawing : Grade;
   end case;
end record;

--------------------------------------------

Low level description of a record:


type BitArray is array (Natural range <>) of Boolean;
type Monitor_Info is
    record
        On     : Boolean;
        Count  : Natural range 0..127;
        Status : BitArray (0..7);
    end record;
for Monitor_Info use
    record
        On     at 0 range 0 .. 0;
        Count  at 0 range 1 .. 7;
        Status at 0 range 8 .. 15;
    end record;

--------------------------------------------

Example usage of both floating point ranges and invariants:


package Places is
    type Disc_Point is private;
    -- various operations on disc points
private
    type Disc_Point is
        record
            X, Y : Float range -1.0 .. +1.0;
        end record
        with Invariant => Disc_Point.X ** 2 +
                          Disc_Point.Y ** 2 <= 1.0;
end Places;

--------------------------------------------

Static predicates (related to the "enum preconditions" I suggested for D):


procedure Seasons is
    type Months is (Jan, Feb, Mar, Apr, May, Jun,
                    Jul, Aug, Sep, Oct, Nov, Dec);
    subtype Summer is Months
        with Static_Predicate => Summer in Nov .. Dec |
                                           Jan .. Apr;
    A_Summer_Month : Summer;
begin
    A_Summer_Month := Jul;
end Seasons;


The code gives:

warning: static expression fails static predicate check on "Summer"

--------------------------------------------

A kind of set syntax:


elsif First and then C in '+' | '0' .. ’9’ then

--------------------------------------------

Loop variants and invariants:


procedure Loop_Var_Loop_Invar is
   type Total is range 1 .. 100;
   subtype T is Total range 1 .. 10;
   I : T := 1;
   R : Total := 100;
begin
   while I < 10 loop
      pragma Loop_Invariant (R >= 100 - 10 * I);
      pragma Loop_Variant (Increases => I,
                           Decreases => R);
      R := R - I;
      I := I + 1;
   end loop;
end Loop_Var_Loop_Invar;

--------------------------------------------

An example in Spark, to clarify access to global variables (for D I suggested a simpler optional @outer() attribute: https://d.puremagic.com/issues/show_bug.cgi?id=5007 ):


with Global => null;       -- Not reference to global items
with Global => V;          -- V is an input of the subprogram
with Global => (X, Y, Z);  -- X, Y and Z are inputs of the subprogram

with Global => (Input  => V); -- V is an input of the subprogram.
with Global => (Input  => (X, Y, Z)); -- X, Y and Z are inputs of the
                                      -- subprogram
with Global => (Output => (A, B, C)); -- A, B and C are outputs of the
                                      -- subprogram
with Global => (In_Out => (D, E, F)); -- D, E and F are both inputs and
                                      -- outputs of the subprogram

with Global => (Proof_In => (G, H)); -- G and H are only used in assertion
                                     -- expressions within the subprogram

with Global => (Input    => (X, Y, Z),
                Output   => (A, B, C),
                In_Out   => (P, Q, R),
                Proof_In => (T, U));
                -- A global aspect with all types of global
                -- specification

--------------------------------------------

To clarify information flow:


procedure P (X, Y, Z : in Integer; A, B, C : in out Integer; D, E out Integer)
  with Depends => ((A, B) =>+ (A, X, Y),
                   C      =>+ null,
                   D      =>  Z,
                   E      =>  null);
-- The "+" sign attached to the arrow indicates self-dependency
-- The exit value of A depends on the entry value of A as well as the entry
-- values of X and Y.
-- Similarly, the exit value of B depends on the entry value of B as well as
--  the entry values of A, X and Y.
-- The exit value of C depends only on the entry value of C.
-- The exit value of D depends on the entry value of Z.
-- The exit value of E does not depend on any input value.

--------------------------------------------

Bye,
bearophile

On Wednesday, 19 February 2014 at 23:55:16 UTC, bearophile wrote:
> Integral ranges and strong types:
>
>
> type Age   is range 0..125;
> type Floor is range -5 .. 15;

Is it possible to implement this using the information that's already available through Value Range Propagation? I think I remember Andrei describing it in TDPL as numeric values carrying around their ranges at compile time, but I don't remember exactly.

> My_Age  : Age;
> My_Floor : Floor;
> ...
> My_Age   := 10;       -- OK
> My_Floor := 10;       -- OK
> My_Age   := My_Floor; -- FORBIDDEN !

How close do you think std.typecons.Typedef is to supporting this functionality? Is it a sufficient replacement?

> Discriminated types:
>
>
> ype Major  is (Letters, Sciences, Technology);
> type Grade is delta 0.1 range 0.0 .. 20.0;
> type Student_Record (Name_Length : Positive;
>                      With_Major  : Major)
> is record
>    Name    : String(1 .. Name_Length); --Size depends on discriminant
>    English : Grade;
>    Maths   : Grade;
>    case With_Major is     -- Variant part, according to discriminant
>       when Letters =>
>          Latin : Grade;
>       when Sciences =>
>          Physics   : Grade;
>          Chemistry : Grade;
>       when Technology =>
>          Drawing : Grade;
>    end case;
> end record;

Ditto, except for with std.variant.Algebraic. It does need some work, but I think the important part is whether it's implementable in the library with a nice syntax. Then it only requires somebody to do the necessary work.

> Low level description of a record:
>
>
> type BitArray is array (Natural range <>) of Boolean;
> type Monitor_Info is
>     record
>         On     : Boolean;
>         Count  : Natural range 0..127;
>         Status : BitArray (0..7);
>     end record;
> for Monitor_Info use
>     record
>         On     at 0 range 0 .. 0;
>         Count  at 0 range 1 .. 7;
>         Status at 0 range 8 .. 15;
>     end record;

Isn't this the same as a struct?

> Static predicates (related to the "enum preconditions" I suggested for D):
>
>
> procedure Seasons is
>     type Months is (Jan, Feb, Mar, Apr, May, Jun,
>                     Jul, Aug, Sep, Oct, Nov, Dec);
>     subtype Summer is Months
>         with Static_Predicate => Summer in Nov .. Dec |
>                                            Jan .. Apr;
>     A_Summer_Month : Summer;
> begin
>     A_Summer_Month := Jul;
> end Seasons;
>
>
> The code gives:
>
> warning: static expression fails static predicate check on "Summer"

What are the limitations on what Static_Predicate can verify? It seems like this could be quite powerful, but not as powerful as runtime checks, since not everything can be checked at compile time.

> A kind of set syntax:
>
>
> elsif First and then C in '+' | '0' .. ’9’ then

I think this would be quite easy to do using mixins. I've also been thinking about list comprehensions a la Python, done with mixins.

> Loop variants and invariants:
>
>
> procedure Loop_Var_Loop_Invar is
>    type Total is range 1 .. 100;
>    subtype T is Total range 1 .. 10;
>    I : T := 1;
>    R : Total := 100;
> begin
>    while I < 10 loop
>       pragma Loop_Invariant (R >= 100 - 10 * I);
>       pragma Loop_Variant (Increases => I,
>                            Decreases => R);
>       R := R - I;
>       I := I + 1;
>    end loop;
> end Loop_Var_Loop_Invar;

This is a neat feature. I thought it was unique to Wiley, but I guess the creator of Wiley must've got it from Ada. Does the loop break if the invariant fails, or does it stop the program?

> An example in Spark, to clarify access to global variables (for D I suggested a simpler optional @outer() attribute: https://d.puremagic.com/issues/show_bug.cgi?id=5007 ):
> ...

I don't think this is quite as important, seeing as D has the pure keyword.

Meta:

> What are the limitations on what Static_Predicate can verify? It seems like this could be quite powerful, but not as powerful as runtime checks, since not everything can be checked at compile time.

In Ada there is Dynamic_Predicate for the other cases :-)


> Does the loop break if the invariant fails, or does it stop the program?

Ada has an elaborate infrastructure to allow you to choose how to react to failures, how to handle them, what failures to ignore, etc. At least, it stops the program.


> I don't think this is quite as important, seeing as D has the pure keyword.

Purity means you can't use mutable values from outer scopes. The point of those Spark annotations (and @outer()) is to do the opposite: to specify the flow of information in system programming when you are not using purity.

Bye,
bearophile

On Wednesday, 19 February 2014 at 23:55:16 UTC, bearophile wrote:
> Related to the Mars lander software thread.
>
> They have released the slides for the FOSDEM 2014 (1 February 2014) conference about Ada and related things (http://people.cs.kuleuven.be/~dirk.craeynest/ada-belgium/events/14/140201-fosdem.html ).
>
> ...

I have been following Ada at FOSDEM for the last years, and its use seems to be increasing in Europe for safety critical systems, mainly thanks to C and C++ issues.

Maybe this is an area where D could be pushed as well.

--
Paulo

On Thursday, 20 February 2014 at 08:03:47 UTC, Paulo Pinto wrote:
[cut]
> I have been following Ada at FOSDEM for the last years, and its use seems to be increasing in Europe for safety critical systems, mainly thanks to C and C++ issues.
>
> Maybe this is an area where D could be pushed as well.

I don't think so: given that D is "C++ done right", it would require many (unlikely to happen) changes to become an interesting alternative for Ada: for example changing the semantic of integers!

That said, one question I should ask to Rust devs is why they didn't base Rust on Ada given their goals..

renoX

On Friday, 21 February 2014 at 10:01:41 UTC, renoX wrote:
> On Thursday, 20 February 2014 at 08:03:47 UTC, Paulo Pinto wrote:
> [cut]
>> I have been following Ada at FOSDEM for the last years, and its use seems to be increasing in Europe for safety critical systems, mainly thanks to C and C++ issues.
>>
>> Maybe this is an area where D could be pushed as well.
>
> I don't think so: given that D is "C++ done right", it would require many (unlikely to happen) changes to become an interesting alternative for Ada: for example changing the semantic of integers!
>
> That said, one question I should ask to Rust devs is why they didn't base Rust on Ada given their goals..
>
> renoX

That is easy to answer, I doubt they could with their rule of not having more than 5 characters per keyword. :)

--
Paulo

On Friday, 21 February 2014 at 12:56:32 UTC, Paulo Pinto wrote:
> That is easy to answer, I doubt they could with their rule of not having more than 5 characters per keyword. :)
Wait, what? REALLY????? What kind of rule is that.
ahahahha... are they stuck to the 70's? :D

On Friday, 21 February 2014 at 13:08:37 UTC, Francesco Cattoglio wrote:
> On Friday, 21 February 2014 at 12:56:32 UTC, Paulo Pinto wrote:
>> That is easy to answer, I doubt they could with their rule of not having more than 5 characters per keyword. :)
> Wait, what? REALLY????? What kind of rule is that.
> ahahahha... are they stuck to the 70's? :D

Yes really, http://forum.dlang.org/post/glnafbocwjodiwrqwmbv@forum.dlang.org

I just cannot find the Reddit thread any longer.

On Friday, 21 February 2014 at 14:27:48 UTC, Paulo Pinto wrote:
> On Friday, 21 February 2014 at 13:08:37 UTC, Francesco Cattoglio wrote:
>> On Friday, 21 February 2014 at 12:56:32 UTC, Paulo Pinto wrote:
>>> That is easy to answer, I doubt they could with their rule of not having more than 5 characters per keyword. :)
>> Wait, what? REALLY????? What kind of rule is that.
>> ahahahha... are they stuck to the 70's? :D
>
> Yes really, http://forum.dlang.org/post/glnafbocwjodiwrqwmbv@forum.dlang.org
>
> I just cannot find the Reddit thread any longer.

Obviously, there is no rule in Rust that keywords have no more than 5 letters (return, extern, ...) but the designers favor short keywords, maybe a bit much for my taste. OTOH, I prefer their preference for favoring immutability and expression oriented style to D's statement oriented preference. The latest version of Ada tries to fix Ada a bit in this regard

http://www.ada-auth.org/standards/12rat/html/Rat12-1-3-2.html

but it's a bit late. I'm glad to hear that Ada use is increasing somewhere, but I don't see it in any market I look at.

The Rust designers are targetting C and C++ users, with a different vision than Walter and Andrei's as to what constitutes "C++ done right", and some specific applications, like Servo.

-- Brian

On Friday, 21 February 2014 at 14:27:48 UTC, Paulo Pinto wrote:
> On Friday, 21 February 2014 at 13:08:37 UTC, Francesco Cattoglio wrote:
>> On Friday, 21 February 2014 at 12:56:32 UTC, Paulo Pinto wrote:
>>> That is easy to answer, I doubt they could with their rule of not having more than 5 characters per keyword. :)
>> Wait, what? REALLY????? What kind of rule is that.
>> ahahahha... are they stuck to the 70's? :D
>
> Yes really, http://forum.dlang.org/post/glnafbocwjodiwrqwmbv@forum.dlang.org
>
> I just cannot find the Reddit thread any longer.

That is not true, Rust has several keywords that are more than 5 characters, such as 'continue'. The full list is here: http://static.rust-lang.org/doc/master/rust.html#keywords . It is true that they prefer short keywords over long ones. It used to be the case that 'loop' could mean 'continue' but people found it confusing so it was fixed.