«

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

Chad <> writes:
>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?

See also:

http://en.wikipedia.org/wiki/Abstrac...mputer_science)

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

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

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

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.

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

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

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

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!