3 ms·

>Can you elaborate? It's not often that they see valid critiques of Rust on HN, and it would be interesting (to me at least) to add to the data bank. Ehm, SPAR

>Can you elaborate? It's not often that they see valid critiques of Rust on HN, and it would be interesting (to me at least) to add to the data bank. Ehm, SPARK has a full proof capabilities, pretty much like you have in Coq (and SPARK integrates with Coq). With SPARK you can prove your code is correct, with Rust you can't, and there is nothing like Frama-C/SPARK available for rust. In Ada12/SPARK14 you have statically checked Hoare triplets (in Ada contracts are ensured in runtime sometimes tho), you can ensure that your output array is sorted in the type system and prove it statically, you can ensure all sorts of invariants statically. I like rust, but it's nowhere near proving correctness since it has neither dependent types (like F star/Low star` has), nor dedicated proof system (like Frama-C/SPARK). You can compare Rust to Ada, though Ada is pretty awesome two and have many features Rust lacks (contracts, subtypes, parametric modules).

touisteur 8y ago
And, even if you don't go 'full platinum level proof' (proof of all the High-Level specs of your software) in SPARK you can still enjoy, without too much effort: - proof of no read access to uninitialized variables - proof of absence of runtime errors (overflow, underflow, array out of bound, incorrect conversion...) - proof of type predicates/invariants, asserts, pre/post conditions... - Less known, you can specify and verify 'data provenance' with 'this function's result depends on parameters a and b c' aspects, and you can also specify and verify global variables access (global_in, global_out). This with a language that supports tasking, generics, and oop natively... And proof on access types (pointers) are on the way. Really amazing tech to work with.