Groups | Search | Server Info | Keyboard shortcuts | Login | Register [http] [https] [nntp] [nntps]

Groups > comp.programming > #696

Re: A question about thinking 'abstractly'....

Show all headers | View raw

In article <j092hi$iaf$1@dont-email.me>, BartC <bc@freeuk.com> wrote:
> "Rui Maciel" <rui.maciel@gmail.com> wrote in message 
> news:4e279ec1$0$31827$a729d347@news.telepac.pt...
> 
> 
> > So, to sum things up, programming is in fact applied math and therefore a
> > programmer needs to employ mathematical reasoning to develop software. 
> > Yet,
> > as no one bothers to prove their code to be correct, either by 
> > incompetence
> > or by simply not being able to afford it, the "correctness" aspect of
> > mathematical reasoning isn't really valued by a programmer, which 
> > represents
> > a chasm between programming practices and how a mathematician is expected 
> > to
> > tackle problems. And this means that the thought processes may be seen as
> > very similar, but the details in which programming has been drifting away
> > from the correctness aspect of math have since made them considerably
> > different.
> 
> Programming is lot more complicated than any mathematical formula I've ever 
> seen (for example in having a very large number of possible inputs and 
> expected outputs).
> 
> And to prove correctness, don't you need some sort of specification? 

Yes, correctness has to be with regard to some specification -- I'm not
sure how it could be meaningful otherwise.  (?)

> (Because if you try and prove two different programs, A and B, which both 
> happen to be correct, and accidentally get them mixed up, both will pass. 
> Until you try and use B instead of A!)

I have no idea what you're saying here -- ?  unless it's to make the
same point I made above?

> In that case, we're back to square one with the specification, which 
> presumably is itself some sort of program...

Or some sort of statement about the state of the system after
execution of the code.  It seems to be surprisingly difficult to
write good complete specifications, if "good" means "captures 
the intended/desired behavior".

A quickly-written specification for a square-root function, in no
particular recognized style:

====

For x >= 0, the return value of sqrt(x) is a number y such that 
y >= 0 and abs(y*y - x) <= $THRESHOLD_VALUE.

====

So, more a mathematical expression than a program, no?

But really I'm responding here so I can mention a favorite example
from a long-ago course .... :

Even for simple problems that are apparently well-understood,
writing "good" (in the sense of complete) specifications can be
more difficult than one might think.  Here's an attempt to write
one for a sort functions:

====

If A references an array of size at least n, after execution of
sort(A, n), A[i-1] <= A[i] for all i in the range 1 <= i <= n-1.

====

Seems okay, right?  but I can write a function that meets this
spec and has O(n) execution time.  Spoiler space ....

..

..

..

..

..

..

..

..

..

..

Set all the elements to zero.

Of course that's not exactly what we usually mean by "sort", 
but ....  :-)?

-- 
B. L. Massingill
ObDisclaimer:  I don't speak for my employers; they return the favor.

Back to comp.programming | Previous | Next — Previous in thread | Next in thread | Find similar | Unroll thread

Thread

A question about thinking 'abstractly'.... Chad <cdalten@gmail.com> - 2011-07-19 12:20 -0700
  Re: A question about thinking 'abstractly'.... Ben Bacarisse <ben.usenet@bsb.me.uk> - 2011-07-19 21:26 +0100
  Re: A question about thinking 'abstractly'.... "Kleuskes & Moos" <kleuske@xs4all.nl> - 2011-07-19 14:02 -0700
  Re: A question about thinking 'abstractly'.... Ulisses Araujo Costa <ulissesmonhecosta@gmail.com> - 2011-07-20 02:23 -0700
    Re: A question about thinking 'abstractly'.... "Kleuskes & Moos" <kleuske@xs4all.nl> - 2011-07-20 03:46 -0700
      Re: A question about thinking 'abstractly'.... Ulisses Araújo Costa <ulissesmonhecosta@gmail.com> - 2011-07-20 09:50 -0700
  Re: A question about thinking 'abstractly'.... Rui Maciel <rui.maciel@gmail.com> - 2011-07-21 04:27 +0100
    Re: A question about thinking 'abstractly'.... "BartC" <bc@freeuk.com> - 2011-07-21 12:27 +0100
      Re: A question about thinking 'abstractly'.... blmblm@myrealbox.com <blmblm.myrealbox@gmail.com> - 2011-07-23 17:47 +0000
        Re: A question about thinking 'abstractly'.... "io_x" <a@b.c.invalid> - 2011-07-23 22:16 +0200
          Re: A question about thinking 'abstractly'.... blmblm@myrealbox.com <blmblm.myrealbox@gmail.com> - 2011-07-25 19:39 +0000
    Re: A question about thinking 'abstractly'.... Nick Keighley <nick_keighley_nospam@hotmail.com> - 2011-07-21 05:11 -0700
    Re: A question about thinking 'abstractly'.... August Karlstrom <fusionfile@gmail.com> - 2011-07-21 15:14 +0200
    Re: A question about thinking 'abstractly'.... Nick Keighley <nick_keighley_nospam@hotmail.com> - 2011-07-22 03:50 -0700
    Re: A question about thinking 'abstractly'.... Nick Keighley <nick_keighley_nospam@hotmail.com> - 2011-07-23 06:33 -0700
    Re: A question about thinking 'abstractly'.... Nick Keighley <nick_keighley_nospam@hotmail.com> - 2011-07-25 03:41 -0700
    Re: A question about thinking 'abstractly'.... Nick Keighley <nick_keighley_nospam@hotmail.com> - 2011-07-25 06:06 -0700
  Re: A question about thinking 'abstractly'.... Nick Keighley <nick_keighley_nospam@hotmail.com> - 2011-07-25 03:42 -0700
    Re: A question about thinking 'abstractly'.... Nick Keighley <nick_keighley_nospam@hotmail.com> - 2011-07-25 06:07 -0700
      Re: A question about thinking 'abstractly'.... Nick Keighley <nick_keighley_nospam@hotmail.com> - 2011-08-10 03:57 -0700

csiph-web