digitalmars.D - Ada conference, Ada and Spark
- bearophile (179/179) Feb 19 2014 Related to the Mars lander software thread.
- Meta (24/104) Feb 19 2014 Is it possible to implement this using the information that's
- bearophile (11/19) Feb 19 2014 Ada has an elaborate infrastructure to allow you to choose how to
- Paulo Pinto (7/13) Feb 20 2014 I have been following Ada at FOSDEM for the last years, and its
- renoX (9/13) Feb 21 2014 I don't think so: given that D is "C++ done right", it would
- Paulo Pinto (5/20) Feb 21 2014 That is easy to answer, I doubt they could with their rule of not
- Francesco Cattoglio (3/5) Feb 21 2014 Wait, what? REALLY????? What kind of rule is that.
- Paulo Pinto (5/10) Feb 21 2014 Yes really,
- Brian Rogoff (14/24) Feb 21 2014 Obviously, there is no rule in Rust that keywords have no more
- Thiez (7/17) Feb 21 2014 That is not true, Rust has several keywords that are more than 5
- Paulo Pinto (11/29) Feb 21 2014 What I was arguing in that old thread was things like pub vs public, mut...
- Francesco Cattoglio (16/20) Feb 21 2014 I knew there was no hard-coded limit, but this "try to keep
- Tobias Pankrath (6/26) Feb 21 2014 Depends on how often and where you write those keywords. mut
- Matej Nanut (8/11) Feb 21 2014 I think Rust's "pub", "priv" and "fn" are just silly. But I don't mind
- Ziad Hatahet (4/6) Feb 22 2014 Something similar had been discussed if I recall correctly, and was
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/1
/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
Feb 19 2014
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’ thenI 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.
Feb 19 2014
"bearophile" <bearophileHUGS lycos.com> 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
Feb 19 2014
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/1 /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
Feb 20 2014
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
Feb 21 2014
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]That is easy to answer, I doubt they could with their rule of not having more than 5 characters per keyword. :) -- PauloI 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
Feb 21 2014
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
Feb 21 2014
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:Yes really, http://forum.dlang.org/post/glnafbocwjodiwrqwmbv forum.dlang.org I just cannot find the Reddit thread any longer.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
Feb 21 2014
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: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. -- BrianOn Friday, 21 February 2014 at 12:56:32 UTC, Paulo Pinto wrote:Yes really, http://forum.dlang.org/post/glnafbocwjodiwrqwmbv forum.dlang.org I just cannot find the Reddit thread any longer.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
Feb 21 2014
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: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.On Friday, 21 February 2014 at 12:56:32 UTC, Paulo Pinto wrote:Yes really, http://forum.dlang.org/post/glnafbocwjodiwrqwmbv forum.dlang.org I just cannot find the Reddit thread any longer.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
Feb 21 2014
Am 21.02.2014 16:57, schrieb Thiez:On Friday, 21 February 2014 at 14:27:48 UTC, Paulo Pinto wrote:What I was arguing in that old thread was things like pub vs public, mut vs mutable and so on. I have a strong ML background as my university teachers were quite found of ML and we had a few courses using Caml Light. So I do like Rust and my issue back then was why to short those keywords and similar. Then again as I come from Pascal family of languages and always liked a bit verbosity, instead of the write only way of C. -- PauloOn Friday, 21 February 2014 at 13:08:37 UTC, Francesco Cattoglio wrote: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.On Friday, 21 February 2014 at 12:56:32 UTC, Paulo Pinto wrote:Yes really, http://forum.dlang.org/post/glnafbocwjodiwrqwmbv forum.dlang.org I just cannot find the Reddit thread any longer.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
Feb 21 2014
On Friday, 21 February 2014 at 15:57:32 UTC, Thiez wrote: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.I knew there was no hard-coded limit, but this "try to keep keywords short" sounds really stupid to me. No offence to designers, but I really don't think we should save some spar characters in 2014... I do all my coding on a remote SSH, but still I have plenty of screen space to spare ;) My first glance: "priv" instead of "private"... bleah! At least it's clear enough "mut"... what is this? "mutable", "mutex", perhaps "mute"? "impl" could be several different things, too, but I guess it's "implements" And "continue" being a different keyword some time ago. In the end they changed it. Tons of discussions and stuff; was it worth saving 3 characters, after all? I hope their standard library is at least WAY more verbose... Otherwise I pity casual Rust programmers :D
Feb 21 2014
On Friday, 21 February 2014 at 17:25:48 UTC, Francesco Cattoglio wrote:On Friday, 21 February 2014 at 15:57:32 UTC, Thiez wrote:Depends on how often and where you write those keywords. mut seems to be quite common and even in D I would not like 'reference' more than 'ref', especially since it is used in parameter lists.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.I knew there was no hard-coded limit, but this "try to keep keywords short" sounds really stupid to me. No offence to designers, but I really don't think we should save some spar characters in 2014... I do all my coding on a remote SSH, but still I have plenty of screen space to spare ;) My first glance: "priv" instead of "private"... bleah! At least it's clear enough "mut"... what is this? "mutable", "mutex", perhaps "mute"? "impl" could be several different things, too, but I guess it's "implements" And "continue" being a different keyword some time ago. In the end they changed it. Tons of discussions and stuff; was it worth saving 3 characters, after all? I hope their standard library is at least WAY more verbose... Otherwise I pity casual Rust programmers :D
Feb 21 2014
On 21 February 2014 20:00, Tobias Pankrath <tobias pankrath.net> wrote:Depends on how often and where you write those keywords. mut seems to be quite common and even in D I would not like 'reference' more than 'ref', especially since it is used in parameter lists.I think Rust's "pub", "priv" and "fn" are just silly. But I don't mind "mut". However it might've been nicer if you didn't have to write "let mut" but just "mut". What made Rust a no-go for me was when I tried to write a generic sort. I still can't figure out how to swap two elements in an array ("vector"). The implementation in their std lib for "swap" has an unsafe block... (And I don't want a GC or RC requirement for the array.)
Feb 21 2014
On Fri, Feb 21, 2014 at 12:06 PM, Matej Nanut <matejnanut gmail.com> wrote:However it might've been nicer if you didn't have to write "let mut" but just "mut".Something similar had been discussed if I recall correctly, and was rejected. Consider: `let (x, mut y) = (1, 2);` which would otherwise have not been possible.
Feb 22 2014