10 ms·
For people wanting to learn, this article trying to use it for audio applications will give you a nice taste of the language: http://www.electronicdesign.com/e
by nickpsecurity 9y ago
For people wanting to learn, this article trying to use it for audio applications will give you a nice taste of the language:
http://www.electronicdesign.com/embedded-revolution/assessing-ada-language-audio-applications http://www.electronicdesign.com/embedded-revolution/assessin...
This Barnes book shows how it’s systematically designed for safety at every level:
https://www.adacore.com/books/safe-and-secure-software https://www.adacore.com/books/safe-and-secure-software
Note: The AdaCore website has a section called Gems that gives tips on a lot of useful ways to apply Ada.
Finally, if you do Ada, you get the option of using Design-by-Contract (built-in to 2012) and/or SPARK language. One gives you clear specifications of program behavior that take you right to source of errors when fuzzing or something. The other is a smaller variant of Ada that integrates into automated, theorem provers to try to prove your code free of common errors in all cases versus just ones you think of like with testing. Those errors include things like integer overflow or divide by zero. Here’s some resources on those:
http://www.eiffel.com/developers/design_by_contract_in_detail.html http://www.eiffel.com/developers/design_by_contract_in_detai...
https://en.wikipedia.org/wiki/SPARK_(programming_language) https://en.wikipedia.org/wiki/SPARK_(programming_language)
https://www.amazon.com/Building-High-Integrity-Applications-SPARK/dp/1107040736 https://www.amazon.com/Building-High-Integrity-Applications-...
The book and even language was designed for people without a background in formal methods. I’ve gotten positive feedback from a few people on it. Also, I encouraged some people to try SPARK for safer, native methods in languages such as Go. It’s kludgier than things like Rust designed for that in mind but still works.
GPL download for AdaCore GNAT:
https://www.adacore.com/community https://www.adacore.com/community
- mcguire 9y agoSPARK might be kludgier than Rust, but the guarantees it can make are stronger. And from what I've seen, it's less kludgy than the dependent type systems I've seen.
- nickpsecurity 9y agoI meant integrating it into FFI's expecting C code. It's true that it makes stronger guarantees. I have a concept also that's called Brute Force Assurance where one source gets converted into Rust, Frama-C, and SPARK. Idea is static analysis tools for each knock out errors others can't catch. Final result is portable C.
- touisteur 9y agoI'd also reference Rosetta Code (http://rosettacode.org/wiki/Rosetta_Code http://rosettacode.org/wiki/Rosetta_Code) to get a taste of Ada. I use it sometimes when I forget some simple stuff. For C++ and Java practitioners : https://www.adacore.com/books/ada-for-the-c-or-java-developer https://www.adacore.com/books/ada-for-the-c-or-java-develope... . There's also http://university.adacore.com http://university.adacore.com . For Spark2014 you might want to start with AdaCore University also, or if you're in Paris in December there is a public training session : https://www.adacore.com/public-spark-training https://www.adacore.com/public-spark-training . Then you might want to look up an implementation guidance : https://www.adacore.com/books/implementation-guidance-spark https://www.adacore.com/books/implementation-guidance-spark And no I don't work for AdaCore :-D.