Discussions of dependent types often assume they're all about specification and proof. That's part of it, but not the most interesting bit.
-
-
But why should you express your understanding _in types_? Ultimately you'll get to the point that ties specification to proof. What if your understanding is hard to prove but easy to verify (well enough)? Limiting "understanding" to formal provability seems wrong for programming.
-
Who said anything about “limiting”? I find it helps me understand things. Using types doesn’t rule out using other methods.
- 12 more replies
New conversation -
-
-
I think teaching patterns too. What are the rough shapes that dependent typed programs take on, what does the code look like to work with those shapes?
-
Right. We need to explain ourselves better (and more experience!) but for now I would like people to see it as more than verification.
- 3 more replies
New conversation -
-
-
I may have brought this to your attention wi last 2yr (or maybe david
@d_Christiansen) http://www.lamdu.org/ https://vimeo.com/97713439 -
Yes, I know of Lamdu,
@EyalL gave me a demo a few years ago. It’s very promising. This is the sort of thing we’ll need.
End of conversation
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.