[dnautics]

empirically untrue. several projects exist that bolt on extra safety to unsafe languages or unsafe parts of language. SeL4 for C, MIRI for rust unsafe. i guess ada/spark for ada too, is the OG, spark being added to ada 4 years after its first release

[afdbcreid]

Hardening is definitely possible, we've had sanitizers in C/C++ for a long time. It's not full memory safety though. Miri is the same.

SeL4C is formal verification, and while it can prove memory safety (and much more) it is much more difficult, to the point that you're basically programming in a different language.

Ada/SPARK is your best example, and also the example I know the least of, so I won't comment on.

[kibwen]

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.

[dnautics]

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

[kibwen]

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).

[dnautics]

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.

[kibwen]

Now we're just having a semantic argument over the word "expressiveness", which is not especially interesting; see https://chrispenner.ca/posts/expressiveness-spectrum . My argument above remains true regardless of the terms you choose to use.