[bitc-dev] Type Classes: Pragmatics Questions

[C Y]

Mark P Jones wrote:
>  - specialization is a whole program analysis, which means that the
>    technique might have problems scaling to deal with large systems.
>    (This doesn't rule out separate compilation, but it does mean that
>    you are going to have to rely on some fairly smart linker/whole
>    program optimizer ...)  Fortunately for us, our interest is in
>    compiling a *micro*kernel ... with any luck, our programs won't
>    be too big (assurance would become a problem too in that case)
>    and whole program analysis should still be a viable option...

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?  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?

I always thought a proof based system would consist of a vast multitude
of small parts, each of which has verified properties, and larger parts
built from proofs depending on the prover properties of the small bits.
 In a sense, a system entirely without redundant code or libraries.  Is
this not workable?

Cheers, and apologies for the beginner questions. 

CY

__________________________________________________
Do You Yahoo!?
Tired of spam?  Yahoo! Mail has the best spam protection around 
http://mail.yahoo.com