>>7
Most language features that have ever existed were developed in some Lisp dialect before they appeared elsewhere, but that doesn't invalidate their later appearances.
I assume >>1-kun has little to no experience with any of these languages, so I gave him the basics. You're right that SPARK is an insane choice for writing a forum. Even normal Ada demands too much ceremony for me to enjoy working with it. Maybe >>1-kun will feel differently, or maybe not.
Also, very few people are using real formal verification techniques with Rust, partly because those tools aren't mature, and partly because you can get pretty far by hacking together some primitive "proofs" using tricks like session types. However, Rust does give you a higher baseline for reasoning about mutable state when compared to stock Ada, and the borrow checker is far less difficult to work with than SPARK.