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"