Carlos Scheidegger sent this proof which is better than my attempt at why -1 * -1 = 1...
The definition of multiplication for whole numbers is:
x * y = y + y + y + ... + y + y, where y appears x times.
Using this, it is easy to prove that, being (succ x) the successor of x,
if x * y = z, then (succ x) * y = z + y, and vice-versa.
By definition, 0 is the successor of -1. Also by definition,
0 * x = 0,
and so, 0 * -1 = 0.
(succ -1) * -1 = 0
(succ -1) * -1 = 1 + -1
Now, we apply the property:
(succ -1) * -1 = 1 + -1 ->
-1 * -1 = 1
----
This proof's only assumption is that -n + n = 0, which is easily
provable. (Very easy using peano arithmetic)
A number of wonderful (literally) thoughts are wrapped up in Ian's item on testing, Dijkstra, Turing, and beautiful code.
One at a time...
On point 1, I would say that developing in a test-driven way is kind of like developing proofs incrementally. Once your code passes the tests, you have not proven the absence of all bugs, but you have at least proven the absence of all bugs you thought were important at the time. So you are not done, but you are significantly closer to being done.
On point 2, I would say that rereading (and refactoring) to achieve "conceptual integrity" is kind of like making a proof more comprehensible. You have done the messy work, now make sure it is presentable so others can use it, extend it, or carry the "proof-in-progress" further with more tests.
On point 3, I would point out that the lambda calculus is not talked about enough in computer science education generally. Developed by Alonzo Church, a peer of Turing, the calculus is both equivalent to the Turing Machine and closer to modern programming languages than is the Turing Machine. (Of course, it doesn't have I/O either, so I am not sure what to do about that argument.) Programming language semanticists as well as compiler writers actually use properties of the lambda calculus all the time. I am not sure the same could be said for the Turing Machine.
Sean asks for an explanation of why a negative times a negative is a positive.
Here we go...
-x * -y = (-1 * x) * (-1 * y) = (-1 * -1) * (x * y) = 1 * (x * y) = x * y
Obsessive Update: The above assumes -1 * -1 = 1. Why? The only thing I thought of, which really becomes a general rule is to create a contradiction. If -1 * -1 = -1 then...
...which is the contradiction we're hoping for.
-1 * (1 - 1) = (-1 * 1) + (-1 * -1)
-1 * (0) = (-1) + (-1)
0 = -2
Update: maybe Sean is looking for an applied explanation rather than a proof?
Hmm... that would be a good one. When do we do -x * -y in the real world?
Well, I do x * -y in the real world when I pay my mortgage (-y) for some number of months (x). So maybe I could ask how much I would have had had I not paid my mortgage (-y) the previous number of months (-x).
Clearly the result of these two formulas should be the opposite. If I paid -$N USD then if I didn't I would have saved $N USD.
A Maryland resident, who installed a photovoltaic system and now contributes more juice to the grid than he draws, made the point on CSPAN that, at current PV prices, someone making a car purchase could buy a less expensive car instead of an SUV and have enough left over to install a PV for their house.
Given current events at home and abroad, would you recommend to your representatives to increase incentives and funding for making each of us net contributors to the grid?
Independence and self-sufficiency is the American way, no? This should be a federal priority at least as important as the federal highway system. A solar system in New York produces 80% of the output as in the Southwest, so this is more than a regional option, especially combined with insulation and other improvements.
Conversion would make a healthy contribution to the employment situation as well as the environment.