ja, see the DDC thesis for notes about how things like Clean get ugly. http://www.reddit.com/r/programming/comments/92k52/type_inference_and_optimisation_for_an_impure/
On Sat, Sep 4, 2010 at 2: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. > > -- > Live well, > ~wren > _______________________________________________ > bitc-dev mailing list > [email protected] > http://www.coyotos.org/mailman/listinfo/bitc-dev > _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
