Why you do not have to prove your function

You do not have to prove your function because software verification is a ladder, not a binary choice.

Many developers look at a law of physics, like Ohm’s law (V=IR), and see a “proven” truth. They wonder why they cannot provide the same certainty for their code. They ask: “Why do I not have to prove my function?”

To answer this, we must first understand what a law of physics actually is. Ohm’s law is not a mathematical theorem. It is an empirical law. Georg Ohm measured the relationship between voltage and current in 1827 and found a regularity that holds for most conductive materials. We use V=IR in every circuit without re-verifying it because the law is universal within its domain and stated simply.

Software correctness is different. It is not a claim about the physical world, but a relation between code and a written specification. A specification is a formal statement of what the code must do for all possible inputs.

Most developers start at the first rung of the assurance ladder: validation. Validation is the process of checking that the code behaves as expected on specific, tried inputs. This is usually done with unit tests.

Unit tests are useful, but they are not proofs. A test suite can pass even if the code is buggy. For example, consider a clamp function that restricts a number to a range between a lower and upper bound. A small set of hand-picked tests might pass for both a correct implementation and one where the upper bound is accidentally ignored.

  correct: 4/4 tests passed
  buggy: 4/4 tests passed

The passing tests carry no information about the inputs the developer did not try.

The next rung is property testing. Property testing does not check specific values. Instead, it checks the specification over thousands of random inputs. This method often finds the bugs that hand-picked tests miss because it explores the edges of the input space.

  buggy: PROPERTY VIOLATED  n=1 lo=0 hi=0 -> 1
  correct: property held on all 3321 inputs checked

Property testing is more powerful than unit testing, but it is still not a proof. It can show that a property held for 3,000 inputs, but it cannot say it holds for all possible integers.

The top rung is formal proof. A formal proof does not execute the code. Instead, it uses a symbolic verifier to ask a single question: “Can any input exist that violates the specification?” If the verifier answers that no such counterexample exists, the function is proven correct for all possible inputs.

  result < lo possible?   unsat
  result > hi possible?   unsat
  PROVEN: lo <= clamp(n, lo, hi) <= hi for ALL integers n, lo, hi with lo <= hi

If proof is so certain, why do we not use it for every function?

We face a wall made of three constraints. First, general proof is often impossible. The halting problem proves that no general algorithm can decide if every program will eventually stop or run forever. Testing all inputs is a superset of this problem, which means some questions about program behavior are undecidable.

Second, you can only prove a relation between code and a specification. In most software, the specification is fuzzy or does not exist. The code itself is the specification. Without a formal “source of truth” to check against, there is nothing to prove.

Third, proof is expensive. In the seL4 project, a verified OS kernel, the developers wrote roughly 50 lines of proof for every one line of C code. This drastically increases the cost per line of code and slows down development velocity.

The industry does not ignore proof. It matches the cost of assurance to the stakes of failure.

In aviation, the DO-178C standard governs how software is certified. Where failure is catastrophic, the industry uses formal methods. Projects like seL4 (an OS kernel), CompCert (a C compiler), and HACL* (a cryptographic library) are proven once and then reused everywhere.

At this level, software begins to look like the laws of physics. A proven kernel becomes a foundation that other systems can trust without re-verifying the kernel itself.

You do not have to prove your function because, for most code, the cost exceeds the benefit. Unit tests find the most common bugs cheaply. Property tests find the tricky bugs. Formal proof is reserved for the small, exact invariants where the stakes are high enough to pay for the proof.