Discussions of dependent types often assume they're all about specification and proof. That's part of it, but not the most interesting bit.
-
-
Sometimes I also find it useful to state properties as types but leave them as axioms. It’s up to the programmer to decide when to stop.
-
Proofs and axioms are far from the only ways to use propositions. In fact, when it comes to programs (rather than math), I would say that they are the two worst ways. One promises everything yet provides little, and the other is too costly and provides too much (usually).
- 10 more replies
New conversation -
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.