[Info-vax] Rust as a HS language, was: Re: Quiet?

[Dan Cross]

In article <a3b299ca-1f94-4f3f-9e9d-21b8d7a5fd30n at googlegroups.com>,
Don Baccus  <dhogaza at gmail.com> wrote:
>On Friday, April 8, 2022 at 10:13:21 AM UTC-7, Arne Vajhøj wrote:
>> On 4/7/2022 2:46 PM, Dan Cross wrote: 
>> > In article <t2navi$sdf$2... at dont-email.me>, 
>> > Simon Clubley <clubley at remove_me.eisner.decus.org-Earth.UFP> wrote: 
>> >> BTW, I wouldn't mind seeing Ada's ranged integers showing up elsewhere, 
>> >> including being supported as an array index. That's a very nice feature 
>> >> of Ada. 
>> > 
>> > That's a feature I would very much like to have. 
>> 
>> Pascal has it. 
>> 
>> :-) 
>> 
>> $ type ar.pas 
>> program ar(input,output); 
>> 
>> type 
>> r = 1..3; 
>> a = array[r] of integer; 
>
>Yes, ADA took the idea from Pascal.
>
>The Oregon Software Pascal-2 compiler leveraged this to
>reduce checking (when checking was enabled) and that worked
>reasonably well if the programmer was careful about declaring
>ranges when it made sense to do so.

It's really refreshing the way a strong type system can be
leveraged to reduce errors by eliminating states that just
cannot be expressed.

About the best explanation I've ever seen of this is this post
from Alexis King:

https://lexi-lambda.github.io/blog/2019/11/05/parse-don-t-validate/

The gist of it is that if one can "parse" data into a form so
that the type system encapsulates the required invariants of the
data, then one needed validate it at the point of use.  The type
becomes something of a token that proves that the data was
validated, and then the type system "proves" that this invariant
holds throughout the program.

	- Dan C.


	- Dan C.