[bitc-dev] Macro removal rationale

[Jonathan S. Shapiro]

On Fri, 2006-07-21 at 22:41 +0200, Pierre THIERRY wrote:
> Scribit Jonathan S. Shapiro dies 20/07/2006 hora 12:04:
> > 3. Mark Miller's observation that macros obscure readability by making
> > it harder to understand what the code in front of you actually does.
> 
> The point is, macros are used to build new abstractions, and make these
> abstractions more readable, instead of crippling them with syntactic
> noise and boilerplate code.

This is not true. Rather: it is true when macros are used by good
programmers with good intentions, but even then it is very easy to write
bad macros. The problem with your statement is that it ignores the
possible *abuses* of macros by *hostile* programmers. It is
straightforward to write macros that appear plausible but completely
alter the program's behavior. Some of these can be subtle and very
difficult to audit.

> Then, in some way, their very role is to hide their internal details,
> but no more than any library call, with the difference that macros
> render abstractions in more readable way.

Only if they are used properly. Try to design a hostile macro as a
thought exercise. Ask yourself: how could I use the macro system to
introduce a compromise that would be very hard for an auditor to
discover?

>  I'm inclined to think, but I'm
> not audit expert, that compared to bare code, macros are indeed a
> problem, but compared to library calls, they have real advantages.

Not at all. Library calls exist within the semantics of the language and
can be analyzed. Macros do not.

I believe you are assuming that libraries are binary-only. We certainly
intend to support this in BitC, but not for programs that must be
analyzed.

> Is there some documentation on the various points that led to that
> consensus?

I'm not sure. I believe that the topic was discussed in the course of
the DarpaBrowser audit. I will ask Mark Miller to comment here.

> I wonder if it would be possible, in the case that the code dealing with
> macro expansion doesn't cause trouble to the team, to keep that code,
> even disabled by default, in the source tree.

I am not sure how this would help. Which code is being disabled here?

Many languages have done very well without this kind of extensibility. I
strongly doubt that this will be the first impediment for BitC.

Finally, remember that we are not committed to the S-expression syntax
in the long term. It is an initial expedience for investigating prover
issues.

shap