Thanks for your correction. I think we're saying the same thing.
Although I think that the safety we claim to have isn't really there
with unsafe ops and the FFI. I can copy the definition of a closure
out of the C headers into an FFI struct, cast the _racket pointer to a
_closure-pointer, and read out the values.
Here's an example:
#lang racket/base
(require ffi/unsafe
rackunit)
(define-values (one two f)
(let ()
(define one (cons 1 null))
(define two (cons 2 null))
(values one two
(λ (x) (cons x one)))))
(check-equal? (f 1) (list 1 1))
(ptr-set! (cast f _racket _pointer) _intptr 2
(cast two _racket _intptr))
(check-equal? (f 2) (list 2 2))
This is something where it is normal to say we can ignore it, because
no one would really do that. But on the other hand, the Arc uses a
very similar thing to make conses mutable again (implemented for them
by Eli.)
I see the connection between types and contracts to be at a similar
level to the FFI/unsafe. I don't think everyone should do it, but I
think it should be "easy" to opt-in to such a connection.
I also would like to see a macro-like compiler extension API for
hooking into optimizations and different specialized JITing. Things
like that are a very effective use of template meta-programming in C++
that I think we could do better.
I think your restatement of my claim is excellent, that we have done a
great job so far, and we should continue doing a great job.
Jay
On Thu, Jun 28, 2012 at 9:50 AM, Matthias Felleisen
<matth...@ccs.neu.edu> wrote:
>
> I found your message strange and I contemplated whether I should reply on
> 'dev' at all.
>
> In the interest of sharing and evolving the Racket idea, I am going with a
> response on 'dev'. Your central claim is that "the programming language
> implementer is not a member of an elite, enlightened caste that can make
> choices mere mortals cannot." Without any constraint this claim is plain
> wrong (like many general claims). You simply do not want every programmer to
> plug code into the JIT easily. You do not want #%plaiin-module-begin change
> meaning on you. You do not want to specify types so that the compiler
> randomly mangles bits for you and claims that they are the result. You can
> see that this is wrong with all the security that Matthew carefully adds to
> the implementation (not to speak of the design idea, which is abstract
> anyway). If we didn't want to restrict access to certain pieces in certain
> ways, why bother with inspectors and armed syntax and generative structs for
> basic forms. Why not allow (closure-environment (lambda (x) x)) to expose the
> pointer to the environment? (Which you can do in MIT Scheme, though there is
> called cadr.)
>
> I think the closest we have come to your claim is that
>
> we wish to push back the boundaries without giving up safety and security.
>
> Finding this middle ground of a high degree of expressivity with good
> constraints imposed on it is the purpose Racket and PLT. And we have done
> really well with it for a long time
>
> -- Matthias
>
>
>
>
>
>
>
>
> On Jun 27, 2012, at 2:12 PM, Jay McCarthy wrote:
>
>> FWIW, I agree with Robby and have had similar conversations with Sam
>> in person. (Although for me it is that I wish I had the ability to
>> claim that macro pieces had certain types regardless of what TR could
>> infer from the generated code.)
>>
>> I think a big part of the Racket philosophy is that the programming
>> language implementer is not a member of an elite, enlightened caste
>> that can make choices mere mortals cannot. This philosophy is the root
>> of what I find beautiful about macros, continuations, first-class
>> synchronization, and structure type properties, for example.
>>
>> Although I am not directly writing anything for the TR implementation,
>> I have opinions about the goal of that project. To me, it is not
>> "figure out a type system that is passable for Racket programs" but
>> "make a type system that is to existing type systems as Racket is to
>> pedestrian languages" ---- in particularly, by allowing more
>> extensions (type or otherwise) to be done in language.
>>
>> I see Robby's point about contract / type isomorphism and mine about
>> more powerful type macros as steps in that direction.
>>
>> <3
>>
>> Jay
>>
>> On Tue, Jun 26, 2012 at 10:10 PM, Robby Findler
>> <ro...@eecs.northwestern.edu> wrote:
>>> Consider me done!
>>>
>>> Robby
>>>
>>> On Tue, Jun 26, 2012 at 11:05 PM, Neil Toronto <neil.toro...@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<sa...@ccs.neu.edu>
>>>>> wrote:
>>>>>>
>>>>>> On Tue, Jun 26, 2012 at 10:44 PM, Robby Findler
>>>>>> <ro...@eecs.northwestern.edu> wrote:
>>>>>>>
>>>>>>> On Tue, Jun 26, 2012 at 9:25 PM, Sam Tobin-Hochstadt<sa...@ccs.neu.edu>
>>>>>>> wrote:
>>>>>>>>
>>>>>>>> On Tue, Jun 26, 2012 at 9:29 PM, Robby Findler
>>>>>>>> <ro...@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
>>>
>>> _________________________
>>> Racket Developers list:
>>> http://lists.racket-lang.org/dev
>>
>>
>>
>> --
>> Jay McCarthy <j...@cs.byu.edu>
>> Assistant Professor / Brigham Young University
>> http://faculty.cs.byu.edu/~jay
>>
>> "The glory of God is Intelligence" - D&C 93
>>
>> _________________________
>> Racket Developers list:
>> http://lists.racket-lang.org/dev
>
--
Jay McCarthy <j...@cs.byu.edu>
Assistant Professor / Brigham Young University
http://faculty.cs.byu.edu/~jay
"The glory of God is Intelligence" - D&C 93
_________________________
Racket Developers list:
http://lists.racket-lang.org/dev
