[Novalug] OT question about a mathematician's proof of a program

Clif Flynt CLIF@CFLYNT.COM
Sat Nov 16 15:05:27 EST 2013


On Sat, Nov 16, 2013 at 02:09:39AM -0500, cmhowe@patriot.net wrote:
> List,
> 
> I'm a bit disappointed in the responses to the question. It was serious.
> ...

  My apology for not answering sooner - been that sort of a week.
  
  Caveat: I've not dealt with the mathematics of programming recently.
(As opposed to the programming of mathematic stuff.)

  My memory is that you can do a rigorous math proof of simple
algorithms to prove that if the inputs are XYZ the output will be ABC. 
My memory is that Knuth talks about this in the first of his "Art of
Programming" series.

  The math getting nasty has a steeper slope than algorithm getting
more complex.  You reach a point where you can't do a solid math
proof before you get to an useful level of algorithmic complexity.

  Once you go from the algorithm to the code, life gets trickier,
since what you code, and what an optimizing compiler creates is not
necessarily the same:

  i=1;
  printf("%d\n", i+1);
  
  may get converted to
  printf("2\n");
  
  When you start actually running the code, life get even more
complex, since most machines nowadays are multi-thread and multi-process,
your task could get interrupted at various points and other things 
could happen.

  If you've got two tasks running in the background on your linux box,
the results of one task doing

  printf("2\n");

  And the other doing 
  printf("I've got 1\n");

  Could generate output on your screen like
  "I've got 12\n\n"
  
  (This is particular failure is very unlikely, and probably can't happen
unless something in a driver or memory buffer is busted.)

  As was mentioned, when you get to security, it's another whole
can of worms added to the other complications.  Now you're talking about
multiple sets of non-deterministic sets of code and networks interacting.

  In the 1970's, computers were considered deterministic.  If you put in
XYZ, you got out ABC.

  By the 1980s, they were starting to be considered as chaotic systems.

  UDP packets are not guaranteed to be delivered.  Bus and network
contention cause semi-random waits for retries can affect timing of
data delivery.  Pipeline behavior and optimizations are not always
intuitively obvious to humans (and maybe not to other computers.)

  It can be mathematically proven that a given algorithm will not
hit a resource lock.  In the real world, you can't be certain that all
the inputs will be received in the order sent, or that decisions will
be implemented the way the algorithm requires.  (Not even counting
stupid coding errors.)

  So, to answer your question, so far as I'm aware, there is no
mathematical proof of correctness for a non-trivial problem.  (Defining
"trivial" as any problem for which a mathemetical solution exists. :-)
)

  Hope this helps,
  Clif
-- 
... Clif Flynt ... http://www.cwflynt.com ... clif@cflynt.com ...
.. Tcl/Tk: A Developer's Guide (3'd edition) - Morgan Kauffman ..
.20'th Annual Tcl/Tk Conference:  Sep 23-27 New Orleans, LA, USA.
.............  http://www.tcl.tk/community/tcl2013/  ............








More information about the Novalug mailing list