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).
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.
Here's another post with some examples: https://blog.adacore.com/taking-on-a-challenge-in-spark
There's a good book, Building High Integrity Applications in SPARK, that goes through things in detail. It's a good read for any programming language user to mine for ideas or explore how similar problems could be solved in their language: https://www.cambridge.org/core/books/building-high-integrity...