[sdeframond]

> I think the hope for 2 is that those programmers would be forced into inaction by the language safety, rather than being allowed to cause problems.

Ah! That's funny :)

In practice there are always ways to circumvent safety, especially when it is easier than the alternative.

In a Typescript codebase I work on, I configured the type-checker to fordbid `any`. Should be easy enough to use `object` When we don't know the type, right? Well then things started being serialized into `string` way more often than I'd like...

[Groxx]

tbh if you think a serialized string bypasses anything in a proof-oriented language... I think that just means you haven't used one before. stringly-typed code is no less safe than strict types in these systems, though it's generally quite a lot more work: more things are fallible, and you need to repeatedly re-build or check every guarantee you are still requiring in other code that you interact with.

the exception is if you explicitly state X is a true statement, as many have some kind of bypass like that (an axiom or assumption or whatever). you could build a system that uses this everywhere to break most of the rules, like you can use `any` everywhere, but it'll be extremely obvious if that's the case.

[sdeframond]

Oh, it is obvious.

My point is: if you try to force people into inaction, chances are they will bypass you.