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

Do you only use code that uses the FFI that people you trust wrote?
How about code in the runtime system? Both of these have lots of
people contributing code that can (and does) easily undermine basic
Racket guarantees, and you don't complain about that. Do you care
about type system guarantees more than basic safety guarantees?

Stepping back, I don't like this general philosophy. Relying on "proof
by smart implementer" is borderline immoral to me. I think have a
declarative language that programmers can program to specify what they
want to specify is the right approach to most everything, including
the specification of optimization opportunities and typed/untyped
boundaries, and whatever else. (I think we don't do this for
inlining-type optimization is that generalizing to a language is hard,
not because we don't want to do it.)

I do think that we have to rely on people being responsible for their
code and I don't mean to imply otherwise, but throwing up arbitrary
boundaries like this doesn't (in my opinion) actually help anyone
guarantee anything in practice.

Robby

Technical note: I was wrong below -- I only know of bugs Vincent found
between the type declarations and the untyped implementation, but I
think both of our comments still stand in light of that revision.

On Tue, Jun 26, 2012 at 8:42 PM, Matthias Felleisen
<matthias at ccs.neu.edu> wrote:
>
> 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 :)
>