I’ve been looking at SPARK Ada after reading comments by users here, since I’m getting into embedded programming but don’t want to go back to writing C and C++. There are a number of very confusing things about SPARK Ada, licensing-wise - a cursory glance will lead you to believe it’s one of those closed-source tooling languages like MATLAB. This blog post cleared up some things.
I didn’t realize that I left this site up. This site is dead (archived) and should have been deleted. Most content got moved to over to ada-lang.io.
AdaCore has great learning material to get you started if you are interested. There is a PDF Introduction to Ada covering all language features in a comparative way to other languages, pointing out the advantages and different design decisions.
If you are particularly interested in SPARK and proofs/contracts/etc., consider the PDF Introduction to SPARK, which covers all the important points very compactly. You won’t need to read the Ada-Introduction, as most things will explain themselves automatically.
Ada/SPARK really are very fascinating programming languages that definitely do deserve some more love. For instance, there is a library called florist which provides complete bindings to the C POSIX API, but the packaging of it is a bit out of date. There was a release of version 22.0.0 in January 2022, but it has been barely packaged.
You do get along fine in most cases even without POSIX bindings of course.