[cap-talk] Re: Question on web calculus - theoretical/practical

David Hopwood david.nospam.hopwood at blueyonder.co.uk
Sun Feb 26 19:31:25 EST 2006

Jed at Webstart wrote:
> At 08:42 AM 2/18/2006, David Hopwood wrote:
>> Jed at Webstart wrote:
>> > On 2/7/06, Olivier Lefevre <lefevrol at yahoo.com> wrote:
>> >
>> >> > > Tyler Close wrote:
>> >> > > I built the Waterken Server toolkit to support developing
>> >> > > capability-based applications. I have built some fairly large,
>> >> > > security sensitive applications with it. [I showed] code
>> >> > > fragments to the audience that proved the software implemented
>> >> > > these guarantees.
>> >> >
>> >> > Still not a _theoretical_ analysis.
>> >>
>> >> Since you did not attend the presentation, your assertion is
>> >> unsupported.
>> >
>> > Hmmm.  Is the above disagreement any more than a terminology issue?
>> > I personally am more concerned with practical analysis than
>> > _theoretical_ analysis.
>> It seems odd to me that anyone would assume /a priori/ that theoretical
>> analysis is not also intended to be practical.
>> "Theoretical" means something like "consistent with, and making use of a
>> well-defined theory". "Practical" means something like "able to be put
>> into practice". Where's the conflict here?
> It seems a common enough connotation to me, e.g. from:
> http://dict.die.net/theoretical/
>      2: concerned with theories rather than their practical
>         applications; "theoretical physics" [ant: applied]
> or from:
> http://www.answers.com/topic/theoretical
>      2.  Restricted to theory; not practical: theoretical physics.
>      3.  Given to theorizing; speculative.
> though I admit that I do think "theoretical physics" is practical and
> is not such a good example.

It's not just that this particular example is a spectacularly bad one [*].
There is an insidious example of the weak Sapir-Whorf hypothesis at work
here: language is affecting the way we think about the relation between
theory and practice, leading to false conclusions and bad policy.

I make a conscious effort not to use the phrase "in theory" when I mean
impractical or purely speculative. I may be swimming against the tide of
common usage here, but I'm going to continue doing so, because it is entirely
counterproductive to disparage the usefulness of theory -- *especially*
as an implicit side effect of the language that we use.

(Another word that has had its meaning similarly distorted is "academic",
but I'll spare you my rant about that.)

[*] Without theoretical physics, we wouldn't have had the industrial
    revolution, or the communication revolution, or computers. Maybe we
    wouldn't have had the Enlightenment, for that matter. Many people are
    alive today only because of medical diagnosis and interventions that
    are dependent on theoretical physics. How much more practical can you
    get? Not that practical utility is the only reason to do science, mind

> In my experience there is often
> a distinction made between theory and practice.

There is a distinction, but there is no conflict.

A theory defines a model, which is intended to partially describe some aspect
of reality or practice.

If we have a case where a given theory does not adequately describe practice,
then there are several possible responses:

1. restrict what is practiced to that which can be modelled with sufficient
   accuracy by currently available theory.
2. extend the theory to accurately model the practice.
3. muddle along with no applicable theory to back up what we are doing.

Either 1 or 2 (or a combination of them) is clearly preferable to 3, although
3 is often what happens.

Incidentally, it seems to me that in computer science we make too little
use of response 1. Many computer systems are unreliable or insecure partly
because they are too ambitious, or are trying to satisfy too many constraints

> For example in
> theory one can use Quantum Mechanics to calculate the orbit[al]s
> of electrons for any atoms.  In practice it's only possible to calculate
> the orbits for the hydrogen atom and to make approximations for the
> helium atom (at least last I checked).

Let's assume this is correct (my knowledge of quantum mechanics is minimal)
and say that you're designing some exotic power reactor in which it is
necessary to have a comprehensive understanding of the orbitals of electrons
in the elements used as fuel. The three kinds of response described above
apply here; you can

 - restrict the design of the reactor (e.g. by using only hydrogen) so
   that your existing theory of electron orbitals is sufficient,
 - extend the theory so that it can calculate the orbitals for the elements
   your reactor will use, or
 - muddle along regardless.

In this case, muddling along would be a particularly bad idea. It's still a
bad idea even if the other responses do not immediately allow you to build
any reactor at all.

> For many years one could say that in theory there should be three times the
> observed flux of neutrinos coming from the Sun to the Earth.

You mean that a *particular* theory predicted three times the flux of neutrinos
coming from the Sun to the Earth than was observed in certain experiments.

In science, theories are first-class entities. There is no single privileged
theory that is universally accepted in a field at any given time. It is an
oversimplication even to say that each scientist supports a single theory at
a time.

> That's a case where they had to change the theory (mass for the neutrino and
> their ability to change types).

Rather, the theory that predicted three times the flux was rejected and a
different theory became better supported by observation, hence more popular.
That's how science works. It could also have been the case that the observations
were inaccurate.

(I remember, even as a small child, being intensely irritated when told the
anecdote that "Scientists Say That Bumble-Bees Can't Fly". It was quite clear
to me that it was the anti-scientific views motivating the popularity of the
anecdote, not any inadequacies of physics or of theory in general, that were
more of a problem. See <http://www.keelynet.com/interact/archive/00001691.htm>
for some discussion of this anecdote, and the mechanisms by which insects
generate vortices to provide additional lift.)

I do not believe that there is any real phenomenon that cannot in principle be
explained by an appropriate theory. That's a stronger position than needed to
support my general argument in this post, but it may help to see where I'm
coming from.

> Even in that call for papers that you just [forwarded] the first sentence
> is: "Computer security is an established field of computer science of both
> theoretical and practical significance." - which would seem to antagonize
> theory and practice.

I don't think that was the writers' intent. AFAICS, they are saying that
computer security is of theoretical significance (i.e. theories of computer
security are needed for a comprehensive understanding of computer science
in general) and that it is of practical significance (i.e. understanding
computer security is necessary for the practical goal of getting computers
to do only what their users want). No antagonism here. On the contrary, the
conference is supposed to be about putting various theories into practice.

> It does seem a bit odd to me that Olivier Lefevre would
> disparage the analysis that Tyler Close described by
> saying that it wasn't a _theoretical_ analysis - apparently suggesting
> as you (David H.) seem to feel that a 'theoretical' analysis is
> based on a known theory and therefore better grounded or more
> sound

I agree with the latter point; I don't agree that the kind of analyses that
Tyler appears to be talking about are not theoretical. Perhaps the issue is
with the degree of formality involved -- i.e. Olivier's argument may be that
these are "only" informal analyses.

Most reasoning used in science, engineering, or even mathematics, is not
completely formal. Strictly formal reasoning by means of axioms and inference
rules with no logical gaps is a rather tedious activity for a human. It is
important, in order to avoid certain kinds of mistake, that formalization is
*possible*, but that doesn't mean that it has to be applied on every occasion
when a theory is used.

I hope and expect that at some point in the near future (< 10 years),
progress in computer-assisted reasoning will make it feasible to produce
strictly formal proofs (that can be checked by very simple theorem checkers)
with a similar investment of effort as is currently the case for semi-formal

In the meantime, much can be achieved without that. A good example is
type-checking: a type system can be at the same time:

 - simple enough to be used by amateur programmers,

 - expressive enough to enforce useful properties of subprograms,

 - automatically checkable, using an algorithm that is straightforward
   enough to be confident in its correctness and efficient enough to be
   used on every compilation.

David Hopwood <david.hopwood at blueyonder.co.uk>

More information about the cap-talk mailing list