|more useful options|
In Re^2: Programming is more like:, moritz brought up the wobbliness of mathematical foundations in physics, when I complained about lack of proper mathematical tools in programming. True, most scientists who do mathematics daily never mind about the actual proofs behind theorems, except of course mathematicians themselves. In physics in particular, there are few purely mathematical proofs; most things can be proven by pointing at a physical fact, or hand-waving as some physicist friends call it. However, this doesn't detract from the usefulness and effectiveness of the method!
I know of a few attempts to conjure "the algebra of programming". Interested monks can search for articles by E. W. Dijkstra (et al., including W. Feijen), David Gries, or Ralph-Johan Back. The approaches are very interesting, and from what I have tried the methods out, I can tell that they do work on small scale -- if-then-else statements, loops, and even individual functions.
Why these methods have not been succesful -- if we measure success by the number of programmers using them -- are partly the same as listed in the parent post, Re: Programming is more like:. An additional reason is that most people seem to regard mathematics as extra labour, waste of time, and something that will guide them away from the actual goal.
A further problem is that the field of programming is very young compared to other big mathematical disciplines. Physics, for instance, begun with astronomy thousands of years ago, and has had rigorous mathematical methods since Newton's times (17th century). Programming is not older than 60 years, and during that time programmable machines have changed a great deal, not to mention programming itself. Even though Von Neumann architecture, for example, has been very successful, there's no saying there wouldn't be better ones out there. If and when such ones are invented, programming languages themselves will change, because most nowadays are (bluntly put) abstractions of the said architecture. A likely catalyst will be quantum computing, unless there will be an additional abstraction layer mimicking a traditional non-quantum one.
So, we don't even know yet what programming is or what it should or will be. We haven't laid down a good enough framework either. You can do loops and conditionals in all programming languages nowadays. Ignoring differences in syntax, they can all be treated same at the abstract level, and useful theorems can be proven about them, if you define useful semantics. But we -- the "average" programmers -- don't know any of the theorems. Given a sorted array and a value we know is in it, why can we know for sure that if we search it in linear order starting at the beginning, we will eventually always find the value at some index? It sounds very basic, and it's not difficult to prove, but the mythical algebra could be built on simple theorems like this, much like Eucledian geometry, and then expanded to cover deeper and more meaningful theorems.
Coming back to physics, programming may not have similar laws as physics does, but if we had something analogous, we could perform similar hand-waving in analyzing problems and actually deriving pieces of the program. This is where the usefulness would lie.