[bitc-dev] [Fwd: BitC suggestions]
Jonathan S. Shapiro
shap at eros-os.org
Thu Jan 27 10:57:09 EST 2005
On Thu, 2005-01-27 at 15:42 +0100, Michael Weber wrote:
> * "Jonathan S. Shapiro" <shap at eros-os.org> [2005-01-26T10:54-0500]:
> > The hidden tax here is that evaluating a macro may imply calling a
> > previously defined procedure -- Lisp-like languages, including BitC,
> > tend to assume that the environment is built incrementally.
> Yes, but all this happens at compile-time (if EVAL and its ilk are
> disallowed, otherwise all bets are off anyway), so a call to a macro
> function eventually returns code. I would imagine this can be handled
> in the same manner as if a programmer would have written this code in
> the first place.
The problem here becomes to ensure that the evaluation environment
implemented by the compilation system matches the one implemented by the
> > The same problem arises if I can say something like:
> > (define a (f x))
> > where 'f' is a previously defined procedure.
> Well, first I'd need to know what the precise semantics of DEFINE
> would be in BitC. :)
> Assuming Scheme-like semantics...
There is no difficulty with understanding the semantics of the statement
above. The difficulty lies in the fact that a procedure evaluation is
being used to define static initial state of the program, and it is
exceptionally hard to reason statically about what the value will be.
In order to restore ability to reason, it may be necessary to restrict
the initializer to an expression in the functional, terminating subset
> The question is now what can be allowed and at what point is it
> sensible to start reasoning about a program?
> I guess one cannot say much about program behavior before all
> initializations are done. Further, if it is possible to assign new
Yes. That captures the issue nicely. Now consider further: if 'f' has
side effects, how are they understood?
What we really want is to be able to reason about the result of
evaluating a program from a known initial state.
> BTW: I seem to remember that ACL2 was used to model VMs (as well as
> real processors), which all have "global places" (registers etc.) so I
> would guess there is some way for ACL2 to cope with such constructs?
ACL2 has something called single-threaded objects. The difficulties we
ran into in ACL2 were:
1. The transform to single-threaded objects sufficiently obscures
the program as to make maintenance impractical.
2. The prover itself has some rather bad bugs.
3. The first-order restriction makes things like implementing
the BitC compiler itself difficult.
> One could also get rid of side-effects and state (which again brings
> us in the purely functional realms) but as I mentioned this makes
> matters simpler *only* if all the backdoors (like monads) go as well,
> and this pretty much renders the language useless, I guess.
One can do this in mathematics. One cannot do this in real systems
programs. I'm not interested in building a language for the sake of
building proofs. I'm interested in building proofs for the sake of
obtaining confidence in real, production software.
> Macros allow me to invent new syntactic expressions to express what I
> want to, and explain their semantics with language constructs which
> already have a precise semantics.
They also allow non-sensical introductions and unintended variable
capture, which is why hygenic macros took something like 15 years to
emerge and then wasn't real useful..
> I think its a perfectly reasonable thing to restrict the scope to a
> specific type of application. Evidently, what BitC seems to be
> designed for is bit-bashing and coping with a very spartanic
> environment (quite what you have right after booting a processor),
> while keeping things as safe as possible (type checking, ability to
> reason about code).
I disagree. A single-purpose language is a waste of energy in this
context. BitC is designed as a general-purpose language, not just s bit-
The problem with domain-specific languages is that they are either
narrow enough not to be very useful or general enough that htey
dramatically add to the burden of training and maintenance.
> On the other hand, why invent a new general-purpose language? There
> are many reasonable ones with a sizeable head start. Getting from
> scratch to a point where e.g. Gambit-C is right now is quite hard,
> especially if the team is small, and the real task is something else.
I would *love* to avoid building BitC. Can you identify *any* language
out there having all of the following properties:
1. A fully specified formal semantics, suitable for embedding
in a theorem prover.
2. Ability to express low-level data structure representation.
3. Sufficient abstractive power to qualify as a modern programming
I have looked, and I haven't found any language that satisfies more than
3 of these requirements. Usually, languages that satisfy (1) do not
satisfy *any* of (2,3,4).
However, if such a language exists then we don't need BitC.
> So, this begs the question: [devil's advocate] why not reuse a
> language and extend it where it is lacking?
Well, that's basically what we are doing. BitC may be viewed as ML with
the following changes:
1. Unambiguous surface syntax that is easily represented as data.
2. Addition of BOX/UNBOX for representation control.
3. Addition of syntax for low-level bitfields, and a greater range
of fixed-precision integral types.
4. Replacement of polymorphism with monomorphism+overloading, because
polymorphism has some rather bad type error problems when
it appears in the same language as mutation.
> BTW: two other language related things I'd like to shoot at you before
> I forget: in <http://www.archub.org/arcsug.txt>, grep for "Dave Moon:
> S-expressions are a bad idea" and "Dave Moon: Arc Syntax" (Note that I
> do not necessarily agree to all of what is said there.)
Of his comments on S-expressions, only point 1 is relevant to BitC. Note
that BitC does NOT include (list 'a) as a primitive type, nor does it
include symbols. Moon's arguments about interactions between cons cells
and source code and the merits of symbols aren't terribly relevant to
BitC, and (IMHO) they are in any case flatly wrong. BitC parens aren't
S-expressions, they are syntax.
I see Moon's argument concerning annotation. I just don't agree with it.
His proposal concerning Arc Syntax leads to a fundamentally non-parsable
language; one in which the parse table is changing on the fly as the
parser operates. Absolutely not! This mistake is one of the many reasons
that ML has nothing remotely like an unambiguous parse (well, this and
purely bad design).
> But even with a single processor you get concurrency due to process
> switching (in the form of interleaving semantics, seen from the
Not in a sensibly designed kernel, you don't.
> BTW: as far as I know, there is only one fully verified compiler
> around which can bootstrap itself (VLISP).
We're aware of that one. VLisp is great work.
More information about the bitc-dev