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

Groups > comp.programming > #681 > unrolled thread

A question about thinking 'abstractly'....

Back to article view | Back to comp.programming

Contents

  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

#681 — A question about thinking 'abstractly'....

One of my friends who attends Harvard took Math 55. He mentioned that
a lot of it was being able to prove major theorems with only the aid
of the definitions. This got me to thinking.  I've had a lot of people
help with me a programming problem by only providing defintions.

Is the thought process to proving some major theorems in math with
only the aid of the defintions similar to implementing some kind of
data structures when given only the definitions of a data structure?

Chad

[toc] | [next] | [standalone]

#683

Chad <cdalten@gmail.com> writes:

> One of my friends who attends Harvard took Math 55. He mentioned that
> a lot of it was being able to prove major theorems with only the aid
> of the definitions. This got me to thinking.  I've had a lot of people
> help with me a programming problem by only providing defintions.
>
> Is the thought process to proving some major theorems in math with
> only the aid of the defintions similar to implementing some kind of
> data structures when given only the definitions of a data structure?

I can't speak about thought processes, but there is a very deep formal
relationship between types and proofs (an isomorphism, in fact).  Look
up the Curry-Howard correspondence if you want to find out more.

BTW, I can't see any connection to C so I've set followups to
comp.programming.

-- 
Ben.

[toc] | [prev] | [next] | [standalone]

#684

On Jul 19, 9:20 pm, Chad <cdal...@gmail.com> wrote:
> One of my friends who attends Harvard took Math 55. He mentioned that
> a lot of it was being able to prove major theorems with only the aid
> of the definitions. This got me to thinking.  I've had a lot of people
> help with me a programming problem by only providing defintions.
>
> Is the thought process to proving some major theorems in math with
> only the aid of the defintions similar to implementing some kind of
> data structures when given only the definitions of a data structure?

Not sure i understand correctly, but theorem provers have been around
for some time. C is not the most convenient language to implement one,
though.

See http://en.wikipedia.org/wiki/Theorem_prover

[toc] | [prev] | [next] | [standalone]

#685

On 19 Jul, 20:20, Chad <cdal...@gmail.com> wrote:
> One of my friends who attends Harvard took Math 55. He mentioned that
> a lot of it was being able to prove major theorems with only the aid
> of the definitions. This got me to thinking.  I've had a lot of people
> help with me a programming problem by only providing defintions.
>
> Is the thought process to proving some major theorems in math with
> only the aid of the defintions similar to implementing some kind of
> data structures when given only the definitions of a data structure?
>
> Chad

Hello Chad,

Is the process of cocking a recipe with only the use of ingredients
similar to implementing some kind of
data structures when given only the definitions of a data structure?

When you prove something, regardless the mechanism you use, will be
faster if you use some of preexisting definitions, axioms,
theorems,... You can reinvent the well if you want to.

Regards,

Ulisses Araújo Costa - caos.di.uminho.pt/~ulisses

[toc] | [prev] | [next] | [standalone]

#686

On Jul 20, 11:23 am, Ulisses Araujo Costa
<ulissesmonheco...@gmail.com> wrote:
> On 19 Jul, 20:20, Chad <cdal...@gmail.com> wrote:
>
> > One of my friends who attends Harvard took Math 55. He mentioned that
> > a lot of it was being able to prove major theorems with only the aid
> > of the definitions. This got me to thinking.  I've had a lot of people
> > help with me a programming problem by only providing defintions.
>
> > Is the thought process to proving some major theorems in math with
> > only the aid of the defintions similar to implementing some kind of
> > data structures when given only the definitions of a data structure?
>
> > Chad
>
> Hello Chad,
>
> Is the process of cocking a recipe with only the use of ingredients
> similar to implementing some kind of
> data structures when given only the definitions of a data structure?
>
> When you prove something, regardless the mechanism you use, will be
> faster if you use some of preexisting definitions, axioms,
> theorems,... You can reinvent the well if you want to.

Nitpick... A "proof" in mathematics consists of showing that it
follows from axioms and theorems have already been shown to do that.
Otherwise they would not be theorems.

[toc] | [prev] | [next] | [standalone]

#687

On 20 Jul, 11:46, "Kleuskes & Moos" <kleu...@xs4all.nl> wrote:
> On Jul 20, 11:23 am, Ulisses Araujo Costa
>
>
>
>
>
>
>
>
>
> <ulissesmonheco...@gmail.com> wrote:
> > On 19 Jul, 20:20, Chad <cdal...@gmail.com> wrote:
>
> > > One of my friends who attends Harvard took Math 55. He mentioned that
> > > a lot of it was being able to prove major theorems with only the aid
> > > of the definitions. This got me to thinking.  I've had a lot of people
> > > help with me a programming problem by only providing defintions.
>
> > > Is the thought process to proving some major theorems in math with
> > > only the aid of the defintions similar to implementing some kind of
> > > data structures when given only the definitions of a data structure?
>
> > > Chad
>
> > Hello Chad,
>
> > Is the process of cocking a recipe with only the use of ingredients
> > similar to implementing some kind of
> > data structures when given only the definitions of a data structure?
>
> > When you prove something, regardless the mechanism you use, will be
> > faster if you use some of preexisting definitions, axioms,
> > theorems,... You can reinvent the well if you want to.
>
> Nitpick... A "proof" in mathematics consists of showing that it
> follows from axioms and theorems have already been shown to do that.
> Otherwise they would not be theorems.

My mistake, you are right! Theorems are already proved material.

--
Ulisses Araújo Costa - caos.di.uminho.pt/~ulisses

[toc] | [prev] | [next] | [standalone]

#688

Chad wrote:

> One of my friends who attends Harvard took Math 55. He mentioned that
> a lot of it was being able to prove major theorems with only the aid
> of the definitions. This got me to thinking.  I've had a lot of people
> help with me a programming problem by only providing defintions.
> 
> Is the thought process to proving some major theorems in math with
> only the aid of the defintions similar to implementing some kind of
> data structures when given only the definitions of a data structure?

Sometimes it may be overlooked but programming is inherently and 
fundamentally a mathematical endeavour, which basically involves nothing 
else than a set of operators being applied to a set of fields in a specific 
order in order to reach an intended outcome.  Following this interpretation, 
any API is nothing more than a set of definitions of a mix of operators and 
sets which a programmer may apply to his sets of data.  With this in mind, 
the answer to your question would be a clear yes, mathematical reasoning is 
as vital to a mathematician as it is to a programmer.  It is because 
mathematics and programming are the same thing.

But then the real world sets in.

The thing is, mathematicians spend their time and energy studying the 
implications of some set of definitions but they also invest a lot of 
themselves trying to prove that the stuff they come up with is correct.  
This mindset is lost in software development, whose approach to the 
mathematical problem of developing a program often ends with providing code 
which only works as expected in very limited circumstances which no one 
knows or cares to know.  Even those who actually care for this sort of stuff 
and actually know their onions shy away from this goal, a fact which may be 
represented by Knuth's quote "Beware of bugs in the above code; I have only 
proved it correct, not tried it."  

Meanwhile, the programming world occupies itself hacking together sets of 
instructions which no one actually cares they are proven to be correct, or 
even if they are valid in the conceivable scenarios which they are designed 
to operate.  That is, when compared to how a mathematician may tackle a 
problem, programmers don't actually know what they are doing and instead 
embrace the fact that the stuff they create does break and that they can't 
do anything to prevent it.  The disregard for this mathematical correctness 
has reached a level that some programming errors committed by programmers 
are so widespread and so frequent that, instead of trying to make sure that 
the programmer is sufficiently competent to avoid them, they are simply 
embraced as a natural occurrence and technologies have been developed to be 
able to sweep those programming errors under the proverbial rug, which is 
the case of technologies such as garbage collection and sandboxes.

And the thing is, this isn't necessarily bad.  Of course, it would be better 
if every piece of softwar ever written would have been developed with enough 
care to be successfully demonstrated to be correct.  Yet, that would mean 
that an ungodly amount of time and energy (and, of course, money) would be 
spent on developing even the smallest program.  Although it would save a lot 
of time and energy in some areas (for example, the software security 
business, at least as we know it, would have never existed) it would simply 
be too cost-prohibitive and also time-consuming to develop any piece of 
software.

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.


Rui Maciel

[toc] | [prev] | [next] | [standalone]

#690

"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? 
(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!)

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

-- 
Bartc 

[toc] | [prev] | [next] | [standalone]

#696

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.

[toc] | [prev] | [next] | [standalone]

#697

"blmblm@myrealbox.com" <blmblm.myrealbox@gmail.com> ha scritto nel messaggio
news:990fq1F8n9U4@mid.individual.net...
> In article <j092hi$iaf$1@dont-email.me>, BartC <bc@freeuk.com> wrote:
> ====
>
> For x >= 0, the return value of sqrt(x) is a number y such that
> y >= 0 and abs(y*y - x) <= $THRESHOLD_VALUE.
>
> ====
>
> 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.
>
> ====

it is all formal
if you not replace the english words with simbols you not have
a language ok

all is formal i.e. the good way of build right symbols from axioms;
programming langages as math are one game build symbols from axioms
that seems to have no pratical meaning :)
they have their meaning as build of allowed set of symbols
they not need other; in pratice we build one home 10000000000000000
can be build

registers are real points that contain 32 bits unsigned numbers
a,b,c,r, etc .
One can sign them in a real[R] X axist

memory is a array of points in the y axist
address 0..maxIndxMemory

than there is the time[here] that is represented from
the formal way to met first instruction symbols

than there are operations of the set of registers
+:R32bit x R32bits -> R32Bit
etc
code could be as a theorem
theorem
a=0|b=0|c=3|r=c+b => r=3

it is like in a debug window we see a=0|b=0|c=3|r=c+b
than in the debug window we see r==3 is true

math can have goto for explain algo one meet in math too

   c=a+b|if c==3 goto v|c=9
v:

where is the difference?

the difference is only with algo we not are sure 100%
of the result even if we debug the code...
because algo seem to be a little difficult

but algo are in math

with the teorems all seem easier if read the math book
and understand it

at last i think that until now

[toc] | [prev] | [next] | [standalone]

#709

In article <4e2b2ba0$0$44211$4fafbaef@reader1.news.tin.it>,
io_x <a@b.c.invalid> wrote:
> 
> "blmblm@myrealbox.com" <blmblm.myrealbox@gmail.com> ha scritto nel messaggio
> news:990fq1F8n9U4@mid.individual.net...
> > In article <j092hi$iaf$1@dont-email.me>, BartC <bc@freeuk.com> wrote:
> > ====
> >
> > For x >= 0, the return value of sqrt(x) is a number y such that
> > y >= 0 and abs(y*y - x) <= $THRESHOLD_VALUE.
> >
> > ====
> >
> > 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.
> >
> > ====
> 
> it is all formal
> if you not replace the english words with simbols you not have
> a language ok

I have no idea what you mean here, sorry.  No offense meant [*], but
I often have trouble with your attempts at English.  Maybe someone
else can translate.  Or not.

[*] Since I'm unfortunately one of those native speakers who can't
claim fluency in any other language.  "Some knowledge" yes, but
fluency no.  So I'm not in a position to be critical.

I'm not doing much better with the text below but will attempt
a few comments:

> all is formal i.e. the good way of build right symbols from axioms;
> programming langages as math are one game build symbols from axioms
> that seems to have no pratical meaning :)
> they have their meaning as build of allowed set of symbols
> they not need other; in pratice we build one home 10000000000000000
> can be build
> 
> registers are real points that contain 32 bits unsigned numbers
> a,b,c,r, etc .
> One can sign them in a real[R] X axist

I'm not sure how well it works to think of register contents as
real numbers, given that the reals are uncountable and the set
of possible values for something with a finite number of bits is
not.  But maybe that's not what you meant anyway?

I wonder, though, whether you're describing some sort of variant
on a Turing machine??

> memory is a array of points in the y axist
> address 0..maxIndxMemory
> 
> than there is the time[here] that is represented from
> the formal way to met first instruction symbols
> 
> than there are operations of the set of registers
> +:R32bit x R32bits -> R32Bit
> etc
> code could be as a theorem
> theorem
> a=0|b=0|c=3|r=c+b => r=3
> 
> it is like in a debug window we see a=0|b=0|c=3|r=c+b
> than in the debug window we see r==3 is true
> 
> math can have goto for explain algo one meet in math too
> 
>    c=a+b|if c==3 goto v|c=9
> v:
> 
> where is the difference?
> 
> the difference is only with algo we not are sure 100%
> of the result even if we debug the code...

Another important difference might be that sometimes one can
formally prove the correctness of an algorithm, but in a way
that ignores some implementation issues such as the finiteness
of most computer representations of numbers.  (The example that
comes to mind involves binary search and how finding the middle
of the index range i1 .. i2 by computing (i1+i2)/2 fails if
the addition produces overflow.)

> because algo seem to be a little difficult
> 
> but algo are in math
> 
> with the teorems all seem easier if read the math book
> and understand it
> 
> at last i think that until now

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

[toc] | [prev] | [next] | [standalone]

#692

On Jul 21, 4:27 am, Rui Maciel <rui.mac...@gmail.com> wrote:


<snip>

> Sometimes it may be overlooked but programming is inherently and
> fundamentally a mathematical endeavour,

well, "Up to a point, Lord Copper"

you might as well say civil engineering is applied mathematics.

[OTH I nearly failed a job interview by saying something along your
lines]


> which basically involves nothing
> else than a set of operators being applied to a set of fields in a specific
> order in order to reach an intended outcome.  

real programmers have to worry about the resources consumed as well


> Following this interpretation,
> any API is nothing more than a set of definitions of a mix of operators and
> sets which a programmer may apply to his sets of data.  With this in mind,
> the answer to your question would be a clear yes, mathematical reasoning is
> as vital to a mathematician as it is to a programmer.  

I've been a fan of proofs of correctness (though this says little as I
don't actually prove programs). Jon Bentley's Progamming Pearls give
an interesting take on this. Even *thinking* about how you would
"informally"[*] prove the program (well function anyway) helps towards
correctness. What are valid arguments (pre-conditions) what is this
loop doing (loop invarient) and when does it stop (termination
condition), and what should the output be (post-condition). A program
is a contract it guarantees certain outputs if-and-only-if certain
guarantees about the input are met.

[*] being a little bit informal is like being a little bit pregnant.
You are either formal or you aren't.

> It is because
> mathematics and programming are the same thing.

bending the definition of programming to near breasking point.


> But then the real world sets in.

it has that nasty habbit.


> The thing is, mathematicians spend their time and energy studying the
> implications of some set of definitions but they also invest a lot of
> themselves trying to prove that the stuff they come up with is correct.  

what mathematicians are trying to do is fundamentally different from
what programmers are trying to do. Mathematicainas are trying to prove
theorums (or conjectures) within some mathematical framework.
Programmers are trying to produce things that do stuff *within highly
constrained tiem frames and resource availability*.

Back to the civil engineers. If they were unconstrained on time scales
and on material usage then building bridges would be easy. "oh bugger
it, just use another 100 tons of steel".


> This mindset is lost in software development, whose approach to the
> mathematical problem of developing a program often ends with providing code
> which only works as expected in very limited circumstances which no one
> knows or cares to know.  Even those who actually care for this sort of
> stuff
> and actually know their onions shy away from this goal, a fact which may be
> represented by Knuth's quote "Beware of bugs in the above code; I have only
> proved it correct, not tried it."  
>
> Meanwhile, the programming world occupies itself hacking together sets of
> instructions which no one actually cares they are proven to be correct, or
> even if they are valid in the conceivable scenarios which they are designed
> to operate.

I think lots of people care. I think we do an adequate job more often
than is appreciated. That plane that landed on the Hudson river came
down in one piece at least partly because some software did the Right
Thing under some very "but that would never happen!" scenario.


> That is, when compared to how a mathematician may tackle a
> problem, programmers don't actually know what they are doing and instead
> embrace the fact that the stuff they create does break and that they can't
> do anything to prevent it.  The disregard for this mathematical correctness
> has reached a level that some programming errors committed by programmers
> are so widespread and so frequent that, instead of trying to make sure that
> the programmer is sufficiently competent to avoid them, they are simply
> embraced as a natural occurrence and technologies have been developed to be
> able to sweep those programming errors under the proverbial rug, which is
> the case of technologies such as garbage collection and sandboxes.

garbage collectors are there for other reasons as well. I think
sandboxes are as well. Not everyone who wants to run programs on your
computer has your best interests in mind.


> And the thing is, this isn't necessarily bad.  Of course, it would be better
> if every piece of softwar ever written would have been developed with enough
> care to be successfully demonstrated to be correct.

I too have this dream.



> Yet, that would mean
> that an ungodly amount of time and energy (and, of course, money) would be
> spent on developing even the smallest program.

I'm not sure it would be as expensive as people sometimes think.


> Although it would save a lot
> of time and energy in some areas (for example, the software security
> business, at least as we know it, would have never existed)

but something like it /would/. Security is a Hard Problem. Proving
something is secure is damn nearly a halting problem.


> it would simply
> be too cost-prohibitive and also time-consuming to develop any piece of
> software.
>
> So, to sum things up, programming is in fact applied math and therefore a
> programmer needs to employ mathematical reasoning to develop software.

I submit that unit testing when properly done is close to automated
correctness proving.    :-)



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

I don't think it drifted. I think it hoist the mainsail and turned
down wind.

The goals are fundamentally different. Yes I think more DbC and so on
would be a damn good idea. I think the educational system could be
improved too. Maybe the people and really critical systems should be
certified.


--
Nick Keighley

[toc] | [prev] | [next] | [standalone]

#693

On 2011-07-21 05:27, Rui Maciel wrote:
> The disregard for this mathematical correctness
> has reached a level that some programming errors committed by programmers
> are so widespread and so frequent that, instead of trying to make sure that
> the programmer is sufficiently competent to avoid them, they are simply
> embraced as a natural occurrence and technologies have been developed to be
> able to sweep those programming errors under the proverbial rug, which is
> the case of technologies such as garbage collection and sandboxes.

...as well as e.g. run-time checks of array bounds and null pointers and 
maybe the whole concept of type safety. If the program is correct we 
don't need these. But as we all know even the best programmers make 
mistakes. It is therefor an important aspect of the programming language 
and environment to fail fast in case of programming errors related to 
invalid use of memory (and not produce garbage results) and to aid in 
locating these errors.

August

-- 
The competent programmer is fully aware of the limited size of his own 
skull. He therefore approaches his task with full humility, and avoids 
clever tricks like the plague. --Edsger Dijkstra

[toc] | [prev] | [next] | [standalone]

#694

On Jul 21, 4:27 am, Rui Maciel <rui.mac...@gmail.com> wrote:
> Chad wrote:


> > One of my friends who attends Harvard took Math 55. He mentioned that
> > a lot of it was being able to prove major theorems with only the aid
> > of the definitions. This got me to thinking.  I've had a lot of people
> > help with me a programming problem by only providing defintions.
>
> > Is the thought process to proving some major theorems in math with
> > only the aid of the defintions similar to implementing some kind of
> > data structures when given only the definitions of a data structure?

I'm not sure this is well formed sentence.


> Sometimes it may be overlooked but programming is inherently and
> fundamentally a mathematical endeavour,

"up to a point Lord Copper"


> [...] which basically involves nothing
> else than a set of operators being applied to a set of fields in a specific
> order in order to reach an intended outcome.  Following this interpretation,
> any API is nothing more than a set of definitions of a mix of operators and
> sets which a programmer may apply to his sets of data.  With this in mind,
> the answer to your question would be a clear yes, mathematical reasoning is
> as vital to a mathematician as it is to a programmer.  It is because
> mathematics and programming are the same thing.

in a sense Civil engineering is just applied maths.

Mathematics and programming are /not/ the same thing. Mathematics is a
useful
tool for the programmer but they are not the same thing.


> But then the real world sets in.

it has that nasty habbit


> The thing is, mathematicians spend their time and energy studying the
> implications of some set of definitions but they also invest a lot of
> themselves trying to prove that the stuff they come up with is correct.
> This mindset is lost in software development, whose approach to the
> mathematical problem of developing a program often ends with providing code
> which only works as expected in very limited circumstances which no one
> knows or cares to know.  Even those who actually care for this sort of stuff
> and actually know their onions shy away from this goal, a fact which may be
> represented by Knuth's quote "Beware of bugs in the above code; I have only
> proved it correct, not tried it."

mathematicians and programmers do not have the same goals.  The
programmer's
aim is to produce things that do useful stuff whilst staying within
resource
constraints (development time/money, run time/memory/money).

Even proven programs have to be tested. Our compilers aren't proven
and nor are
our libraries. And they don't do proofs of correctness on the hardware
(not since
Viper anyway).


> Meanwhile, the programming world occupies itself hacking together sets of
> instructions which no one actually cares they are proven to be correct, or
> even if they are valid in the conceivable scenarios which they are designed
> to operate.  That is, when compared to how a mathematician may tackle a
> problem, programmers don't actually know what they are doing and instead
> embrace the fact that the stuff they create does break and that they can't
> do anything to prevent it.  The disregard for this mathematical correctness
> has reached a level that some programming errors committed by programmers
> are so widespread and so frequent that, instead of trying to make sure that
> the programmer is sufficiently competent to avoid them, they are simply
> embraced as a natural occurrence and technologies have been developed to be
> able to sweep those programming errors under the proverbial rug, which is
> the case of technologies such as garbage collection and sandboxes.

both garbage collection and sandboxes have other reasons to exist.

garbage collectors arose out of languages (Lisp) that probably had a
more sound
mathematical basis than the vast majority of languages. They were also
invented
in the programming paleolithic, when resource constraints were
*really* resource
constraints. It is a perfectly sound design choice to automate things.
Does your
car have a starting handle?

sandboxes are also needed because not everyone who wants to run
programs on
your computer has your best interests at heart.


> And the thing is, this isn't necessarily bad.  Of course, it would be better
> if every piece of softwar[e] ever written would have been developed with enough
> care to be successfully demonstrated to be correct.  Yet, that would mean
> that an ungodly amount of time and energy (and, of course, money) would be
> spent on developing even the smallest program.

unit test when properly done could be thought of as an automated proof
system

> Although it would save a lot
> of time and energy in some areas (for example, the software security
> business, at least as we know it, would have never existed)

but something would. Security is a Hard Problem. Some parts of it hit
Halting
Problem difficulties. Addmittedly virus checkers seem like a
fundamentally a
broken solution.


> it would simply
> be too cost-prohibitive and also time-consuming to develop any piece of
> software.

yes!


> So, to sum things up, programming is in fact applied math and therefore a
> programmer needs to employ mathematical reasoning to develop software.

no. But it wouldn't hurt if programmers thought like this more.
Bentley's Programming Pearls is worth a read.


>  Yet,
> as no one bothers to prove their code to be correct, either by incompetence
> or by simply not being able to afford it,

or ignorance. I suspect most programmers would not have a clue where
to start.
Or express surprise that such a thing was even conceivable!


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

not drifted, more like hoist the mainsail and pointed down wind.

Although I seem to be disagreeing- well actually I /am/ disagreeing.
Programming
is /not/ mathematics and nor should it be. OTOH I agree more formality
probably
wouldn't do any harm.

We /should/ wonder if our loops will terminate and under what
conditions our program
should be expected to work.

Each "module" (line, function, package, program...) should have a pre-
condition (what
it expects to be true before it executes), a post-condition (what will
be true when it
terminates, if its pre-condition was met) and some guarantee it will
terminate.
Even thinking about these things helps.

OO programmers should think about class invarients.

Whilst full blown proofs are too expensive in most environments.
There's DbC and even
the humble assert. Lots of unit tests.

Mathematicians may laugh being a little bit informal is like being
little bit pregnant.
But *my* machine doesn't come with an infinite tape!

[toc] | [prev] | [next] | [standalone]

#695

On Jul 21, 4:27 am, Rui Maciel <rui.mac...@gmail.com> wrote:
> Chad wrote:

> > One of my friends who attends Harvard took Math 55. He mentioned that
> > a lot of it was being able to prove major theorems with only the aid
> > of the definitions. This got me to thinking.  I've had a lot of people
> > help with me a programming problem by only providing defintions.
>
> > Is the thought process to proving some major theorems in math with
> > only the aid of the defintions similar to implementing some kind of
> > data structures when given only the definitions of a data structure?

I'm not sure this is well formed sentence.


> Sometimes it may be overlooked but programming is inherently and
> fundamentally a mathematical endeavour,

"up to a point Lord Copper"


> [...] which basically involves nothing
> else than a set of operators being applied to a set of fields in a specific
> order in order to reach an intended outcome.  Following this interpretation,
> any API is nothing more than a set of definitions of a mix of operators and
> sets which a programmer may apply to his sets of data.  With this in mind,
> the answer to your question would be a clear yes, mathematical reasoning is
> as vital to a mathematician as it is to a programmer.  It is because
> mathematics and programming are the same thing.

in a sense Civil engineering is just applied maths.

Mathematics and programming are /not/ the same thing. Mathematics is a
useful
tool for the programmer but they are not the same thing.


> But then the real world sets in.

it has that nasty habbit

> The thing is, mathematicians spend their time and energy studying the
> implications of some set of definitions but they also invest a lot of
> themselves trying to prove that the stuff they come up with is correct.
> This mindset is lost in software development, whose approach to the
> mathematical problem of developing a program often ends with providing code
> which only works as expected in very limited circumstances which no one
> knows or cares to know.  Even those who actually care for this sort of stuff
> and actually know their onions shy away from this goal, a fact which may be
> represented by Knuth's quote "Beware of bugs in the above code; I have only
> proved it correct, not tried it."

mathematicians and programmers do not have the same goals.  The
programmer's
aim is to produce things that do useful stuff whilst staying within
resource
constraints (development time/money, run time/memory/money).

Even proven programs have to be tested. Our compilers aren't proven
and nor are
our libraries. And they don't do proofs of correctness on the hardware
(not since
Viper anyway).


> Meanwhile, the programming world occupies itself hacking together sets of
> instructions which no one actually cares they are proven to be correct, or
> even if they are valid in the conceivable scenarios which they are designed
> to operate.  That is, when compared to how a mathematician may tackle a
> problem, programmers don't actually know what they are doing and instead
> embrace the fact that the stuff they create does break and that they can't
> do anything to prevent it.  The disregard for this mathematical correctness
> has reached a level that some programming errors committed by programmers
> are so widespread and so frequent that, instead of trying to make sure that
> the programmer is sufficiently competent to avoid them, they are simply
> embraced as a natural occurrence and technologies have been developed to be
> able to sweep those programming errors under the proverbial rug, which is
> the case of technologies such as garbage collection and sandboxes.

both garbage collection and sandboxes have other reasons to exist.

garbage collectors arose out of languages (Lisp) that probably had a
more sound
mathematical basis than the vast majority of languages. They were also
invented
in the programming paleolithic, when resource constraints were
*really* resource
constraints. It is a perfectly sound design choice to automate things.
Does your
car have a starting handle?

sandboxes are also needed because not everyone who wants to run
programs on
your computer has your best interests at heart.


> And the thing is, this isn't necessarily bad.  Of course, it would be better
> if every piece of softwar[e] ever written would have been developed with enough
> care to be successfully demonstrated to be correct.  Yet, that would mean
> that an ungodly amount of time and energy (and, of course, money) would be
> spent on developing even the smallest program.

unit test when properly done could be thought of as an automated proof
system


> Although it would save a lot
> of time and energy in some areas (for example, the software security
> business, at least as we know it, would have never existed)

but something would. Security is a Hard Problem. Some parts of it hit
Halting
Problem difficulties. Addmittedly virus checkers seem like a
fundamentally a
broken solution.


> it would simply
> be too cost-prohibitive and also time-consuming to develop any piece of
> software.

yes!


> So, to sum things up, programming is in fact applied math and therefore a
> programmer needs to employ mathematical reasoning to develop software.

no. But it wouldn't hurt if programmers thought like this more.
Bentley's Programming Pearls is worth a read.


>  Yet,
> as no one bothers to prove their code to be correct, either by incompetence
> or by simply not being able to afford it,

or ignorance. I suspect most programmers would not have a clue where
to start.
Or express surprise that such a thing was even conceivable!


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

not drifted, more like hoist the mainsail and pointed down wind.

Although I seem to be disagreeing- well actually I /am/ disagreeing.
Programming
is /not/ mathematics and nor should it be. OTOH I agree more formality
probably
wouldn't do any harm.

We /should/ wonder if our loops will terminate and under what
conditions our program
should be expected to work.

Each "module" (line, function, package, program...) should have a pre-
condition (what
it expects to be true before it executes), a post-condition (what will
be true when it
terminates, if its pre-condition was met) and some guarantee it will
terminate.
Even thinking about these things helps.

OO programmers should think about class invarients.

Whilst full blown proofs are too expensive in most environments.
There's DbC and even
the humble assert. Lots of unit tests.

Mathematicians may laugh- being a little bit informal is like being a
little bit pregnant.
But *my* machine doesn't come with an infinite tape!

[toc] | [prev] | [next] | [standalone]

#702

On Jul 21, 4:27 am, Rui Maciel <rui.mac...@gmail.com> wrote:
> Chad wrote:


> > One of my friends who attends Harvard took Math 55. He mentioned that
> > a lot of it was being able to prove major theorems with only the aid
> > of the definitions. This got me to thinking.  I've had a lot of people
> > help with me a programming problem by only providing defintions.
>
> > Is the thought process to proving some major theorems in math with
> > only the aid of the defintions similar to implementing some kind of
> > data structures when given only the definitions of a data structure?

I'm not sure this is well formed sentence.


> Sometimes it may be overlooked but programming is inherently and
> fundamentally a mathematical endeavour,

"up to a point Lord Copper"


> [...] which basically involves nothing
> else than a set of operators being applied to a set of fields in a specific
> order in order to reach an intended outcome.  Following this interpretation,
> any API is nothing more than a set of definitions of a mix of operators and
> sets which a programmer may apply to his sets of data.  With this in mind,
> the answer to your question would be a clear yes, mathematical reasoning is
> as vital to a mathematician as it is to a programmer.  It is because
> mathematics and programming are the same thing.

in a sense Civil engineering is just applied maths.

Mathematics and programming are /not/ the same thing. Mathematics is a
useful
tool for the programmer but they are not the same thing.


> But then the real world sets in.

it has that nasty habbit


> The thing is, mathematicians spend their time and energy studying the
> implications of some set of definitions but they also invest a lot of
> themselves trying to prove that the stuff they come up with is correct.
> This mindset is lost in software development, whose approach to the
> mathematical problem of developing a program often ends with providing code
> which only works as expected in very limited circumstances which no one
> knows or cares to know.  Even those who actually care for this sort of stuff
> and actually know their onions shy away from this goal, a fact which may be
> represented by Knuth's quote "Beware of bugs in the above code; I have only
> proved it correct, not tried it."

mathematicians and programmers do not have the same goals.  The
programmer's
aim is to produce things that do useful stuff whilst staying within
resource
constraints (development time/money, run time/memory/money).

Even proven programs have to be tested. Our compilers aren't proven
and nor are our libraries. And they don't do proofs of correctness on
the hardware (not since Viper anyway).


> Meanwhile, the programming world occupies itself hacking together sets of
> instructions which no one actually cares they are proven to be correct, or
> even if they are valid in the conceivable scenarios which they are designed
> to operate.  That is, when compared to how a mathematician may tackle a
> problem, programmers don't actually know what they are doing and instead
> embrace the fact that the stuff they create does break and that they can't
> do anything to prevent it.  The disregard for this mathematical correctness
> has reached a level that some programming errors committed by programmers
> are so widespread and so frequent that, instead of trying to make sure that
> the programmer is sufficiently competent to avoid them, they are simply
> embraced as a natural occurrence and technologies have been developed to be
> able to sweep those programming errors under the proverbial rug, which is
> the case of technologies such as garbage collection and sandboxes.

both garbage collection and sandboxes have other reasons to exist.

garbage collectors arose out of languages (Lisp) that probably had a
more sound mathematical basis than the vast majority of languages.
They were also invented in the programming paleolithic, when resource
constraints were *really* resource constraints. It is a perfectly
sound design choice to automate things. Does your car have a starting
handle?

sandboxes are also needed because not everyone who wants to run
programs on
your computer has your best interests at heart.


> And the thing is, this isn't necessarily bad.  Of course, it would be better
> if every piece of softwar[e] ever written would have been developed with enough
> care to be successfully demonstrated to be correct.  Yet, that would mean
> that an ungodly amount of time and energy (and, of course, money) would be
> spent on developing even the smallest program.

unit test when properly done could be thought of as an automated proof
system

> Although it would save a lot
> of time and energy in some areas (for example, the software security
> business, at least as we know it, would have never existed)

but something would. Security is a Hard Problem. Some parts of it hit
Halting Problem difficulties. Addmittedly virus checkers seem like a
fundamentally a broken solution.


> it would simply
> be too cost-prohibitive and also time-consuming to develop any piece of
> software.

yes!


> So, to sum things up, programming is in fact applied math and therefore a
> programmer needs to employ mathematical reasoning to develop software.

no. But it wouldn't hurt if programmers thought like this more.
Bentley's Programming Pearls is worth a read.


>  Yet,
> as no one bothers to prove their code to be correct, either by incompetence
> or by simply not being able to afford it,

or ignorance. I suspect most programmers would not have a clue where
to start.
Or express surprise that such a thing was even conceivable!


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

not drifted, more like hoist the mainsail and pointed down wind.

Although I seem to be disagreeing- well actually I /am/ disagreeing.
Programming
is /not/ mathematics and nor should it be. OTOH I agree more formality
probably
wouldn't do any harm.

We /should/ wonder if our loops will terminate and under what
conditions our program
should be expected to work.

Each "module" (line, function, package, program...) should have a pre-
condition (what
it expects to be true before it executes), a post-condition (what will
be true when it
terminates, if its pre-condition was met) and some guarantee it will
terminate.
Even thinking about these things helps.

OO programmers should think about class invarients.

Whilst full blown proofs are too expensive in most environments.
There's DbC and even the humble assert. Lots of unit tests.

Mathematicians may laugh being a little bit informal is like being
little bit pregnant.
But *my* machine doesn't come with an infinite tape!

[toc] | [prev] | [next] | [standalone]

#704

On Jul 21, 4:27 am, Rui Maciel <rui.mac...@gmail.com> wrote:
> Chad wrote:


> > One of my friends who attends Harvard took Math 55. He mentioned that
> > a lot of it was being able to prove major theorems with only the aid
> > of the definitions. This got me to thinking.  I've had a lot of people
> > help with me a programming problem by only providing defintions.
>
> > Is the thought process to proving some major theorems in math with
> > only the aid of the defintions similar to implementing some kind of
> > data structures when given only the definitions of a data structure?

I'm not sure this is well formed sentence.


> Sometimes it may be overlooked but programming is inherently and
> fundamentally a mathematical endeavour,

"up to a point Lord Copper"


> [...] which basically involves nothing
> else than a set of operators being applied to a set of fields in a specific
> order in order to reach an intended outcome.  Following this interpretation,
> any API is nothing more than a set of definitions of a mix of operators and
> sets which a programmer may apply to his sets of data.  With this in mind,
> the answer to your question would be a clear yes, mathematical reasoning is
> as vital to a mathematician as it is to a programmer.  It is because
> mathematics and programming are the same thing.

in a sense Civil engineering is just applied maths.

Mathematics and programming are /not/ the same thing. Mathematics is a
useful
tool for the programmer but they are not the same thing.


> But then the real world sets in.

it has that nasty habbit


> The thing is, mathematicians spend their time and energy studying the
> implications of some set of definitions but they also invest a lot of
> themselves trying to prove that the stuff they come up with is correct.
> This mindset is lost in software development, whose approach to the
> mathematical problem of developing a program often ends with providing code
> which only works as expected in very limited circumstances which no one
> knows or cares to know.  Even those who actually care for this sort of stuff
> and actually know their onions shy away from this goal, a fact which may be
> represented by Knuth's quote "Beware of bugs in the above code; I have only
> proved it correct, not tried it."

mathematicians and programmers do not have the same goals.  The
programmer's
aim is to produce things that do useful stuff whilst staying within
resource
constraints (development time/money, run time/memory/money).

Even proven programs have to be tested. Our compilers aren't proven
and nor are
our libraries. And they don't do proofs of correctness on the hardware
(not since
Viper anyway).


> Meanwhile, the programming world occupies itself hacking together sets of
> instructions which no one actually cares they are proven to be correct, or
> even if they are valid in the conceivable scenarios which they are designed
> to operate.  That is, when compared to how a mathematician may tackle a
> problem, programmers don't actually know what they are doing and instead
> embrace the fact that the stuff they create does break and that they can't
> do anything to prevent it.  The disregard for this mathematical correctness
> has reached a level that some programming errors committed by programmers
> are so widespread and so frequent that, instead of trying to make sure that
> the programmer is sufficiently competent to avoid them, they are simply
> embraced as a natural occurrence and technologies have been developed to be
> able to sweep those programming errors under the proverbial rug, which is
> the case of technologies such as garbage collection and sandboxes.

both garbage collection and sandboxes have other reasons to exist.

garbage collectors arose out of languages (Lisp) that probably had a
more sound
mathematical basis than the vast majority of languages. They were also
invented
in the programming paleolithic, when resource constraints were
*really* resource
constraints. It is a perfectly sound design choice to automate things.
Does your
car have a starting handle?

sandboxes are also needed because not everyone who wants to run
programs on
your computer has your best interests at heart.


> And the thing is, this isn't necessarily bad.  Of course, it would be better
> if every piece of softwar[e] ever written would have been developed with enough
> care to be successfully demonstrated to be correct.  Yet, that would mean
> that an ungodly amount of time and energy (and, of course, money) would be
> spent on developing even the smallest program.

unit test when properly done could be thought of as an automated proof
system

> Although it would save a lot
> of time and energy in some areas (for example, the software security
> business, at least as we know it, would have never existed)

but something would. Security is a Hard Problem. Some parts of it hit
Halting
Problem difficulties. Addmittedly virus checkers seem like a
fundamentally a
broken solution.


> it would simply
> be too cost-prohibitive and also time-consuming to develop any piece of
> software.

yes!


> So, to sum things up, programming is in fact applied math and therefore a
> programmer needs to employ mathematical reasoning to develop software.

no. But it wouldn't hurt if programmers thought like this more.
Bentley's Programming Pearls is worth a read.


>  Yet,
> as no one bothers to prove their code to be correct, either by incompetence
> or by simply not being able to afford it,

or ignorance. I suspect most programmers would not have a clue where
to start.
Or express surprise that such a thing was even conceivable!


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

not drifted, more like hoist the mainsail and pointed down wind.

Although I seem to be disagreeing- well actually I /am/ disagreeing.
Programming
is /not/ mathematics and nor should it be. OTOH I agree more formality
probably
wouldn't do any harm.

We /should/ wonder if our loops will terminate and under what
conditions our program
should be expected to work.

Each "module" (line, function, package, program...) should have a pre-
condition (what
it expects to be true before it executes), a post-condition (what will
be true when it
terminates, if its pre-condition was met) and some guarantee it will
terminate.
Even thinking about these things helps.

OO programmers should think about class invarients.

Whilst full blown proofs are too expensive in most environments.
There's DbC and even
the humble assert. Lots of unit tests.

Mathematicians may laugh being a little bit informal is like being
little bit pregnant.
But *my* machine doesn't come with an infinite tape!

[toc] | [prev] | [next] | [standalone]

#703

On Jul 19, 8:20 pm, Chad <cdal...@gmail.com> wrote:
> One of my friends who attends Harvard took Math 55. He mentioned that
> a lot of it was being able to prove major theorems with only the aid
> of the definitions. This got me to thinking.  I've had a lot of people
> help with me a programming problem by only providing defintions.
>
> Is the thought process to proving some major theorems in math with
> only the aid of the defintions similar to implementing some kind of
> data structures when given only the definitions of a data structure?
>
> Chad

ping

[toc] | [prev] | [next] | [standalone]

#705

On Jul 21, 4:27 am, Rui Maciel <rui.mac...@gmail.com> wrote:
> Chad wrote:


> > One of my friends who attends Harvard took Math 55. He mentioned that
> > a lot of it was being able to prove major theorems with only the aid
> > of the definitions. This got me to thinking.  I've had a lot of people
> > help with me a programming problem by only providing defintions.
>
> > Is the thought process to proving some major theorems in math with
> > only the aid of the defintions similar to implementing some kind of
> > data structures when given only the definitions of a data structure?

I'm not sure this is well formed sentence.


> Sometimes it may be overlooked but programming is inherently and
> fundamentally a mathematical endeavour,

"up to a point Lord Copper"


> [...] which basically involves nothing
> else than a set of operators being applied to a set of fields in a specific
> order in order to reach an intended outcome.  Following this interpretation,
> any API is nothing more than a set of definitions of a mix of operators and
> sets which a programmer may apply to his sets of data.  With this in mind,
> the answer to your question would be a clear yes, mathematical reasoning is
> as vital to a mathematician as it is to a programmer.  It is because
> mathematics and programming are the same thing.

in a sense Civil engineering is just applied maths.

Mathematics and programming are /not/ the same thing. Mathematics is a
useful
tool for the programmer but they are not the same thing.


> But then the real world sets in.

it has that nasty habbit


> The thing is, mathematicians spend their time and energy studying the
> implications of some set of definitions but they also invest a lot of
> themselves trying to prove that the stuff they come up with is correct.
> This mindset is lost in software development, whose approach to the
> mathematical problem of developing a program often ends with providing code
> which only works as expected in very limited circumstances which no one
> knows or cares to know.  Even those who actually care for this sort of stuff
> and actually know their onions shy away from this goal, a fact which may be
> represented by Knuth's quote "Beware of bugs in the above code; I have only
> proved it correct, not tried it."

mathematicians and programmers do not have the same goals.  The
programmer's
aim is to produce things that do useful stuff whilst staying within
resource
constraints (development time/money, run time/memory/money).

Even proven programs have to be tested. Our compilers aren't proven
and nor are
our libraries. And they don't do proofs of correctness on the hardware
(not since
Viper anyway).


> Meanwhile, the programming world occupies itself hacking together sets of
> instructions which no one actually cares they are proven to be correct, or
> even if they are valid in the conceivable scenarios which they are designed
> to operate.  That is, when compared to how a mathematician may tackle a
> problem, programmers don't actually know what they are doing and instead
> embrace the fact that the stuff they create does break and that they can't
> do anything to prevent it.  The disregard for this mathematical correctness
> has reached a level that some programming errors committed by programmers
> are so widespread and so frequent that, instead of trying to make sure that
> the programmer is sufficiently competent to avoid them, they are simply
> embraced as a natural occurrence and technologies have been developed to be
> able to sweep those programming errors under the proverbial rug, which is
> the case of technologies such as garbage collection and sandboxes.

both garbage collection and sandboxes have other reasons to exist.

garbage collectors arose out of languages (Lisp) that probably had a
more sound
mathematical basis than the vast majority of languages. They were also
invented
in the programming paleolithic, when resource constraints were
*really* resource
constraints. It is a perfectly sound design choice to automate things.
Does your
car have a starting handle?

sandboxes are also needed because not everyone who wants to run
programs on
your computer has your best interests at heart.


> And the thing is, this isn't necessarily bad.  Of course, it would be better
> if every piece of softwar[e] ever written would have been developed with enough
> care to be successfully demonstrated to be correct.  Yet, that would mean
> that an ungodly amount of time and energy (and, of course, money) would be
> spent on developing even the smallest program.

unit test when properly done could be thought of as an automated proof
system

> Although it would save a lot
> of time and energy in some areas (for example, the software security
> business, at least as we know it, would have never existed)

but something would. Security is a Hard Problem. Some parts of it hit
Halting
Problem difficulties. Addmittedly virus checkers seem like a
fundamentally a
broken solution.


> it would simply
> be too cost-prohibitive and also time-consuming to develop any piece of
> software.

yes!


> So, to sum things up, programming is in fact applied math and therefore a
> programmer needs to employ mathematical reasoning to develop software.

no. But it wouldn't hurt if programmers thought like this more.
Bentley's Programming Pearls is worth a read.


>  Yet,
> as no one bothers to prove their code to be correct, either by incompetence
> or by simply not being able to afford it,

or ignorance. I suspect most programmers would not have a clue where
to start.
Or express surprise that such a thing was even conceivable!


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

not drifted, more like hoist the mainsail and pointed down wind.

Although I seem to be disagreeing- well actually I /am/ disagreeing.
Programming
is /not/ mathematics and nor should it be. OTOH I agree more formality
probably
wouldn't do any harm.

We /should/ wonder if our loops will terminate and under what
conditions our program
should be expected to work.

Each "module" (line, function, package, program...) should have a pre-
condition (what
it expects to be true before it executes), a post-condition (what will
be true when it
terminates, if its pre-condition was met) and some guarantee it will
terminate.
Even thinking about these things helps.

OO programmers should think about class invarients.

Whilst full blown proofs are too expensive in most environments.
There's DbC and even
the humble assert. Lots of unit tests.

Mathematicians may laugh being a little bit informal is like being
little bit pregnant.
But *my* machine doesn't come with an infinite tape!

[toc] | [prev] | [next] | [standalone]

#745

On Jul 25, 2:07 pm, Nick Keighley <nick_keighley_nos...@hotmail.com>
wrote:

sorry about the repeats! Google Groups problems

[toc] | [prev] | [standalone]

Back to top | Article view | comp.programming

csiph-web