Re: Rust's temporal safety for Ada/SPARK

[digitalkevlar@gmail.com]

@ Robert Eachus

"There are some cases that require run-time checking, and most programmers consider code that needs run-time checking as a bug"

I can see why they'd avoid such constructions if their tooling couldn't prove them safe. If another tool can, though, then I'm thinking it's a bug in Ada in that Ada's model or tools can't handle that analysis at compile-time. Something worth fixing with R&D. That's why I'm trying to assess what Ada can do currently in this area. Several other languages knock this problem out at compile time. They're functional, logical, and imperative. So, I know it is feasible in general case.

@ All

Niklas Holsti's post shows he understands what capability I'm describing. Rust code can be shown free of double-free's and dangling-pointers at *compile-time* with *no runtime checks or GC*. It does it with just a few simple rules. Here's the simplest, shortest description I could find to save you all time:

https://stackoverflow.com/questions/36136201/how-does-rust-guarantee-memory-safety-and-prevent-segfaults

Those are combined with "traits"... or something else in language... to allow race-free concurrency. Instead of mandating one model for language, various models of concurrency are defined in libraries to let you use model easiest for your problem. Language's ownership model & borrow-checker ensures they're all memory-safe and race-free along with any code using them. So, you get these guarantees even in multi-threaded code doing many allocations and de-allocations of memory dynamically. New developers do have a hard time fighting with the borrow-checker early on. My meta-analysis of their comments indicates much of it is intrinsic to safely handling ownership and borrowing of references that C and GC'd languages didn't teach them. The tool just enforces rules (i.e. affine types) known to work. Learning curve is about 1-2 months of practice until they say borrow-checker rarely has problems with their code.

So, can someone today use Ada in a straight-forward way to write single- or multi-threaded applications that are, in every use-case, totally immune at compile-time to use-after-free and double-free errors with zero, runtime overhead? Or can it not do that?