[bitc-dev] Comparisons with other languages: ATS
eschew at gmail.com
Sat Sep 4 15:40:30 PDT 2010
On Sat, Sep 4, 2010 at 5:56 PM, wren ng thornton <wren at freegeek.org> 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
> > 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.
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the bitc-dev