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

On Tue, Jun 26, 2012 at 9:29 PM, Robby Findler
<robby at eecs.northwestern.edu> wrote:
> This sounds like a terrible solution.
>
> There are lots of places in our system where we just declare facts and
> don't prove them and then use them for lots of things (often
> optimizations). Why should this one be special?

I don't know of any places like this in Racket.  What are you thinking of?

Certainly, Typed Racket is intended to be sound in the same sense that
Racket is safe, and that Haskell, OCaml, and Java are safe as well: if
you don't use specifically-marked unsafe features (such as the FFI and
`racket/unsafe/ops`), then you get a guarantee that depends only on
the correctness of the runtime system/compiler, not on the correctness
of any user code.  I think this a very important guarantee: we've seen
far too often that trusting user code in languages like C and C++ was
a big mistake in many contexts.

Sam

> On Tue, Jun 26, 2012 at 8:16 PM, Matthias Felleisen
> <matthias at ccs.neu.edu> wrote:
>>
>> On Jun 26, 2012, at 9:12 PM, Neil Toronto wrote:
>>
>>> I'm addicted to optimizations. If I use Real -> Real, TR can't prove that (log1p 1.0) is Float and... hmm. I'll let Vincent explain why that's bad. :)
>>>
>>> Another option is to provide both log1p and fllog1p. I just wrote fllog1p anyway.
>>
>>
>> Sounds like the right solution -- and now you see how every type system forces you to duplicate code. -- Matthias
>>
> _________________________
>  Racket Developers list:
>  http://lists.racket-lang.org/dev