> SPARK is something I wish all languages were: formally provable as a first class citizen. It wouldn't make sense for the average language to make this a goal

> SPARK is something I wish all languages were: formally provable as a first class citizen. It wouldn't make sense for the average language to make this a goal. The cost is steep. To the typical programmer, SPARK looks like a thoroughly anaemic language, which of course it is. If Rust, say, had made formal verification a goal, it would have had to sacrifice its ergonomics to the point it would lose much of its appeal.