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

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?

>> 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.  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.

Sam

> That is, what should guide is is NOT "do we have a theorem like some
> other big popular (or not so popular I guess) language?" but "what
> invariants should I help programmers that read my code be aware of?".
> While these are similar kinds of things, they are not just the same as
> "types = where invariants go" or "type soundness is what we need".
>
> As a concrete example: I think that our elimination of mutable cons
> cells was a change we made that made it far easier to reason about the
> correctness of our multithreaded code and this has nothing to do with
> types. (And just to be sure I'm being clear: types are a great way to
> get all kinds of invariants. I like that.)
>
> So, just to be sure we're all on the same page here: I'm writing all
> this as a counter argument to Matthias's claim about whether or not it
> is a good idea to allow users of TR to declare that specific types
> match up to specific contracts. I mean for all this email spooge to be
> considered only in that context, not in some more general way.
>
> Robby