On Sat, Sep 4, 2010 at 5:56 PM, wren ng thornton <[email protected]> wrote:
> On 9/4/10 11:48 AM, Ben Karel wrote: > > The example code for a function that provably > > sorts its input list is cool in theory but (at least to my untrained > eyes) > > impenetrable in practice. > > That's the standard problem with any of today's dependently typed > languages, unfortunately. At least you have the benefit that, so long as > /someone/ can penetrate it, you have a formal proof of correctness. > That's a heck of a lot better than impenetrable code written in, say, C. > But, honestly, this is one of the reasons dependent types haven't moved > beyond theorem proving and started making a real impact on programming yet. > And why DML-style index sorts seem to hit such a sweet spot. Many of the standard examples of dependent types are indexed by natural numbers. I think it's because such examples tend to fall in the intersection of easy-to-grasp and obviously-beneficial. Forcing constraints to be linear might be a slight hassle in practice (no personal experience) but I suspect that programmers would grumble and accept it, knowing that it's a small price to pay for guarantees of both safety and (compile + runtime) performance.
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
