Q.E.D. Code

In 2000, Eric Brewer presented the CAP Conjecture to the Symposium on Principles of Distributed Computing. This states that a distributed system cannot simultaneously guarantee consistency, availability, and partition tolerance. It can, however, guarantee two of the three. It makes little sense to talk about guaranteeing consistency and availability while sacrificing partition tolerance. Network partitions are going to occur, so we must choose whether we are going to give up consistency or availability when that happens.

Mathematical induction is a style of proof whereby you prove the base case (typically N = 1), and then you prove the inductive step (that if it's true for N, it's true for N+1). In programming, mathematical induction is used when writing recursive functions. First, implement the function for the base case. Then, assuming that the function works for smaller cases, reuse it to implement the function for larger ones.

Constructors can be used to prove that one thing happens before another, and furthermore that it does not happen again. The constructor is the only method that must be called once, and cannot be called twice. Furthermore, it must be called before any other method of the object. This is a powerful contract that should not be misused.

Knowing that a directed graph is acyclic is useful. If you construct directed graphs in a certain way, then you can prove that they have no cycles. Design systems to produce constructable graphs, and you can take advantage of all of the theorems known to be true of DAGs.

Alan Turing proved that there could not be a general procedure to determine whether an expression in first order predicate calculus is satisfyable. This extends Godel's Incompleteness Theorem by asserting not only that there are some true statements that cannot be proven, but also that there is no way to decide whether a statement in general even has a proof.

In the process of constructing this proof, Alan Turing defined the Universal Machine, which can perform any mechanical computation. This is the genesis of the computers that we use today.

Leslie Lamport finishes off his paper on Time, Clocks, and the Order of Events in a Distributed System by showing how to synchronize physical clocks. This is useful to avoid anomalies caused by communications out-of-band. He calculates how quickly we can expect the clocks to become synchronized, so that we can set expectations and improve our designs.

In a directed acyclic graph, we can use reachability to determine a partial order. But sometimes we want a total ordering of the nodes to accomplish some result. There are usually many possible total orderings that satisfy the partial ordering. Topological sorting algorithms can help us discover them, whether we want just one, or all possible orderings.

Unit tests can only cover one scenario. Mathematical proof, while it generalizes to many scenarios, is not always feasible. Thankfully, we have tools that will search the input space to help us find problems in our code. Parameterized unit tests come in two flavors: generitive tests and exploratory tests. Generitive testing tools, like Quick Check and Test.Check, try random inputs. Exploratory testsing tools, like Pex and Code Digger, discover scenarios that cover as many branches in the code as possible. These tools are a good addition to the other two, helping us fill that gap.

Leslie Lamport used logical clocks in a distributed system to solve the mutual exclusion problem. He used the partial order of "happened before" to construct one possible total ordering of events. He then applies this total ordering to the mutual exclusion problem so that processes can determine whether they own the shared resource.

A fully ordered set is one in which we can tell for any two members which one comes before the other. Think integers. A partially ordered set, however, only gives us an answer for some pairs of nodes. A directed acyclic graph defines a partial order over its nodes. Find out how to compute this partial order, and some of the ways in which it can be applied.

The number of degrees of freedom in a system of equations is equal to the number of unknowns minus the number of equations. We can add unknowns, as long as we also add the same number of equations, without changing the behavior of the system. Then we can rewrite the equations, again without changing behavior, to solve for some of those unknowns in terms of others. Doing so, we divide the system into independent and dependent variables. The number of degrees of freedom is equal to the number of independent variables.

In 1978, Leslie Lamport wrote "Time, Clocks, and the Ordering of Events in a Distributed System". In this paper, he constructs a clock that gives us a way of saying which events in a distributed system happened before another. See how he did it, and start to imagine why this might be useful.

The number of degrees of freedom in a solution should match the number in the problem. If you have extra degrees of freedom, then you have to write extra code to keep them in sync. This opens the door for bugs.

To count the degrees of freedom in a solution, count the mutable fields and the auto properties. These constructs introduce one degree of freedom for each instance of the object.

Kurt Godel proved that first order predicate calculus is complete. Any true statement can be proven from axioms. However, he also proved that more complex systems are incomplete. No matter how many axioms you introduce, there will be true statements that you cannot prove. See how he did it, and how that eventually lead to the invention of the comupter.

Many of the data structures that we use are directed graphs. Relational databases have foriegn keys, which are directional edges between two records. Build systems have dependencies, which are directional edges between projects. Some of these systems not only directed, but also acyclic. Find out which ones, and prepare to explore the advantages of directed acyclic graphs.

In the .NET Socket API, if you call methods in the wrong order, the Socket class will throw an exception. Wouldn't it be better if it guided you into the pit of success at compile time? One pattern from the Gang of Four book holds the key to proving that prerequisites happen first.

You can compute how many degrees of freedom are in a problem. This tells you how many decisions you can make, or how many values it takes to describe the current state. Knowing this will tell you some interesting things about the solution to that problem.

Daan Leijen explores the balance between type constraints, which make it possible to prove interesting assertions about values, and generalizations, which make it easy to express types. Finding this balance is sometimes a hard problem, leading some to abandon statically typed languages for dynamically typed ones. In Extensible Records with Scoped Labels, Daan shows us how we can take on some of the power of dynamic typing -- extension -- without giving up type inference.

FirstOrDefault is an extension method used in Linq. It is often used incorrectly, leading to exceptions or ignored data. Learn techniques for accessing members of a Linq expression without the possibility of errors.

"Theorem" and "theory" sound similar, but they mean completely different things. Learn the difference, and how a theorem can be part of a theory.

Continuing with Claude E. Shannon's "The Mathematical Theory of Communication", we learn how to model random noise within a channel. How does this noise effect the bandwidth of the channel? How can we achieve any desired confidence in the message received, shy of certainty?

The math tells us how.