Ask HN: SPARK2014 or Rust for high-integrity, secure, distributed application?

[eggy]

I have a job opportunity to develop a secure, high-integrity, high-reliability, very low fault distributed communications application where I will have the option of choosing the PL/platform. SPARK2014 has an edge over Rust due to its more venerable Ada relationship, verification toolset, and use in government contracts. I know Rust has gained a lot of traction, but the arena for this opportunity is slow to adopt new technologies. I didn't put Erlang/Elixir in the title, although the fault-tolerance and distributed nature of them has me interested especially NIFs in Rust. Any advice or tips are very much appreciated. Thanks!

[zelly]

Both of those choices have huge costs. SPARK may cost you actual money to use. It also takes longer to develop because of the large amount of safety checks. It is suitable for writing code that runs on nuclear missiles. But you may not actually need that level of correctness and can just use Java instead. Rust's safety features focus on memory errors, which with Java is already solved for you. Another aspect of Rust's safety is preventing data races, which Java doesn't guarantee prevention of but SPARK does[1]. Rust covers a small subset of potential errors your program could have whereas SPARK could find errors throughout your code including in logic. Honestly though most "high-integrity fault tolerant distributed systems" out are written in C++, so just using something like Java is already a massive improvement in safety. But if you must choose one of these two, then it must be for a good reason, so choose SPARK. Rust occupies this middle zone which is neither specialized for extreme correctness nor convenience like Python.

[1] https://docs.adacore.com/spark2014-docs/html/ug/en/source/co...