I think Ada/SPARK comes pretty close in my opinion. How come it does not get as much attention as Rust when it comes to safety?
To stay on topic: https://docs.adacore.com/spark2014-docs/html/ug/en/source/co... and https://blog.adacore.com/gnat-community-2020-is-here are worth a read.
Additionally:
> The Ada concurrency model is based on the notion of task, a unit of concurrency that represents an independent thread of control. All, the tasks and the mechanisms for inter-task communication and synchronization, are introduced at language level in order to allow building safer programs. As an illustration, Ada 95 introduced protected objects to allow controlling how data is accessed, thus eliminating race conditions. Additionally, in 1997, Burns et al. introduced the Ravenscar profile, a subset of the Ada programming language that allows high integrity applications to be analyzed for their timing properties by pursuing three main goals: (1) ensuring predictable execution, (2) simplifying the runtime support, and (3) eliminating constructs with high overhead. The limitations imposed by the Ravenscar profile have an inevitable impact in the complexity of correctness analyses, e.g. tasks can only communicate through shared objects (tasks entries are not allowed, so the rendezvous mechanism cannot be used), tasks are assumed to be non-terminating, and tasks and protected objects cannot be dynamically allocated.
> Along the same lines, SPARK, a language that subsets Ada to enable the formal verification of programs, eliminates race conditions by forcing any global object referenced from a task to be marked as Part Of that task, or be a synchronized object.
I think I have a comment about Ada's concurrency where I get into it in more detail (IIRC).
> How come it does not get as much attention as Rust when it comes to safety?
Community building.
That said, Nim is very much inspired by Ada for the future safety features, in particular Z3 integration to enable Spark-like use-cases
- https://nim-lang.org/docs/drnim.html
AFAIK Ada was also inspired by Rust for memory-related safety. I find the cross-pollination between languages fascinating.
WHat's the multithreading story of Ada like? I didn't find that much code or article or papers when I was searching for multithreading runtime in other languages.
Hi,
Actually, it is the pointer support in the SPARK variant of Ada that was inspired by Rust's ownership/borrower semantic. Originally, SPARK didn't allow any pointer usage, but with the new ownership/borrower semantics, SPARK allows limited usage of Ada pointers.
As for more literature about using Ada's tasking features, I recommend the wonderful books and papers by Alan Burns and/or Andy Wellings, such as "Concurrent and Real-Time Programming In Ada (3rd Edition)." AdaCore has an old presentation on using Ravenscar with multi-core processors (https://people.cs.kuleuven.be/~dirk.craeynest/ada-belgium/ev...). There are more articles on the internet on Ada Ravenscar tasking profile and full Ada tasking.
Recently AdaCore announced they are adding support for CUDA applications in SPARK (https://developer.nvidia.com/gtc/2020/video/s21122-vid)
Ah yes, I watched that talk at FOSDEM 2019, it was very nice.
The link you provided to the SPARK user manual is a great reference. It explains how using the Ravenscar tasking profile in SPARK helps to avoid data-races and race-conditions. That, along with the ability to formally prove the absence of runtime errors and that your program satisfies various program properties and requirements are good reasons for people to seriously consider looking into using SPARK for critical parts of their software.
Because GNAT is the only free compiler out of surviving 5 or so, and even it has had some controversy in the past regarding GCC and Pro version, on a day and age, where many don't want to pay for compilers, which unfortunately are on corporate price levels in what concerns Ada offerings.
Then Pascal/Algol syntax is not cool, so you always get a bit of push back on a world that now breaths curly brackets.
However NVidia has recently chosen Ada/SPARK for their security critical firmware, so there's that.