Untyped Scheme should be built on Typed Scheme? WAS: Re: [plt-scheme] macro question

> An x86.  But it was probably *written* in C, which has a rudimentary
> type system.

1. That's not consistent with the direction of your argument for
Scheme, which is that you wanted the *lower* level to be typed, not
the upper levels that translate to it.

2. Your argument about C suggests that we have a vast disagreement
here.  Most people would say a type *system* consists of

- a definition of type attribution (eg, derivation rules)
- one or more algorithms for attribution types (esp. if the rules
  happen to be non-deterministic)
- a type soundness theorem that relates the static and dynamic
  semantics

C has none of these.  Though the first can be reconstructed (though in
a very machine-dependent way), and the second is straightforward, the
third is non-existent.  Indeed, as I discuss in PLAI, the third can't
even be meaningfully defined for regular C.

So you don't actually mean a type *system*; you mean some syntactic
means of rejecting programs, irrespective of the relationship to the
semantics (it could be sound, unsound, complete, incomplete, random).
But at least to me, an unsound type is even worse than not having one
at all (because it doesn't create a false sense of security).

>> You should also consider revisiting the end-to-end paper, if it's been
>> a while since you read it.
>
> The end-to-end paper?  Could you provide a reference?

http://en.wikipedia.org/wiki/End-to-end_principle

and the link to the original paper is at the bottom.

Shriram