AdaCore Blog

>> I don't know Ada well personally
>> But I'm not very educated.

If you don't know, please don't speculate.

I use Ada professionally and I am experimenting with Rust. Rust has great promise and I am interested to see where it will go, especially as an alternative to C++.

>> it's a bit less advanced than Rust at static checks

Ada 2012 has comparable and in many cases more advanced static checks than Rust with the exception of memory management. This is especially true of the Ada type system (https://learn.adacore.com/courses/intro-to-ada/chapters/strongly_typed_language.html) and design by contracts (https://learn.adacore.com/courses/intro-to-ada/chapters/contracts.html).

If you use the SPARK subset of Ada, you can use advanced tools to prove the correctness of your program. See https://learn.adacore.com/courses/intro-to-spark/index.html

Rust's borrow checker approach to memory management is novel and SPARK is acutally adding similar concepts to the next version of SPARK (https://blog.adacore.com/using-pointers-in-spark).

>> a good bit simpler than Rust and Swift but more complex than Go

Ada is a large and fairly complex language because it was designed for hard real-time, safety-critical, embedded systems and it has been in real-world use for 40+ years. I don't think it is that simple, but judging simplicity is subjective: what one person sees as complex, another person might see as simple. You can browse the Ada 2012 Language Reference Manual and see what…

I'm disagreeing with the assertion that Ada looks like COBOL. You may or may not agree with that statement, but you made it.

> This filtering process happens in the crudest possible way, based more on feelings and hearsay than on verified facts

And that's why people should stop making statements like:

>>> Ada, unfortunately, looks cobol-like, so someone who knows nothing automatically assumes a ton of bureaucracy. Run away if you want work done.

Without much stronger caveats to clarify that it is not a correct impression. Without a strong statement clarifying that it's only an impression (based on the most superficial of analyses) and not the reality, people will read comments like yours (and others in threads like this one) and never go any further to realize that they're false, and end up repeating them.

In an Ada thread just a few weeks back someone wrote COBOL-ish code claiming it was Ada code. It was a math-y example like the GCD code above, and clearly wouldn't work if you had even a passing familiarity with Ada. But it was written in such strong terms that it gave the impression the author was competent when they were really ignorant.

> If you look at rust, the work done by Mozilla and people like e.g. Steve Klabnik to put the language on the map is enourmously valuable. With code examples, blog post, fixing real world pain points, answering questions, .... It took years but they did it. If Ada had a group of people and a bigname organization, all doing this…

Hah, Chevy Spark, and it's a gasoline car!

I usually put "SPARK2014 programming" or "SPARK2014 Ada" in my searches. I used to get annoyed by all of the Apache Spark stuff that came up, but that seems to have waned a bit this past year or two.

Vermont Technical College (VTC) used SPARK2014 to program their CubeSat and the book, "Building High Integrity Applications with SPARK"[1] is a great intro to it in a nice context of practical use.

There was also an article on the AdaCore site about someone who rewrote some drone firmware in SPARK2014, which is another nice real-world application. [2]

[1] https://www.amazon.com/Building-High-Integrity-Applications-SPARK/dp/1107040736/ref=sr_1_5?crid=3OQW9ZYPSM71A&keywords=high+integrity+software&qid=1662723880&sprefix=high+integrity+sloftware%2Caps%2C60&sr=8-5

[2] https://blog.adacore.com/how-to-prevent-drone-crashes-using-spark

Who said anything about RAII? Having RAII doesn't make C++ memory safe. If you can take a reference or pointer to some RAII-created vector, and access it after the vector is gone… then you're not memory safe?

Yes, SPARK exists, and is very cool. I think there's work on a similar system for rust (or ferrocene, anyway, which is being co-developed by AdaCore: https://blog.adacore.com/adacore-and-ferrous-systems-joining-forces-to-support-rust). It also seems that SPARK now has memory ownership and aliasing support, but only since ~2019 (https://blog.adacore.com/using-pointers-in-spark), and with clear inspiration from rust. It seems to me that this addition to SPARK was felt necessary by the AdaCore people, meaning that rust had something Ada did not support (or did not support well).

People who don't want to read the first line of the article, rejoice!

It sounds like a good decision though. Formal verification tends to make more sense in highly concurrent situations where there is a high-value stable API to be supported. That describes graphics cards and surrounding environments really well so it makes sense that Nvidia would find use cases.

Something more from the article is also that they made the decision with a pilot project that went well. It'd be nice to have more details about it; that sort of thing is important to do well and always interesting. Lo and behold, we do have more details about it! https://blog.adacore.com/when-formal-verification-with-spark-is-the-strongest-link - there is a video in there that looks to be worth a watch.

Ada is something I've always wanted to get into (it interests me that there's a low level programming language that came around at the same time as C but just never took off)

Ada has a bunch of features built into it already, including concurrency support with tasks [0]

I just haven't found the right motivation to figure out what to do with it yet. Maybe I could play around with the Raylib bindings [1] at some point?

There's also the SDL bindings, which a LOT of work has seemingly gone into [2]

[0] https://learn.adacore.com/courses/intro-to-ada/chapters/tasking.html

[1] https://blog.adacore.com/ada-gamedev-part-3-enjoy-video-games-programming-with-raylib-2

[2] https://github.com/ada-game-framework/sdlada