[racket-dev] math collection [was: Hyperbolic functions]

From: Matthias Felleisen (matthias at ccs.neu.edu)
Date: Tue Jun 26 21:42:18 EDT 2012

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 :)


Posted on the dev mailing list.