Hacker News new | past | comments | ask | show | jobs | submit login

For people wanting to learn, this article trying to use it for audio applications will give you a nice taste of the language:


This Barnes book shows how it’s systematically designed for safety at every level:


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:




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:


I'd also reference 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-develope... .

There's also 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 .

Then you might want to look up an implementation guidance : https://www.adacore.com/books/implementation-guidance-spark

And no I don't work for AdaCore :-D.

SPARK 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.

I 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.

Guidelines | FAQ | Support | API | Security | Lists | Bookmarklet | Legal | Apply to YC | Contact