Making Reasoning Obviously Locally Correct

post by JGWeissman · 2011-03-12T19:41:44.756Z · LW · GW · Legacy · 26 comments

Contents

  us = Request("name")
  s = Request("name")
  us = Request("name")
  usName = us
  sName = us
  sName = Encode(us)
  Write usName
  Write sName
  Write Encode(usName)
None
26 comments

             x = y

            x² = x*y

     x² - y² = x*y - y²

(x+y)(x-y) = y(x-y)

         x+y = y

         y+y = y

         2*y = y

            2 = 1

The above is an incorrect "proof" that 2=1. Even for those who know where the flaw is, it might seem reasonable to react to the existence of this "proof" by distrusting mathematical reasoning, which might contain such flaws that lead to erroneous results. But done properly, mathematical reasoning does not look like this "proof". It is more explicit, making each step obviously correct that an incorrect step cannot meet the standard. Let's take a look at what would happen when attempting to present this "proof" following this virtue:

The set of real numbers is known to be non empty, so let y be a real number. Let x = y.

By an axiom of the real numbers, a real number multiplied by a real number is a real number, so x*x = x*y.^α

By the same axiom y*y is a real number. By an axiom y*y has an additive inverse -y*y.

By an axiom, adding a real number to a real number is a real number, so x*x + -y*y = x*y + -y*y.

By axioms defining addition, multiplication, and additive inverse, (x+y)*(x+-y) and y*(x+-y) are real numbers.

By the distributive law of multiplication over addition, (x+y)*(x+-y) = (x+y)*x + (x+y)*(-y) = x*x + y*x + x*(-y) + y*(-y)

By commutativity and associativity of addition and multiplication, and distribution of multiplication over additive inverses,

  x*x + y*x + x*(-y) + y*(-y) = x*x + (x*y + -x*y) + - y*y = x*x + -y*y

Similarly y*(x+-y) = y*x + y*(-y) = x*y + -y*y

So, by transitivity of equality, (x+y)*(x+-y) = y*(x+-y)

By an axiom a real number not equal to zero has a multiplicative inverse. I want x+-y to have a multiplicative inverse, so I want to prove that x+-y is not zero, but I can't, since it is not true. By construction x = y, so x+-y= y+-y, and by the definition of an additive inverse, y+-y = 0. The proof fails.

Now, citing axioms and theorems to justify a step in a proof is not a mere social convention to make mathematicians happy. It is a useful constraint on your cognition, allowing you to make only inferences that are actually valid. Similarly, there is a virtue in the art of programming that constrains you from making mistakes in code. In Making Wrong Code Look Wrong, Joel Spolsky describes a solution to the problem of keeping track of which strings are already HTML encoded and ready to be written to a web page, and which strings are unformatted and may have come from a malicious user who wants to inject an evil script into your website (or a normal user who wants to display a message with characters that happen to be HTML control characters):

All strings that come from the user must be stored in variables (or database columns) with a name starting with the prefix "us" (for Unsafe String). All strings that have been HTML encoded or which came from a known-safe location must be stored in variables with a name starting with the prefix "s" (for Safe string).

Let me rewrite that same code, changing nothing but the variable names to match our new convention.

us = Request("name")

...pages later...
usName = us

...pages later...
recordset("usName") = usName

...days later...
sName = Encode(recordset("usName"))

...pages or even months later...
Write sName

Every line of code can be inspected by itself, and if every line of code is correct, the entire body of code is correct.

The thing I want you to notice about the new convention is that now, if you make a mistake with an unsafe string, you can always see it on some single line of code, as long as the coding convention is adhered to:

s = Request("name")

is a priori wrong, because you see the result of Request being assigned to a variable whose name begins with s, which is against the rules. The result of Request is always unsafe so it must always be assigned to a variable whose name begins with “us”.

us = Request("name")

is always OK.

usName = us

is always OK.

sName = us

is certainly wrong.

sName = Encode(us)

is certainly correct.

Write usName

is certainly wrong.

Write sName

is OK, as is

Write Encode(usName)

Just like the single step in the attempted mathematical proof that can't be explicitly justified, a single line of code violating Spolsky's convention is obviously wrong. In both these cases, it is possible to be sufficiently explicit and detailed that an automated process can verify correctness, a proof verifier for mathematics and compilers and static analysis for computer programs.

What about in domains where everything is not so clearly defined, where you have to deal with uncertainty? Well, first of all, probability theory is a mathematical description of uncertainty. You can be rigorous in keeping track of what the ideal amount of uncertainty is for a particular claim. Though that is a lot of work, and may be worthwhile only for beliefs that inform important decisions. But even in your everyday reasoning, beware local mistakes. Just as Spolsky would advise you to scream "Error!" wherever an unsafe string is stored in a variable meant for safe strings, even if that unsafe string never ends up written to a web page (until someone makes some locally correct modifications), don't wait for a global failure to hit you over the head with the wrongness of your local mistake. Nip that problem in the bud, back up, and do it right. And try to have a simply verified concept of locally correct that still adds up to globally correct.

 

---

 

α. I am being extra explicit in that I am avoiding using common notations that have been carefully defined with rules of manipulation derived from more basic rules of inference. This is for the benefit of non mathematicians who may have learned these notations (like subtraction, exponents) but not their justifications.

 

26 comments

Comments sorted by top scores.