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

Consider me done!

Robby

On Tue, Jun 26, 2012 at 11:05 PM, Neil Toronto <neil.toronto at gmail.com> wrote:
> I haven't got a clue what you two are arguing about anymore. If you both
> stop, maybe Sam can implement that perfectly safe change to the typed ->
> untyped contract barrier that he said he could do. That would be nice.
>
> ;)
>
> Neil ⊥
>
>
> On 06/26/2012 09:23 PM, Robby Findler wrote:
>>
>> On Tue, Jun 26, 2012 at 10:08 PM, Sam Tobin-Hochstadt<samth at ccs.neu.edu>
>>  wrote:
>>>
>>> On Tue, Jun 26, 2012 at 10:44 PM, Robby Findler
>>> <robby at eecs.northwestern.edu>  wrote:
>>>>
>>>> On Tue, Jun 26, 2012 at 9:25 PM, Sam Tobin-Hochstadt<samth at ccs.neu.edu>
>>>>  wrote:
>>>>>
>>>>> 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?
>>>>
>>>>
>>>> The inliner and the JIT compiler and that whole interaction are the
>>>> ones I thought of. I should have said "lots of facts" not "lots of
>>>> places", tho. Sorry about that.
>>>
>>>
>>> I'm still not sure what you're thinking of.  What operation does the
>>> inliner or JIT perform that is justified by a
>>> programmer-declared-but-not-checked fact?
>>
>>
>> There are many operations that are implemented partially in JIT and
>> wholly in the runtime system. The JIT generated version gets used
>> unless certain conditions hold, in which case the runtime system
>> version gets used. The programmer declared fact is embedded into the
>> code and not specified as a fact per se, but for example, there is one
>> such fact saying "this pile of assembly instructions is equivalent to
>> the C implementation of list-ref, under the condition that the number
>> argument is a fixnum less than 10,000 and we don't run out of pairs
>> too soon" (roughly). There are large pile of such things. Another one
>> you're probably more familiar with: "this pile of assembly
>> instructions is equivalent to + when the arguments are both fixnums or
>> both flonums".
>>
>> There is another pile of such invariants in the (pre-bytecode level)
>> inliner. It relies on beta substitution and the ability to run certain
>> primitives at compile time. (I don't know as much about that one, so
>> probably there are more things it relies on than that.)
>>
>>>>> 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.
>>>>
>>>>
>>>> Of course I understand this. I'm pointing out that this is not a
>>>> significant guarantee, in and of itself (see last para below for an
>>>> elaboration here).
>>>>
>>>>>  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.
>>>>
>>>>
>>>> I don't think this is an either/or. Indeed, just to continue with C:
>>>> if everyone understood that the types were really just size markers
>>>> and nothing else, then lots of the seeming unsoundness goes away in C
>>>> (not all, of course, and as I've been learning from Regehr's blog,
>>>> there are lots of other dark corners). But no one is suggesting we
>>>> remove checks from array bounds, which is what really cost society
>>>> money wrt to C and, IMO, the kind of invariant that matters.
>>>
>>>
>>> I don't think the distinction that you're trying to draw here is
>>> meaningful.  In particular, to return to our earlier example, if you
>>> assert the type Neil gave for an untyped value, backed up with the
>>> contract `(->  real? real?)`, then Typed Racket's type system can be
>>> off by arbitrarily much -- no claim it makes can be trusted.
>>
>>
>> I think you're making this out to be a boogey man, when it really isn't.
>>
>> But why doesn't your argument apply to any program that uses the FFI?
>> It also invalidates all of the guarantees that TR makes. (And there
>> are essentially no programs that don't use the FFI anymore.)
>>
>> And anyways, I think that TR actually makes *no* guarantees in a
>> precise technical sense. Even if I accept the proofs about the models
>> in your papers then (as I said earlier) we are not running your
>> models. Why should you be the only allowed to introduce these
>> particular bugs? I'm allowed to introduce other bugs, for example.
>>
>>> Further,
>>> the optimizer will happily transform your program from one that
>>> behaves one way to a different program, and cause the entire Racket
>>> runtime to segfault.  So if we went the route that you're suggesting,
>>> Typed Racket might serve the "what invariants should I help
>>> programmers that read my code be aware of?" role, but we'd have to
>>> take out the optimizer, and the claims that if Typed Racket tells you
>>> something, then you know it to be true (modulo the extensive caveats
>>> about bugs in TR, Racket, GCC, Linux, Intel, etc).  I don't think
>>> that's the right trade to make.
>>
>>
>> (I don't really get what you're saying here at all, but I also think
>> it isn't really an argument against my argument.)
>>
>> But I'll note that you forgot perl in your list. I'm sure it is used
>> in the build process of one of those tools that we rely on.
>>
>> Everything is hopeless.
>>
>> Robby
>>
>> _________________________
>>   Racket Developers list:
>>   http://lists.racket-lang.org/dev
>
>
> _________________________
>  Racket Developers list:
>  http://lists.racket-lang.org/dev