Comment by kibwen
18 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
A language is more expressive when it allows more programs and less expressive when it allows fewer programs. I don't know zig-clr, but if it rejects programs that Zig accepts (for example, by rejecting the aforementioned ambiguous pointers), then it is less expressive, not more (keeping in mind that being less expressive is not a pejorative).
no thats not the definition of more expressive. more expressive means the language can encode more programmer intent without making a dog's breakfast of the code.
1 reply →