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

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.

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

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