I am thinking ahead about proving things, and I am becoming concerned
about the generality of BitC initializers.
Since we don't have italics in email, I will try to use *lowercase*
where I mean to be referring to metasyntax, and uppercase for real code.
The current language allows general initializers of the form
(DEFINE identifier expression)
with the intended meaning that the identifier should be bound to the
result of the expression. Thus
(DEFINE abc (+ 2 3))
does what you expect.
It has lately occurred to me that this introduces an issue that may
prove to be a problem for later verification. My concern is that the
expression may have side effects, and that this makes a very complex
mess out of the notion of "initial state."
Let me come at this backwards in an attempt to expose where my concern
is coming from.
Suppose we restricted the initializer expressions to say that they must
fall (recursively) within the purely functional subset of the language,
and further declare that they must terminate. If these restrictions are
put in place, then every initializer like the one above can be resolved
at compile time to some particular value. The very nice thing about this
is that if we want to define the notion of "initial global program
state", we can simply imagine wrapping all of the global variables
within a structure. Each field will have a well-defined initializer,
which means that we can actually instantiate this type statically and
maybe reason about executing the program from it.
Suppose now that we do NOT impose this restriction. Now consider the
program:
(define a (mutable 1))
(define (example x)
(set! a x)
x)
(define something (example 5))
(define b (+ a 3))
One can see that as this example generalizes we will rapidly become
unable to determine the initial value of 'b' at compile time, and that
the boundary between compile time execution and run time execution
becomes rather hopelessly blurred. Dealing with the pragmatic
implementation of this is not such a big deal. Dealing with the verifier
implications worries me. Read on.
So now let's go back to the notion of defining the program's initial
state. Defining the *type* of this state works just like before.
However, if we want to reason inductively about how the program state
evolves we are going to need some *instance* of this type that
corresponds to the initial program state. The difficulty is that we
cannot instantiate this instance, because there is no way to specify an
initially unknown value for the global identifier b. This is a real
nuisance, because now we are going to have to define a progressive
series of types of states, in each of which a new value gets defined.
Okay, we could do that, but then we might easily end up in a situation
where either (a) there is no single "type" for "state" that can be used
in EVAL in the prover, or (b) the prover definition of "state" is
implemented as a map from strings to values, and it becomes possible to
attempt an EVAL on a procedure passing a state that is unsufficiently
defined for that procedure to run.
All of this suggests to me that we would like to make sure that all
globals are initialized at compile time. If so, I think we should
restrict the defining expressions to the functional subset of BitC.
Discussion?
shap
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
