Don't forget there's a middle ground between not having them and manual, formal verification. It started with Eiffel with basic contracts that checked properties during testing and/or runtime. That did well in commercial deployments. SPARK took it formal with a basic, boolean encoding for programmer understanding. It uses a subset of Ada to prove absence of all kinds of error conditions without runtime checks or manual proof. It can optionally do more with a theorem prover but optional. Eschersoft did Perfect Developer to do it in high-level language with C, Java, or Ada generation. So, at least three are doing it in products with industry deployments with two highly concerned about performance in low-level applications.
Although I'm not getting into this dispute, I will add in general that Rust might benefit from such contracts or push-button verification of key properties as deployed successfully in Eiffel, SPARK, Ada 2012, and Perfect Developer. A language subset might be used like in SPARK to allow automated verification of those sections against common types of errors. Three follow-up benefits will be easier changes/integrations in maintenance phase, automated test generation from specs, and aiding dynamic analysis by giving it invariants to look at. Could be optimization benefits but I'm not qualified to say on that. Intuitively seems possible like using minimum-sized, data structure for a number range in spec or type. Stuff like that.
These techniques are really under-utilized despite being proven out many times over in high-reliability products.
Yeah, this exists, and would be interesting. I again think that it's a bit too extreme a solution to be baked into Rust itself, but I'd love a SPARKish Rust variant.
I'd like both. SPARK's stuff was ported to Ada 2012. It can be done for Rust as well. The trick is to make it optional so people don't have to pay attention to it. Maybe even have editors filter it out for people not paying attention to it. At the least, it being used in standard library and OS API's would let it enforce correct usage of those in debug/testing mode. 80/20 rule says that should have some impact given how much damage we've seen C and Java developers do misusing the foundational stuff.
Yeah, me too. However, I think we should wait for the formal verification of Rust to be completed before trying this. While it is possible to make something SPARKish without complete formal verification, it's probably better to build it using concepts learned during the formal verification.
Although I'm not getting into this dispute, I will add in general that Rust might benefit from such contracts or push-button verification of key properties as deployed successfully in Eiffel, SPARK, Ada 2012, and Perfect Developer. A language subset might be used like in SPARK to allow automated verification of those sections against common types of errors. Three follow-up benefits will be easier changes/integrations in maintenance phase, automated test generation from specs, and aiding dynamic analysis by giving it invariants to look at. Could be optimization benefits but I'm not qualified to say on that. Intuitively seems possible like using minimum-sized, data structure for a number range in spec or type. Stuff like that.
These techniques are really under-utilized despite being proven out many times over in high-reliability products.