Comment by kibwen
3 hours ago
SPARK omits some features of Ada, so it would only reinforce the sentiment that bolting on verifiability after-the-fact is difficult. Expressivity is generally the antithesis of static analysis, and it's very easy and tempting to make a language that is accidentally too expressive to support a given analysis without being required to make breaking changes to reduce expressivity.
i mean in zig-clr it pushes you towards more expressive patterns, for example, making you label pointers as optional if their status is ambiguous