Le 30/09/2024 à 19:03, Kevin Chadwick via Dng a écrit :
> Robert Dewar once said that Ada has better support for pointer
> arithmetic than C.
>
> Of course it isn't needed and best avoided in Ada. There are far better
> options.
>
> Spark is a proving tool that understands the flow of an Ada program at
> compile time. It is more capable than Rust and the good thing about it
> being a separate tool is that this proving does not impact compilation
> time. The Gnat compiler still sees if you have specified that some code
> or a whole package is in spark mode and will give an error if you use a
> feature such as dynamic oop that isn't allowed in spark due to it
> breaking the ability to perform compile time flow analysis.
>
> Spark actually supports borrowing now and even prevents memory leaks
> (rust doesn't). I think it is much neater than Rusts borrowing. You can
> see that demonstrated here.
>
> https://youtu.be/97G1V2U8Drk?si=o5AL5OpoLVlMHwS1

    SPARK is much promoted by Adacore. It was already 15 years ago,
when I was programming in Ada. But the spectacular demonstration in the
video assumes familiarity with the language. One doesn't need SPARK to
learn Ada and one does not need to know all of Ada features to enjoy
writing beautifull and safe programs. The presentation reminds me of
another safety feature, beside defining the range of a variable: you
cannot create a reference to a variable unless this variable has been
declared "aliased". There is also a demonstration of packed data and bit
fields, which shows the remarkable ability of Ada to represent the hardware.

    The presentation is spectacular because the guy uses an IDE which
automatically compiles and analyses the program when a modification is
made. I never used an IDE, just Emacs and a terminal emulator to run
gcc, gnatbind, gnatlink or gnatmake. BTW Emacs has a nice Ada mode.

--     Didier