4 ms·

Sounds like you're describing dependent types. You've now got the problem that showing your program is correct involves writing maths proofs that show your prop

• nine_k 6y ago
  But maybe analyzing all cases is not needed if we know (or postulate) something about the predicates? E.g. we can prove (or just assume since the case is simple) that construction of Norm3 is defined for any triple except (0, 0, 0), and that it is preserved under rotation and under reflection, but guaranteed to be broken under addition. I suspect that if we factor out such basics, the amount of proof for a reasonable function may become manageable.
  • seanwilson 6y ago
    > or just assume since the case is simple That's like what the blog post is about where you're tagging values you assume have a certain property. > I suspect that if we factor out such basics, the amount of proof for a reasonable function may become manageable. It's not obvious how you contain the complexity though and you don't need a lot before it becomes well beyond practical for even experienced programmers. The moment you have to write an algebraic proof where variables are multiplied together you're in the realm of nonlinear arithmetic which is undecidable for example, and writing proofs is hard. Mainstream languages contain the proof complexity by limiting what you can express e.g. it's trivial for the computer to prove "String = String" and "Dictionary = HashTable" as part of type checking.