points by William_BB 4 days ago | 0 comments
> If the caller is passing in something derived from their own arguments, or from I/O, all bets are off.
This is the part of contracts that I don't understand. I suppose you could (1) runtime validate any user input to the program and then (2) chain multiple functions like `safe_sqrt` that provide pre and post conditions.
In theory, this should allow the static analyzer to reason about any arbitrary input. However, this to me raises even more questions: is this practical, is this possible and why would I not try to achieve the same through types ("make invalid types unrepresentable"). Maybe I'm completely off the mark here.
If they can't, then it is IMO a mistake for the language to make contracts declarative (like types), or to think of the static checks as anything more than something extra on top of what is actually a runtime check. And if they can, then why are they not just types?
Bad idea to assume "someone will write static analyzers", and use that to justify a language feature capable of expressing much more complex logic than any static analyzer would be capable of handling.