3 ms·
Agreed. Ada 2012 [1] and Spark [2] (an Ada subset with formal verification features) provide production-ready versions of most of these features. Clojure's sp
by thesuperbigfrog 8y ago
Agreed. Ada 2012 [1] and Spark [2] (an Ada subset with formal verification features) provide production-ready versions of most of these features.
Clojure's spec [3] is also promising for better specifications and more automated testing
Over the past decade or so, we have seen many mainstream programming languages adopt functional programming features. My hope is that more mainstream languages adopt preconditions, postconditions, invariants, and useful formal verification features. There are so many more great tools that could be used to build high quality software than unit testing.
[1] https://www.ada2012.org/ https://www.ada2012.org/
[2] https://en.wikipedia.org/wiki/SPARK_(programming_language) https://en.wikipedia.org/wiki/SPARK_(programming_language)
[3] https://clojure.org/about/spec https://clojure.org/about/spec
- int_19h 8y agoIf you look at the issue linked in the Rust tracker from the article, the people discussing this are specifically referencing Ada and SPARK. https://github.com/rust-lang-nursery/wg-verification/issues/14 https://github.com/rust-lang-nursery/wg-verification/issues/...
- thesuperbigfrog 8y agoNice! I did not have a chance to look at the issue discussion. Thank you for pointing it out. It's good to see that Rust is learning from Ada. Ada is also learning from Rust: https://arxiv.org/abs/1710.07047 https://arxiv.org/abs/1710.07047
- blub 8y agoC++20's getting contracts: https://en.cppreference.com/w/cpp/language/attributes/contract https://en.cppreference.com/w/cpp/language/attributes/contra...