[bitc-dev] Type Classes: Pragmatics Questions

Jonathan S. Shapiro shap at eros-os.org
Wed Jul 20 21:41:30 EDT 2005


On Wed, 2005-07-20 at 12:43 -0700, C Y wrote:

> Would it be OK for me to ask a REALLY dumb question here?  Assuming no
> program really stands alone (it at least takes input in and/or outputs
> something, in some form or fashion) what is the theoretical difference
> between a large number of small programs and one large program doing
> the job of all of the smaller ones?  Inter-relatedness between the
> various functionalities?  Or by "whole program analysis" do you mean
> the entire microkernel?...

Generally, the term "whole program analysis" means "everything that will
get linked together, after which no further stuff will get linked in."
The idea is that if you can get a global view of the program, you can do
cross-file analysis that you cannot do on a file by file basis.

The answer to the question that I *think* you are asking is:

When two programs interact at a program boundary, they do so over an
explicit interface with a fully stated and concretized type at the
interface.

E.g. UNIX programs interacting over pipes use an interface that may be
described as "read from fd returning string" and "write string to fd".

Because the interface type is fully stated and fully concrete, no
further type analysis across the programs can be helpful.

>   I've always had the impression the complexity
> of one program or a set of small programs doing the same job as the
> large one is a function of the fundamenal algorithmic logic needed to
> express the task to be done, rather than how it is implimented in
> detail.  Is this not the case?  If you produce code from a proof that
> has proved properties, can you not build on those properties in futher
> proofs, regardless of whether that code is for one program or a small
> part of one?

This is an independent question, and it isn't that simple. The problem
is that the prover has to inductively explore the entire state space of
the entire program, and the search is multiply exponential in the size
of the state space and the complexity of the program.

What you suggest *is* true in certain kinds of restricted programs. In
particular, many proof systems have exploited this approach for purely
functional, known-terminating programs. Such programs can be verified
using term rewriting and do not generally require a state space
analysis.

Further, many *stateful* programs can be converted into this class of
program through monadic transforms.

Note, however, that the "proven to terminate" qualifier is significant,
and that this sharply restricts the space of programs that can be
handled with this technique. Also, the monadic state transform can make
human understanding of the proof process much harder.


shap



More information about the bitc-dev mailing list