Both Ada and spark have zero costs abstractions, they’re designed to run on embedded platforms.

Spark is a different use case from rust - it’s a full prover, and the goal is formal verification, typically in contexts where human life is at stake ( say, you’re writing software for an artificial heart , to take an extreme example ). This comes at the cost of being less flexible, but they’ve been slowly evolving spark so that it can handle increasingly complex cases .