> SPARK itself can handle and prove some ownership properties but to the best of my knowledge isn't at the level of rust in memory safety on dynamically allocated memory.
And using https://www.adacore.com/sparkpro as a reference (ignore the 'Pro' bit as it's also available in the GPL edition) - anything certified to SPARK Silver level is far safer than any Rust code out there.
My understanding is that Rust doesn't have so much to offer Ada/SPARK. I haven't looked that hard at Rust though, so maybe I've overlooked some of it's features.
You have to jump through the same sort of hoops in Rust as you do C++ to get the sort of basic type safety found in Ada/SPARK. Rust doesn't so much have a focus on safety and correctness in general, as a focus on memory safety.
Admittedly, Ada/SPARK doesn't make the kinds of guarantees that Rust does about memory. However, accessibility checks help prevent dangling pointers and the use of memory subpools can avoid the need for explicit frees.
Additionally, Ada offers some features like the ability to return a dynamically sized array as if it were on the stack which helps reduce how often memory needs to be manually managed. I believe SPARK may not allow this sort of thing though.
I'm also not sure why you would want to abandon the actually verified properties of Ironsides for a hope those properties remained in an unverified port.
> Standard Ada supports safe use of pointers (“access types” in Ada) via strongtype checking, but safety is guaranteed only for programs where there is no explicit deallocation of pointed-to objects
This validates "With Ada you can't use dynamic memory allocation and pointers safely, unless you buy into SPARK". (GC not relevant in this context.)
> In this work, we propose a restricted form of pointers for Ada that is safe enough to be included in the SPARK subset. As our main contribution, we show how to adapt the ideas underlying the safe pointers from permission-based languages like Rust [3] or ParaSail [13]
This validates that the pointer support in SPARK "post-dates Rust".
"heavier-weight" is arguable. I'll withdraw that assertion. SPARK is definitely less expressive than Rust though; it doesn't have lifetime variables, and it doesn't allow borrows of stack values:
> The most notable one is that SPARK does not allow general access types. The reason is that we did not want to deal with accesses to variables defined on the stack and accessibility levels.
Who said anything about RAII? Having RAII doesn't make C++ memory safe. If you can take a reference or pointer to some RAII-created vector, and access it after the vector is gone… then you're not memory safe?
Yes, SPARK exists, and is very cool. I think there's work on a similar system for rust (or ferrocene, anyway, which is being co-developed by AdaCore: https://blog.adacore.com/adacore-and-ferrous-systems-joining...). It also seems that SPARK now has memory ownership and aliasing support, but only since ~2019 (https://blog.adacore.com/using-pointers-in-spark), and with clear inspiration from rust. It seems to me that this addition to SPARK was felt necessary by the AdaCore people, meaning that rust had something Ada did not support (or did not support well).
No. Ada had no safe solution to dynamic memory deallocation until SPARK started supporting it, and ergonomic support for pointers in SPARK (borrowing) postdates Rust. Arguably we still don't have proof that SPARK is ergonomic enough for widespread adoption.
(I dated Rust's breakthrough to five years ago because although Rust had the features well before then, it was only about five years ago that it became clear they were good enough for programmers to adopt at scale.)
With Ada you can't use dynamic memory allocation and pointers safely, unless you buy into SPARK, which is heavier-weight than Rust (and also post-dates Rust).
> The goal is to allow a pattern of use of pointers that avoids dangling references as well as storage leaks, by providing safe, immediate, automatic reclamation of storage rather than relying on unchecked deallocation, while also not having to fall back on the time and space vagaries of garbage collection.
with Ada.Unchecked_Deallocation;
procedure Test is
type Int_Ptr is access Integer;
procedure Free is new Ada.Unchecked_Deallocation (Object => Integer, Name => Int_Ptr);
X : Int_Ptr := new Integer'(10);
Y : Int_Ptr;
begin
Y := X;
Free (Y);
end Test;
GNATprove output:
test.adb:8:04: info: absence of memory leak at end of scope proved
test.adb:9:04: info: initialization of "Y" proved
test.adb:9:04: info: absence of memory leak at end of scope proved
test.adb:11:06: info: absence of memory leak proved
Yes, thanks. There are a lot more examples. I wish someone with deep knowledge and real experience in both Ada and Rust would write a side-by-side comparison covering all relevant aspects, including more recent developments like https://www.adacore.com/papers/safe-dynamic-memory-managemen....
no, I mean that in SPARK you are able to state that some program will not grow it's memory usage indefinitely (I believe you also have worst case time analysis).
AFAICT this requires forbidding recursion, unbounded loops and use of heap allocators or types/procedures which in turn have access to such facilities.
Or somewhat equivalently: the SPARK subset of Ada is statically verifiable by not being turing complete, so bits of the code can be verified, and elsewhere the full Ada language can be used.
I am not sure if Rust can emulate this.
(Again, I am not an Ada/SPARK developer so all of what I wrote may be wrong, do not take life decisions based on what I write)
I should also add that while you can do a lot of this subsetting, I wouldn't be surprised if some of these issues were already covered by the time the rest of Rust has been formally modelled and verified enough to be a competitor to Spark.
That is, what RustBelt analyzes right now is a language which has an analogue to Rust's borrow checker, but is much much simpler overall; and they ported Rust's implementation of several types of shared mutable or owned references over to this language to verify them.
There is a lot of Rust outside of these few caveats that hasn't been covered; these are just the things which could be in scope of the RustBelt work that haven't been covered by it.
Here are a few things that there's ongoing work on that you would want to finish before saying you were confident in a using a formally verified language:
1. The memory model. This gives a formal definition of what kinds of aliasing assumptions the compiler is able to make about raw pointers in `unsafe` code. This is being worked on here: https://github.com/nikomatsakis/rust-memory-model
2. The borrow checker. While the RustBelt work shows that a much simpler borrow checker can be sound, Rust's borrow checker has to deal with a much more complicated language, and there are few known soundness bugs in it (discussed elswhere in this thread). You'd want that to be formally modeled and verified.
3. The type system. Rust has a fairly full featured type system, so you want to ensure that's sound
4. The compiler itself. Even once you have sound code in a sound language, you need to make sure that the compiler follows the rules and compiles it correctly.
5. Any libraries or code that you are using which might be using `unsafe`. The RustBelt work so far has done so for a few core primitives, as well as a couple of third-party libraries, but of course you'd want to re-do this work against the full language (or a real-world subset, not LambdaRust that this paper used) and include any other libraries that you might need to use.
So, I'd say that there's a good chance that the RustBelt work could be extended to include one or more of these listed features before all of the rest of the above has been done. It will be a while before you could have a usable, verified subset of Rust, but once you do I think it could be a good alternative to something like SPARK, or development in C following extremely stringent rules and compiling with CompCert.
You don't need annotations to write memory safe programs in SPARK. With annotations you can verify properties of the program up to functional correctness which is not integrated in the Rust ecosystem.
Rust has an elegant concept in its ownership paradigm.
As the Rust book mentions:
Ownership is Rust’s most unique feature, and it enables Rust to make memory safety guarantees without needing a garbage collector.
In other words, you have the power/speed of a low level language without certain of the dangers, such as "double free" errors.
(That said, I'm only now proceeding through the official book. In other words, if I got this wrong, someone correct me.)
Not as much as rust, but still. I'm not sure whether it qualifies as memory safety for you but using Controlled types alleviates a large part of the problems of dynamic memory allocation. http://www.adacore.com/knowledge/technical-papers/the-gnat-i... might be of interest for the underlying implementation.
I also find that 'not null' access types, typed pointers and in general the in/out/in-out parameter passing mode help making ownership clearer... And there's also the limited types in the toolbox, to 'hide' ugly pointers/resource ids, etc.
Could we devise some simple rules and conventions inspired by Rust to have a safer resource/memory experience with C++ ?
Some pointers I gathered:
* A nice SO answer: http://stackoverflow.com/questions/30011603/how-to-enable-rust-ownership-paradigm-in-c/30062820#30062820
http://stackoverflow.com/a/30062820
* Stroustrup et al "Resource-Model" based on code static analysis: http://www.stroustrup.com/resource-model.pdf
* The idea of "Owner" hinting is nice, but requires tooling
> Rust only makes it hard to accidentally share a memory location,
Not just a memory location, any value. You can use the tools Rust gives you on any piece of state you care to manage - a database connection, a remote server, the office coffee machine - represent it as a value and Rust will let you check that it's owned where you want it to be owned, borrowed where you want it to be borrowed and so on.
> Also nothing is impossible until you prove it via formal methods (e.g. TLA+).
What's the distinction you're drawing between something like TLA+ and something like the Rust borrow checker?
> Rust guarantees memory safety with a feature called ownership. Ownership works differently from a garbage collector in other languages, because it simply consists of a set of rules that the compiler needs to check at runtime.
The rust compiler also removes bounds checks and such if it can statically prove that they won't occur. You don't have as much tooling to communicate it to the compiler as you do in SPARK just yet.
When I learned Ada (blog post somewhere in this thread) I was pretty shocked by how many more runtime checks it had than Rust does, overall. Rust usually checks things at compile time.
Yes, see, in C++, you still need to think about ownership, the compiler just can't help you out. One way of thinking about Rust is "C++, but the compiler understands ownership and memory lifetime."
It actually is: https://www.adacore.com/uploads/techPapers/Safe-Dynamic-Memo...
And using https://www.adacore.com/sparkpro as a reference (ignore the 'Pro' bit as it's also available in the GPL edition) - anything certified to SPARK Silver level is far safer than any Rust code out there.
reply