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

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