Re: Ada Interfaces and the Liskov Substitution Principle

["Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>]

On Tue, 29 May 2007 15:33:54 +0200, Georg Bauhaus wrote:

> On Tue, 2007-05-29 at 14:05 +0200, Dmitry A. Kazakov wrote:
> 
>>>   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.

Any mathematical model is still an approximation. The reason why
mathematics is better here than ad-hocery of outsourced programmers, is
that the mathematical "hardware" is far more powerful than one of Intel.
Hence there is a far less constraints imposed upon you when you model it
mathematically. So even if you had a very good mathematical model it might
be quite difficult to implement it on the machine hardware. This is all
programming is about - porting mathematics. (:-)) To model the reality in
just one hop might be just impossible for a normal programmer. You cannot
rely on Nobel Price laureates, they are rare, expensive and uninterested in
our problems.

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

How can you know that? (:-)) Let's take the braking control system for your
next car...

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

Ordered set, mathematical induction etc.

> and how does it help?

A lot. For example it can tell the code reviewer that the above program is
equivalent to:

    if k < 100 then
      k := 100;
   end if;

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de