Nick Keighley
7/21/2011 12:11:00 PM
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