> Again, I don't see how this is any different or special compared to any other programming language that would handle the error by asking the user to retry the function.
The blog's emphasis is that SPARK catches the possible error at compile time, so you can't forget/neglect to handle the error. Notice that neither rustc nor clippy complain at compile time about the potential OOB access in the Rust program that precedes the SPARK demo, while SPARK catches the potential issue in the naive translation.
> But I think the discussion here is about Rust, Ada, C/C++ no?
Sure, but my point is that type systems are not all equally capable. I don't think it's controversial at all that Rust's type system is capable of proving things at compile time that C++'s type system cannot, the most obvious examples being memory safety and data race safety. Likewise, SPARK (and C++, for that matter) is capable of things that Rust is not.
> The type system in Rust, Ada, and C++ are all robust enough at least to accomplish this.
I'm not sure about that? You might be able to approach what SPARK could do, but at least off the top of my head you'll need to make a check the compiler can't verify somewhere.
And that's just for this instance; I don't think Rust nor C++ are able to match SPARK's more general capabilities. For example, I believe neither Rust nor C++ are able to express "this will not panic/throw" in their type systems. There are tricks for the former that approximate the functionality (e.g., dtolnay/no_panic [0]), but those are not part of the type system and have limitations (e.g., does not work with panic=abort). The latter has `noexcept`, but that's basically semantically a try { } catch (...) { std::terminate(); } around the corresponding function and it certainly won't stop you from throwing or calling a throwing function anyways.
> Exactly! This is the root of my issue: you can accomplish this magical "proof" you speak of without using SPARK or Ada or any special "contract" language.
Perhaps I wasn't clear enough. I was trying to say that it's contradictory to complain about formal proofs while also claiming you can accomplish the same using other programming languages' type systems because those type systems are formal proofs! It's like saying "You don't need formal proofs; just use this other kind of formal proofs".
I don't think that assertion is correct either. The reason separate languages are used for this kind of proof is because they restrict operations that can't be proven, add constructs that provide additional information needed for the proof, or both. Perhaps as an extreme example, consider trying to make compile-time proofs for a "traditional" dynamically-typed language - Smalltalk, pre-type-hints Python, Lua, etc.