Maybe it's time to give it a shot:
https://ada-lang.io/

It would be cool if you can get it going on a microcontroller without needing to pay license fees for commercial products.
You can. But even with 'alire', setting up the toolchain is a PITA (it's doable, but still annoyingly quirky, probably for lack of traction, so not enough people helping making this available for free).
One can start here:
https://blog.adacore.com/ada-on-any-arm-cortex-m-device-in-just-a-couple-minutesDon't expect it to work right as is described in the tutorial though in "a couple minutes". It probably won't happen. I tried on Linux and was able to get everything working (so up to generating the linker script and startup code) except getting the support for ARM cortex eabi, so building the project failed. 'alire' doesn't pull the compiler on its own as is "suggested". Or maybe I missed something. The Ada front-end for GCC for arm-none-eabi is not available directly in my Linux distro and I doubt it is in most others either. I think this can be downloaded from AdaCore, but didn't try going this route yet:
https://www.adacore.com/downloadTrying Ada for x86_64 targets on desktop is relatively easy though with alire, and can also be done without it, just with the raw GCC toolchain with the Ada front-end. If you're on Linux, many distros have a "gcc-ada" package of some kind.
Building the Ada front-end when building GCC for x86_64 is pretty much merely a matter of adding "ada" in the list of supported languages when configuring it, because the runtimes are already part of mainline. For embedded targets, that's not so and thus it's a royal pain. Too bad.
For those having a working GCC with the Ada front-end ("GNAT") on the desktop, here is a "bit more than hello world" to get you started, and the way you can build it purely with GCC/GNAT, without alire or gprbuild (which is a popular build tool for Ada).
with GNAT.IO; use GNAT.IO;
procedure Hello is
type Number is digits 12 range -999_999_999_999.0e999 .. 999_999_999_999.0e999;
function Sum(A, B : Number) return Number with
Pre => A <= 0.0 and B >= 0.0,
Post => Sum'Result = A + B;
function Sum(A, B : Number) return Number is
begin
return A + B;
end;
begin
Put_Line("Hello World!");
Put_Line("Sum(-2, 5) = " & Number'image(Sum(-2.0, 5.0)));
Put_Line("Sum(2, 5) = " & Number'image(Sum(2.0, 5.0)));
end Hello;
Name the source file "hello.adb".
It contains an example of a function with pre- and post-condition. As you may have guessed, the second call to Sum: "Sum(2, 5)" will fail as it doesn't match the pre-condition.
To build it:
gcc -c -Wall -gnata hello.adb
gnatbind hello
gnatlink hello
Note the '-gnata' option that is required to support assertions, which will trigger an assertion at run-time when executing the second Sum(). If you omit '-gnata', the two Sum() will execute ignoring the pre-condition. You can otherwise catch it with an exception block.
Now, apparently GCC doesn't support checking pre- and post-conditions at compile time, which is a bummer. I think Spark does.
Otherwise, you need to use a static analysis tool, such as GNAT SAS:
https://docs.adacore.com/live/wave/gnatsas/html/user_guide/introduction.htmlI think it's integrated in GNAT Studio, although that'll have to be checked.
And if you prefer using GNAT Studio (AdaCore's IDE), see here:
https://github.com/AdaCore/gnatstudiothere are Linux and Windows binaries.