A gentle introduction to C* V

In a digital computational system, software is constructed under two separate but equally important premises. These are their stories.

Welcome to part five of A gentle introduction to C* – the first post where we dive deep into the nuts & bolts of the often mentioned Law & Order that makes C* so special.

First, here’s an executive summary: Law & Order is a colloquialism coined to market a novel feature of C* that is new in the world of programming languages. The formal name (or definition, really) of this is fully arbitrary mutability of state. This is achieved by imposing constraints, or laws, on data types, analytically enforcing them at compile time through something called a transient variable lifetime, and marshalling the enforcement on data from foreign code at cost.

Before we get into what this means, let me make sure you understand what it is not. Law & Order is not formal verification, as it has nothing to do with enforcing the correctness of code; it is solely concerned with the form taken by data. Nor is Law & Order at all related to dependent typing; like C, C* does not have much in the way of a type system at all. There are really only numerics, somethings (bits) and nothings (void), and structs to stack it all together, with some clever syntax to make construing a program’s ABI something less than a giant pain in the neck. C* does not hold the names of things to be semantically important for construing the meaning or behaviour of a program at all.

---

So, with those bits out of the way, let’s talk about laws.