Spark (Ada) for General Programming?

Question

Has anyone used SPARK or Ada for general programming, like JSON parsing, writing a web API, etc?The language is intriguing to me because of its safety guarantees. I believe it could compete with languages like Haskell and Rust in that area.It's on my list to learn. But one issue is that (I think) there's a preferred (and only one?) IDE for developing in it.See:https://www.cse.msu.edu/~cse814/Lectures/09_spark_intro.pdfhttps://en.wikipedia.org/wiki/SPARK_(programming_language)

_vdpp · Accepted Answer

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 per-package basis and either come back to it later, or just prove that callers to the function abide by the specification without the function body itself being legal SPARK.
For IDEs, I prefer VSCode over AdaCore's GPS IDE; AdaCore has a VSCode LSP plugin that I use: https://github.com/AdaCore/ada_language_server. Having said that, I used the GPS IDE for the computer architecture project and it worked well.
Good luck!

annexistrayline · Answer

You typically wouldn't write an entire program (unless it is really critical) in SPARK. The biggest payoff from SPARK is being able to prove that exceptions can't happen, and therefore you can turn off Ada's run-time checks. For mainstream applications like you're talking about, Ada works well with the run-time checks on, and exceptions doing their thing. This usually provides enough safety - and more safety than Rust imho.
We did use SPARK to implement a UTF-8 stream decoder, for example, as well as in core parts of a JSON parser, where speed and security are particular important. With SPARK, you want to use it in the really critical parts, since formal verification is hard and expensive. You use Ada for everything else - and you end up with something that is extremely robust.
As far as IDEs, honestly I use emacs, but AdaCore has a functional language server if you want to use VS Code. They also have their own GPL ide "gnat studio"

henrikeh · Answer

About a year ago on /r/Ada, there was a rather interesting discussion around using Ada for a website/webservice: https://www.reddit.com/r/ada/comments/7p12n3/going_allin_wit...