www.digitalmars.com         C & C++   DMDScript  

digitalmars.D - Some notes on Rust

reply "bearophile" <bearophileHUGS lycos.com> writes:
In the best language blog:
http://lambda-the-ultimate.org/node/5113

The discussion is long. They discuss if a good GC can be written 
in the language itself, about actual security, what a GC can and 
can't do, and more.

Bye,
bearophile
Feb 05 2015
next sibling parent reply "Ola Fosheim =?UTF-8?B?R3LDuHN0YWQi?= writes:
OT: Have you looked at Ada SPARK 2014 yet? Provides nice and 
strong system programming language semantics. With a verification 
tool... nice.

http://docs.adacore.com/spark2014-docs/html/ug/spark_2014.html
Feb 05 2015
parent reply "Vlad Levenfeld" <vlevenfeld gmail.com> writes:
On Friday, 6 February 2015 at 05:05:08 UTC, Ola Fosheim Grøstad 
wrote:

 OT: Have you looked at Ada SPARK 2014 yet? Provides nice and 
 strong system programming language semantics. With a 
 verification tool... nice.

 http://docs.adacore.com/spark2014-docs/html/ug/spark_2014.html


Even more OT: Most of this doc went over my head. Controlled 
types, access types? I only grok that its meant for 
safety-critical systems. What's this kind of programming called? 
And can you recommend any resources for learning about the 
subject from square one?
Feb 05 2015
next sibling parent "Ola Fosheim =?UTF-8?B?R3LDuHN0YWQi?= writes:
On Friday, 6 February 2015 at 05:16:56 UTC, Vlad Levenfeld wrote:

 safety-critical systems. What's this kind of programming 
 called? And can you recommend any resources for learning about 
 the subject from square one?


I haven't actually used SPARK, so my knowledge on what it can do 
is only superficial, but it is a step in the right direction to 
allow critical parts of your program to be better secured than 
the less critical parts. There is a tutorial here:

http://docs.adacore.com/spark2014-docs/html/ug/tutorial.html

The books on verification I have are from the '90s and heavy to 
read, so you probably should look elsewhere.

The terminology differs, off the top of my head:

- program verification
- verifiable programming
- partial correctness
- formal specification techniques
- formal methods
...

http://en.wikipedia.org/wiki/Formal_verification
http://en.wikipedia.org/wiki/Correctness_(computer_science)
Feb 05 2015
prev sibling parent reply "Paulo Pinto" <pjmlp progtools.org> writes:
On Friday, 6 February 2015 at 05:16:56 UTC, Vlad Levenfeld wrote:

 On Friday, 6 February 2015 at 05:05:08 UTC, Ola Fosheim Grøstad 
 wrote:

 OT: Have you looked at Ada SPARK 2014 yet? Provides nice and 
 strong system programming language semantics. With a 
 verification tool... nice.

 http://docs.adacore.com/spark2014-docs/html/ug/spark_2014.html


 Even more OT: Most of this doc went over my head. Controlled 
 types, access types? I only grok that its meant for 
 safety-critical systems. What's this kind of programming 
 called? And can you recommend any resources for learning about 
 the subject from square one?


Access types is Ada speak for pointers.

Ada is quite expressive with pointers, as what the developers are 
allowed to do with them depends on their declaration.

Outside the ML languages, Ada is probably the only language that 
allows for expressing correct programs just by taking care to 
define the right type abstractions.

For example no need to check if a variable is inside a specific 
range, if the type only allows that range.

Or no need to check for null pointers if they are declared as non 
nullable.

It is one of my favourite languages.
Feb 06 2015
parent reply Ziad Hatahet via Digitalmars-d <digitalmars-d puremagic.com> writes:
On Fri, Feb 6, 2015 at 12:08 AM, Paulo Pinto via Digitalmars-d <
digitalmars-d puremagic.com> wrote:


 For example no need to check if a variable is inside a specific range, if
 the type only allows that range.


Are you referring specifically to Ada here? Otherwise, how would ML-based
languages allow for this in a way that your traditional OO languages would
not?


--
Ziad
Feb 07 2015
parent reply "Paulo Pinto" <pjmlp progtools.org> writes:
On Saturday, 7 February 2015 at 09:13:19 UTC, Ziad Hatahet wrote:

 On Fri, Feb 6, 2015 at 12:08 AM, Paulo Pinto via Digitalmars-d <
 digitalmars-d puremagic.com> wrote:


 For example no need to check if a variable is inside a 
 specific range, if
 the type only allows that range.


 Are you referring specifically to Ada here? Otherwise, how 
 would ML-based
 languages allow for this in a way that your traditional OO 
 languages would
 not?


 --
 Ziad


Mostly Ada. An example in Ada taken from WikiBooks
(http://en.wikibooks.org/wiki/Ada_Programming/Type_System#Subtype_categories)

package Device_Driver is
     type Size_Type is range 0 .. 64;
     type Register is record
        A, B : Boolean;
        Size : Size_Type;
     end record;

     procedure Read (R : out Register);
     procedure Write (R : in Register);
end Device_Driver;

Any attempt to assign anything outside 0..64 range to Size will
trigger an error, either at compile or run-time.

As for ML languages I was thinking that similar constraints can
be expressed via dependent types, in the variants that allow
them, but never used them.

--
Paulo
Feb 07 2015
parent reply Andrei Alexandrescu <SeeWebsiteForEmail erdani.org> writes:
On 2/7/15 3:46 PM, Paulo Pinto wrote:

 Any attempt to assign anything outside 0..64 range to Size will
 trigger an error, either at compile or run-time.


What would be the similarities and differences of this built-in feature 
with traditional encapsulation using e.g. a C++ class? Thanks! -- Andrei
Feb 07 2015
parent "Paulo Pinto" <pjmlp progtools.org> writes:
On Saturday, 7 February 2015 at 23:52:04 UTC, Andrei Alexandrescu 
wrote:

 On 2/7/15 3:46 PM, Paulo Pinto wrote:

 Any attempt to assign anything outside 0..64 range to Size will
 trigger an error, either at compile or run-time.


 What would be the similarities and differences of this built-in 
 feature with traditional encapsulation using e.g. a C++ class? 
 Thanks! -- Andrei


For starters you don't need to do anything more than the type 
statement.

With C++ someone needs to write the class, overload the set of 
operators that apply to the type, including copy and move 
operations/constructors.

Compile time validation can only be done maybe with C++14 
constexpr.

Probably with clever template metaprogramming some of that code 
can be generated, but we all know how average developers like the 
error messages.

So basically the difference between declaring a class in C++, or 
doing OOP by hand in C.

Sometimes it is better to leave the hard work for the compiler.

--
Paulo
Feb 07 2015
prev sibling parent "weaselcat" <weaselcat gmail.com> writes:
On Thursday, 5 February 2015 at 14:17:16 UTC, bearophile wrote:

 In the best language blog:
 http://lambda-the-ultimate.org/node/5113

 The discussion is long. They discuss if a good GC can be 
 written in the language itself, about actual security, what a 
 GC can and can't do, and more.

 Bye,
 bearophile


although it's not a language feature, I rather like how 
'structured' their development feels, they even have a github bot 
that automatically warns if a PR contains modified unsafe code.
Feb 05 2015