Formally proving programs correct is especially hard when there are pointers. This approach manages to handle them, without even requiring special programmer annotations like Rust requires.
I'm a big fan of the Why3 / ProVal / Toccata approach. Instead of building one tool to do everything, they've broken things down so they can support multiple programming languages (C / Java / Ada / Why's ML variant), multiple automated provers (e.g., Z3, alt-ergo), and multiple interactive provers (Coq, Isabelle). It seems to be a very promising approach.
To be honest, the system in this paper doesn't really match the Rust system at all. It isn't based on regions and all borrows occur upon function calls, so it's pretty similar to pre-Cyclone alias-tracking features.
For embedded Ada programs, this simpler form is probably sufficient. The main improvement you'd get from Cyclone-style nested regions is being able to type-check functions that produce outputs that are themselves borrowed pointers, either by returning them or storing them in a data structure passed as an argument. In embedded code you're much less likely to have dynamic data structures whose lifetimes are anchored to a given stack frame or control-flow region, so this isn't as useful as it is for the C++11ish coding style encouraged by Rust.
Ada and SPARK predate Rust by decades. For Rust to come on the scene and start influencing them and their well-established community is something that reflects favorably on Rust.
By contrast, when a modern language adopts something from Lisp, that doesn't really say anything new about Lisp. It's been around forever and everyone who actually bothers to learn about the history of programming languages knows Lisp has a lot to teach those who bother to learn. When a new language borrows from Lisp, that says more about the state of the new language author's education than about Lisp itself.
> Ada and SPARK predate Rust by decades. For Rust to come on the scene and start influencing them and their well-established community is something that reflects favorably on Rust.
It definitely does ! And FWIW I work at AdaCore, and even though Rust did not invent those features, I can safely say that the work we do on safe pointer is very directly inspired by Rust.
I told Yannick at AdaCore that getting parity with Rust's borrow-checker was critical given SPARK was otherwise the champ of highly-assured, system code. He said someone was working on something like that. I appreciate the tip from touisteur about this work because it's awesome!
This is also potentially a boost for my Brute-Force Assurance concept of doing versions of same code in multiple languages to leverage their verification tooling, esp automated. One obstacle was mismatch between Rust's pointers with borrow-checker and SPARK's lack of them. Bringing them closer together might let one use SPARK to model unsafe code in Rust to prove its safety. Other languages, too.
By the way, slightly off-topic but I found an interesting thread that might get you some answers about the state of the art on automatic proof of floating point operations (our last conversation on the subject) : http://lists.forge.open-do.org/pipermail/spark2014-discuss/2...
Lots of links to recent stuff, you should look it all... If you have the time :-D.
In that case, one could just go with the semantics of the SPARK-like tool with equivalent algorithm, turn that to C or assembly, and use it with Rust's FFI. That's similar to my proposal for Rust + x86 Proved or TALC. This is also an area where formal specifications can have benefit showing intent for unsafe Rust and the proven replacement.
This is a really cool paper with impressive results.
An interesting property that this paper doesn't consider (I believe the language described does not allow it though) is casting pointers/references to integers. Many languages consider this unsafe, but Rust does not. Considering casting pointers to integers unsafe prevents 'address disclosure' vulnerabilities, which is relevant in the context of any program that incorporates (potentially buggy) unsafe code (read: all of them). This can be used to defeat ASLR.
The `unsafe` keyword in Rust isn't about preventing general security vulnerabilities though, it's about denoting parts of the code where proof of memory safety has to be determined by hand.
And to display addresses (with GNAT only...) :
https://www2.adacore.com/gap-static/GNAT_Book/html/rts/s-add... . Nothing preventing you to display addresses anyway. Surely something I've reached only once or twice in 10+ years of Ada. I'm left wondering how one could debug low-level stuff without it. Sure you can use gdb, valgrind. But sometimes you can't.
I guess, because GNAT is the only free Ada compiler, all the remaining ones being commercial.
So Ada and SPARK ended up just catering to the industry that created them, high integrity systems, the kind where people die when an out-of-bounds occurs.
I've always wondered if it was in part because porting an ADA compiler ideally also involves porting some support for constructs like TASK - which ends up more like getting maintenance in place for both a language compiler as well as OS elements. In comparison porting a C compiler is mostly about the instruction set, and you can separately decide to port/support thread libs or selected RTOSes.
It's been a long time since I programmed in ADA, but the TASK support on the toolchain/system I was a long time ago sucked, and you couldn't climb into it and fix it like you might a standalone C RTOS because it was part of the tooling supplied by a vendor.
Vs with Rust, the borrow checker is fairly portable memory lifetime tracking and reasonably independent of hw architectures.
At least with GNAT, it isn't that bad - you don't have to port support for tasking when targeting an architecture or OS - e.g. there's it supports bare-metal on many ARM boards, the runtime+glue needed is not much more than for a C compiler
I don't think so, there were already other languages, like e.g. Modula-2 with similar features built-in (processes, semaphores and co-routines).
For me there were two main reasons:
1 - the cost of getting a commercial Ada compiler, much more expensive than most alternatives
2 - initially many though that Ada compilers would be extremely costly to implement. Ironically, C++ compilers are way more complex to implement than Ada ones.
As somebody who works on an Ada compiler, I'm not sure about that.
On some levels, Ada has a better design which simplifies compiler implementation.
On some others, the RM spec is extremely complicated - in my opinion because it was specified before it was implemented, and because of the need for safety - and very hard to implement.
See for example, dynamic access check, pool specific controlled types, anything related to elaboration, build in place for limited types, etc ..
Well at first almost everyone seemed to have thought it had to be complex to write an Ada compiler. It wasn't until the Robert Dewar talked (for some time) with Richard Stallman that he saw à way to drastically simplify the implementation of an Ada compiler.
No, but many millennials don't even know about Algol linage of programming languages, think C was the very first systems programming language and so Rust is more appealing to them.
Ada only caters to developers and industries that care about quality before price, and where sloppy programming and cutting corners might kill people.
Given that the computer industry still enjoys EULAs with disclaimers, product refunds and lawsuits due to sloppy programming or CVE exploits are still pretty rare, it is almost impossible to convince people otherwise.
One of the great outcomes of the increase in malware attacks is finally getting more buy-in for safer native languages.
Formally proving programs correct is especially hard when there are pointers. This approach manages to handle them, without even requiring special programmer annotations like Rust requires.
I'm a big fan of the Why3 / ProVal / Toccata approach. Instead of building one tool to do everything, they've broken things down so they can support multiple programming languages (C / Java / Ada / Why's ML variant), multiple automated provers (e.g., Z3, alt-ergo), and multiple interactive provers (Coq, Isabelle). It seems to be a very promising approach.
Cool! Thanks for sharing!