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. -- Live well, ~wren _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
