* "Jonathan S. Shapiro" <[EMAIL PROTECTED]> [2005-01-26T10:54-0500]:
> [And my current response -- hopefully the sequence will stay on bitc-dev
> now.]
Thanks for the invitation! Maybe it's a good idea to forward the few
previous mails as well?
> On Tue, 2005-01-25 at 23:08 +0100, Michael Weber wrote:
> > > > * Macros
> > > We initially had DEFMACRO. It was taken out after it was pointed out
> > > that one absolutely cannot reason about this kind of thing successfully.
> >
> > I guess you asked the ACL2 people. With my very limited experience with
> > ACL2 I would've guess one can reason /after/ macro expansion.
>
> Didn't ask them, but we've used ACL2 experimentally. Macros are a train
> wreck, which is why they deal with post-expanded code.
>
> 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.
Of course, given this you cannot reason about macro functions
themselves, but I see no problem there.
> The same problem arises if I can say something like:
>
> (define a (f x))
>
> where 'f' is a previously defined procedure. I'm thinking that we
> probably do NOT want to allow this in BitC, and we will probably
> need to refine the specification accordingly. The main issue is that
> the evaluation "(f x)" will occur in an environment defined by the
> compiler, and we must contrive to ensure that it has **precisely**
> the same semantics that it would have in the target environment.
Well, first I'd need to know what the precise semantics of DEFINE
would be in BitC. :)
Assuming Scheme-like semantics, we have two parts here: the static
semantics declares a named place `a' (with initially undefined
content) unless it already exists, nothing exciting there. The
operational semantics then are equivalent to (set! a (f x)), I assume.
That is: "lookup a function F and variables A and X in the currently
active environment (toplevel), apply F to X, and store the result in
A. We also need to fix /when/ this statement is executed. Sensibly,
the effect would be the same as a toplevel looking like:
(begin
...
(set! a ...)
...
(main))
with initializers executed in textual order. I don't have RnRS at
hand but I guess this is similar to what Scheme does. (I assume you
know all this, I just am writing it to ensure that we talk about the
same things).
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
values to toplevel variables at arbitrary points during the run you
will run into pretty much the same problem.
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?
Of course, you could go radical and disallow global variables at all,
like in Haskell. Down that path lies madness. I can show you
horrible way to fake them, and how many non-trivial Haskell programs
precisely do this because they are so convenient (purely functional,
ya right! ;)).
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.
> The main issue is that the evaluation "(f x)" will occur in an
> environment defined by the compiler, and we must contrive to ensure
> that it has **precisely** the same semantics that it would have in
> the target environment.
Hmm, could you give another example of the problem?
> > Are you planning on any builtin language support for this (database-like)
> > functionality?
>
> Absolutely not! Two reasons:
>
> 1. If the language isn't good enough to let us construct the necessary
> abstractions for this within the language, we need a better
> language!
That's why I suggested macros. They kind of "open-code" the compiler,
which has a ton of advantages (and a few complications...).
[I am trying hard not to go into philosophical ramblings about
compilers in general ;)]
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.
The compiler should provide me with a set of "axioms" to build on to
make life easier. Apart from that, it should be as simple as
possible, in my opinion.
> 2. Much of this sort of thing is highly application dependent. We don't
> see BitC as a purely OS-oriented language (what a bad cost/benefit
> tradeoff *that* would be).
Oh, then I misinterpreted the scope a little. I was thinking that
"systems programming language" means "OS and maybe one layer above",
but not general-purpose.
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).
Domain-specific languages help making code understandable because they
let the programmer concentrate on what needs to be done, with the
right level of details visible. Bonus points, if the host language
supports the construction and usage of DSLs in a natural way.
For example, Bossa <http://www.emn.fr/x-info/bossa/> does this for
writing schedulers.
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.
So, this begs the question: [devil's advocate] why not reuse a
language and extend it where it is lacking?
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.)
> About the only piece I'm tempted to (someday) consider language support
> for is concurrency, but there only seem to be two classes of languages
> in the world:
>
> + languages without direct concurrency support
> + languages with bad concurrency support
Yes, there are many of these. But there's also Erlang
<http://www.erlang.org/>, Mozart <http://www.mozart-oz.org/> and Alice
<http://www.ps.uni-sb.de/alice/> which have nice concurrency models.
> E, please note, does not support concurrency in the sense that I
> mean; all behavior within a VAT is single-threaded behavior. In any
> case, the E model wouldn't be appropriate for an SMP kernel.
I don't know much about E besides the name, so I cannot immediately
comment on it. What is the role of a VAT?
Recently, I looked into SMP support of the NetBSD kernel, and even
with this rather coarse "Biglock" model it is not immediately obvious
what's going on, and more importantly, why.
Of course, with multi-core processors already there and the hype
around Cells, it is clear that good ways to express concurrency will
become more important, and a language supporting it has advantages,
obviously.
But even with a single processor you get concurrency due to process
switching (in the form of interleaving semantics, seen from the
kernel) , and being able to specify this within the language might
e.g. help to avoid explicit locking schemes.
> At a high level, the more you build in to a language the more you have
> to build in to the prover and the less credible the verifications
> become.
Well, if there is something lacking in the language, it won't be long
until it is reinvented (likely in a poorer way than with compiler
support), and then the prover has to deal with it anyway. It's also a
question from where do you start to "trust"? :) At compiler level?
BTW: as far as I know, there is only one fully verified compiler
around which can bootstrap itself (VLISP).
BTW2: one can use macros to reason about code, see e.g. Kiselyov's
<http://okmij.org/ftp/Scheme/callcc-calc-page.html>. Describes
source transformations expressed as macros.
BTW3: although it might seem so, I am not trying to push macros. As I
said, I fully understand the issue of limited work force.
> > As I said, I was considering a future project along the same lines until I
> > found Coyotos.
> Then perhaps you should join this one!
Well, I'll be available at around end of this year ;)
Jokes aside, I see what I can do.
Cheers,
Michael
--
You find yourself in a twisty maze of kernel traps, all alike.
> go west
You find yourself in a twisty maze of kernel traps, all alike.
>
_______________________________________________
bitc-dev mailing list
[EMAIL PROTECTED]
http://www.coyotos.org/mailman/listinfo/bitc-dev
