Re: Ada Interfaces and the Liskov Substitution Principle

[Georg Bauhaus <rm.tsoh+bauhaus@maps.futureapps.de>]

On Tue, 2007-05-29 at 14:05 +0200, Dmitry A. Kazakov wrote:

> > The idealized difference between programming oriented (model) research
> > and researching formal properties of models is that, in the first case,
> > you do not start from models only and then find different models,
> > refine existing models etc.. You start in the programming shop, so to
> > speak.
> 
> But an application program is always a model of some physical reality.

Yes. I just think that programs should be written with (a model
of) physical reality in mind, but employ Off-the-Shelf standard
models only if applicable.

> >   In fact, this is happening. For example, timing properties of
> > co-operating procedures are captured in mathematical models. This is
> > different from the ubiquitously alleged mathematicality of programming:
> > that programs model mathematical functions. Some programs do, but is this
> > all that matters?
> 
> Yes, because application programming deals with mathematical models of the
> reality. I doubt you could skip this abstraction layer.

Programming deals with models of reality and, empirically, most of the
time these models have properties that can be described using
mathematics. Which is a good thing.
However, asking for *mathematical* models of reality is asking for
a clean room definition of the physical model in terms of mathematics.
Many programs just happen to be a model of reality, and they still
work well, even though they were not mathematically designed.
The programmers are hardly aware of every conceivable mathematical
property of their model. Still, they write sound programs.
Can mathematics capture this process?

Next, how much detail can you reasonably place in a formal
specification of a model? Programming in UML seems to be over the
top, IMHO, whereas modeling in UML using a reasonably small set
of L isn't, of course.

> > Shouldn't the relation between programs and mathematical
> > functions be reversed? Wait, it is!
> 
> You can consider mathematics or parts of as programming on some "axiomatic
> hardware".

What I want is the mathematics of program models, more than programming
to satisfy mathematics. BTW, what is the best suited mathematical
structure that (minimally) describes the loop

   while k < 100 loop
     k := Integer'succ(k);
   end loop;

and how does it help?