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