ada_language_server

It's also worth mentioning that Ada and SPARK are very easy to pick up these days. There's Cargo-like tool Alire [1], official VSCode plugin [2] and Open VSX plugin [3], Ada Language Server [4], Emacs Ada mode [5] and GNAT Studio [6]. With Alire one can easily install GNAT FSF builds (meaning GPL with linking exception) and SPARK tools. All libre software. Not to mention Ada being really versatile and well thought out language. And there's upcoming Ada 2022 standard [7]. [1] https://alire.ada.dev/ [2] https://marketplace.visualstudio.com/items?itemName=AdaCore.... [3] https://open-vsx.org/extension/AdaCore/ada [4] https://github.com/AdaCore/ada_language_server [5] https://www.nongnu.org/ada-mode/ [6] https://github.com/AdaCore/gnatstudio [7] https://learn.adacore.com/courses/whats-new-in-ada-2022/inde...

I recently used Ada (not the SPARK subset) to develop an assembler/simulator (for a made-up ISA) for a computer architecture course I was taking. I used the GtkAda bindings for the GUI, which worked well: https://github.com/docandrew/YOTROC I'm using SPARK for another project, and I think it's great. I don't think there is really an easier way of writing formally-verified software right now. Depending on the pre-conditions and post-conditions you put on your code, it can offer much stronger guarantees than other general-purpose programming languages do, but _proving_ those guarantees can be tricky if you don't have much experience with it. The nice thing about SPARK is that if you get something you can't prove (either because it's not legal SPARK or because the solver can't figure it out), you can turn off SPARK mode on a per-function or