Engineering Fluency OS

Why This Matters

Testing can show that code works for specific inputs, but it cannot guarantee correctness for all inputs. A direct proof does exactly that: it builds a chain of logical steps from accepted truths to a conclusion, covering every possible case. When you prove that your sorting algorithm always produces a sorted output, you have a guarantee no amount of testing can match.

A theorem is a statement that has been proven true. An axiom is a statement accepted as true without proof, serving as a starting point. Direct proof works by assuming the hypothesis is true and then applying definitions, axioms, and previously proven theorems step by step until you reach the desired conclusion.

Direct proof is the most straightforward proof technique. It teaches you to think rigorously and to justify every step. This skill transfers directly to writing correct code: every line should follow logically from what came before. When you can construct a direct proof, you can also write clear documentation, explain your reasoning in code reviews, and design algorithms with provable properties.

Define Terms

Visual Model

Hypothesis (Given)Assume P is true

Axioms / DefinitionsAccepted truths

Step 1Apply definition

Step 2Apply known theorem

Step 3Algebraic manipulation

Conclusion (Q)Therefore Q is true

Theorem: P implies QProven statement

The full process at a glance. Click Start tour to walk through each step.

A direct proof chains logical steps from hypothesis to conclusion, with each step justified by definitions or known theorems.

Code Example

Code

// Direct proof pattern: verify a theorem computationally
// Theorem: The sum of two even numbers is always even

function isEven(n) {
  return n % 2 === 0;
}

// Direct verification for specific cases
function verifySumOfEvens(a, b) {
  if (!isEven(a) || !isEven(b)) {
    console.log(`${a} and ${b} are not both even. Skipping.`);
    return;
  }
  const sum = a + b;
  const result = isEven(sum);
  console.log(`${a} + ${b} = ${sum}, is even: ${result}`);
  return result;
}

verifySumOfEvens(4, 6);   // 10, is even: true
verifySumOfEvens(12, 8);  // 20, is even: true
verifySumOfEvens(0, 14);  // 14, is even: true

// Exhaustive check over a range (computational proof)
function proveForRange(max) {
  for (let a = 0; a <= max; a += 2) {
    for (let b = 0; b <= max; b += 2) {
      if (!isEven(a + b)) {
        console.log(`COUNTEREXAMPLE: ${a} + ${b} = ${a+b}`);
        return false;
      }
    }
  }
  console.log(`Verified for all even pairs up to ${max}`);
  return true;
}

proveForRange(100); // Verified for all even pairs up to 100

// The actual proof:
// Let a = 2m and b = 2n (definition of even)
// a + b = 2m + 2n = 2(m + n)
// Since m + n is an integer, a + b is even (definition of even)
console.log("Direct proof: 2m + 2n = 2(m+n), which is even by definition.");

Interactive Experiment

Try these exercises:

Prove computationally that the product of two odd numbers is always odd. Test all odd pairs up to 50.
Write a function that takes two even numbers and returns the "proof trace": the values of m, n, m+n, and 2(m+n).
Verify that for any integer n, n squared + n is always even. Test for n from -10 to 10.
Try to find a counterexample to "the sum of two even numbers is even." What does failure to find one suggest?
Prove that if n is divisible by 6, then n is divisible by both 2 and 3. Verify for n = 6, 12, 18, 24.

Quick Quiz

Coding Challenge

Sum of Evens Verifier

Write a function called `verifySumEvens` that takes two integers a and b. If both are even, return true if their sum is even (which it always should be). If either is not even, return false to indicate the precondition was not met. This computationally verifies the theorem: the sum of two even numbers is even.

Loading editor...

Real-World Usage

Direct proof thinking applies throughout software engineering:

Algorithm correctness: Loop invariants are proven by direct proof: the invariant holds at initialization, and each iteration preserves it.
Type systems: Type checking is a form of proof. If every operation is type-safe, the whole program is type-safe. Each step is verified directly.
Smart contracts: Blockchain smart contracts require formal verification. Direct proofs show that funds cannot be lost or locked.
Protocol design: Security proofs for encryption protocols chain logical steps to show that an adversary cannot break the system.
API documentation: Preconditions and postconditions form a contract. If the precondition holds (input is valid), the postcondition is guaranteed (output is correct).

Direct Proof