4 ms·
It seems to me that using dependent types to express the type "the number of primes below one million" would take at least as much code, and be at least as erro
by cousin_it 12y ago
It seems to me that using dependent types to express the type "the number of primes below one million" would take at least as much code, and be at least as error-prone, as writing that function in a dynamically typed language directly. In fact I'd be surprised if the dependently typed version were less than 2x the size of the direct version.
- codemac 12y agoThis is why they brought up the language that uses the same syntax for types as it does for your function definition. It really sounds like you haven't played with Coq or Agda.. because expressing these things are not that much code at all. Also the presentation literally covers that complaint, and how they think more programming languages are needed.