I'm happy to see people talking about the problem posed by implicit invariants, but this post strikes me as defeatist. This line especially:
> Implicit invariants are, by definition, impossible to enforce explicitly.
Yes, Hyrum's Law (and, at the limit, Rice's Theorem) and all that means that we won't ever be perfect, but just because an invariant is currently implicit doesn't mean it must remain implicit forever. We can identify classes of implicit invariants and make them explicit using things like type systems.
I understood article saying that implicit invariants are like undocumented choices.
If I have blog where blogposts have maximum length of 4096 bytes. But why would there be such limit, is it creative decision? is there technical limitation? was it just some "good enough" number when blog was created?
I don't think type systems really can encode these reasons. You see the constraints but not the reasoning.
type BlogPostThatFitsInSMS = BlogPost<FixedString<150>>
No one would write this type in the real world (and most type systems can’t encode it), but you see lower-level sorts of reasoning all over the place in type systems.
> Implicit invariants are, by definition, impossible to enforce explicitly.
Yes, Hyrum's Law (and, at the limit, Rice's Theorem) and all that means that we won't ever be perfect, but just because an invariant is currently implicit doesn't mean it must remain implicit forever. We can identify classes of implicit invariants and make them explicit using things like type systems.