[racket-dev] math collection [was: Hyperbolic functions]
If even the few people who understand the type basis properly
get types wrong, why should you have programmers open up loopholes
into types that are supposed to "harden" their programs? When I have
just a few implementors manipulate the type base I can stick to the
allusion that the language is perfect and its implementation flawed,
but fixable. When everyone can open loopholes, I need to question
every single decision I made concerning such loopholes. (If we base
optimizations on them, we might descend into the C++ pit.)
-- Matthias
On Jun 26, 2012, at 9:34 PM, Robby Findler wrote:
> I agree with that, to a point. Here were are now considering a very
> concrete tradeoff, however: asking the user to cope with code
> duplication in return for ... what? Very little, I claim. In
> particular, I think that TR already has lots of type+contracts that
> are asserted (not proven) to be equivalent. For example, + seems to
> have a pretty big type in the implementation--- has that contract been
> proven to match to the type?
>
> That is, what I'm trying to say is that there are currently a few
> people that can make these unproven assertions about types and
> contracts that match up. Why should they be the only ones?
>
> EVEN BETTER: we can use random testing to falsify these!
> Systematically! Vincent is already doing this a little bit and he has
> found bugs. If we make this an explicit thing to connect types to
> contracts and allow people to make more connections, then we can do a
> better job finding bugs in the currently untested/unproven ones!
>
> (random testing uber alles :)