A question about thinking 'abstractly'....

Discussion in 'C Programming' started by Chad, Jul 19, 2011.

  1. Chad

    Chad Guest

    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, Jul 19, 2011
    #1
    1. Advertising

  2. Chad

    Stefan Ram Guest

    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/Abstraction_(computer_science)
     
    Stefan Ram, Jul 19, 2011
    #2
    1. Advertising

  3. 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.
     
    Ben Bacarisse, Jul 19, 2011
    #3
  4. On Jul 19, 9:20 pm, 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?


    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
     
    Kleuskes & Moos, Jul 19, 2011
    #4
  5. On 19 Jul, 20:20, 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?
    >
    > 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
     
    Ulisses Araujo Costa, Jul 20, 2011
    #5
  6. On Jul 20, 11:23 am, Ulisses Araujo Costa
    <> wrote:
    > On 19 Jul, 20:20, 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?

    >
    > > 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.
     
    Kleuskes & Moos, Jul 20, 2011
    #6
  7. On 20 Jul, 11:46, "Kleuskes & Moos" <> wrote:
    > On Jul 20, 11:23 am, Ulisses Araujo Costa
    >
    >
    >
    >
    >
    >
    >
    >
    >
    > <> wrote:
    > > On 19 Jul, 20:20, 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?

    >
    > > > 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
     
    Ulisses Araújo Costa, Jul 20, 2011
    #7
  8. Chad

    Rui Maciel Guest

    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
     
    Rui Maciel, Jul 21, 2011
    #8
  9. On Jul 19, 8:20 pm, 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?
    >
    > Chad


    ping
     
    Nick Keighley, Jul 25, 2011
    #9
  10. On Jul 21, 4:27 am, Rui Maciel <> 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!
     
    Nick Keighley, Jul 25, 2011
    #10
  11. On Jul 25, 2:07 pm, Nick Keighley <>
    wrote:

    sorry about the repeats! Google Groups problems
     
    Nick Keighley, Aug 10, 2011
    #11
    1. Advertising

Want to reply to this thread or ask your own question?

It takes just 2 minutes to sign up (and it's free!). Just click the sign up button to choose a username and then you can ask your own questions on the forum.
Similar Threads
  1. Homa
    Replies:
    7
    Views:
    453
    John Saunders
    Nov 16, 2003
  2. Simon Harris

    Thinking the right way?

    Simon Harris, May 31, 2004, in forum: ASP .Net
    Replies:
    4
    Views:
    377
    Simon Harris
    Jun 2, 2004
  3. Giammarco
    Replies:
    2
    Views:
    403
    Giammarco
    Aug 25, 2005
  4. metaperl
    Replies:
    3
    Views:
    292
    Steven D'Aprano
    Jan 24, 2007
  5. optimistx

    Linear thinking vs essential thinking

    optimistx, Oct 28, 2009, in forum: Javascript
    Replies:
    4
    Views:
    179
    Dr J R Stockton
    Oct 29, 2009
Loading...

Share This Page