Re: Ada Interfaces and the Liskov Substitution Principle

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

On Wed, 2007-05-30 at 09:53 +0200, Dmitry A. Kazakov wrote:

> > OK. So why should a normal programmer like me consider it a cost effective
> > idea to try to construct a proven mathematical model for my daily work?
> 
> Why are you sure that your daily work isn't based on such models? You could
> use them unconsciously.

Hm. If you are suggesting that we have a working model of unconscious
mathematics, then in a sense, empirical programming science would
try to observe its working patterns then.


> The point one is - how would you enjoy the
> "spinal programming" model of things you do care? The second point is - why
> to program anything we don't care?

I'm assuming programmers who work carefully.
Let them be guided by principles. The principles need not
be the best thing since sliced bread only because they have
been described standard math terms.


> >>> 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.
> > 
> > Uhm, can we have less than a group?
> 
> Yes, as you don't mention the operation of.

I mean, what mathematical model (such as LSP) is helpful in describing
this particular loop, such that the math of the model rules out writing
   k := k + 1;
for example? I would start with a model that isn't originally inspired
by mathematics (because higher math typically frowns upon operations,
that is, the things that computers do).
My vague model has loop invariants, loop termination,
and the fact that the type Integer happens to include a successor
function in its interface.  Now, the type Integer offers much
more than that, e.g. "*". Still, it seems reasonable to start from
the mathematical structure that maps to a type like Integer,
even when I do not need either of the inverse,
the neutral element, or commutativity, which Integer types have
(mostly), among other things.


> >>> 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;
> > 
> > Making assumptions about k ... This is how mathematics can make us prefer
> > default perspectives by moving all important points of view behind Formal
> > Mountains. The above change wouldn't have helped at all, on the contrary,
> > 
> >    for k'Address use ...;
> > 
> > What's the mathematics of that, then?
> 
> That k is a pair of functions mapping the system state to the value of k
> and reverse:
> 
>    Get_k : S -> Integer
>    Set_k : S x Integer -> S 

That's not a mathematical model. It is a pair of functions that
can be mapped to some aspects of how k is supposedly operating,
when amended with sequencing. I bet that few programmers writing
the above loop will have functions in mind that map from and to
world state.

> Thank you for making my point! What mathematics makes here is all the rest,
> which could well be incomputable. Consider k a hardware random generator.
> You could not describe it in any programming language, but you can in the
> language of probability theory.

Thank you for making my point! :-) Probability theoretic constructs
can be mapped into executable computer constructs only in very limited
ways, some of them using clever bit shuffling, others relying on
something *outside* the reach of mathematics, such as /dev/random (as
opposed to /dev/urandom). Outside insofar as there is no practical
way of mapping noise to a precise, hence programmable, formula.
This doesn't make them any less useful.