This paper addresses the question ``what is a digital circuit?'' in relation to the fundamentally analog nature of actual (physical) circuits.
A simple informal definition is given and then formalized in the proof assistant Agda.
At the heart of this definition is the \emph{timely} embedding of \emph{discrete} information in temporally \emph{continuous} signals.
Once this embedding is defined (in constructive logic, i.e., type theory), it is extended in a generic fashion from one signal to many and from simple boolean operations (logic gates) to arbitrarily sophisticated sequential and parallel compositions, i.e., to computational circuits.

Rather than constructing circuits and \emph{then} trying to prove their correctness, a \emph{compositionally correct} methodology maintains specification, implementation, timing, and correctness proofs at every step.
Compositionality of each aspect and of their combination is supported by a single, shared algebraic vocabulary and related by homomorphisms.
After formally defining and proving these notions, a few key transformations are applied to reveal the \emph{linearity} of circuit timing (over a suitable semiring), thus enabling practical, modular, and fully verified timing analysis as linear maps over higher-dimensional time intervals.

An emphasis throughout the paper is simplicity and generality of specification, minimizing circuit-specific definitions and proofs while highlighting a broadly applicable methodology of scalable, compositionally correct engineering through simple denotations and homomorphisms.

Conal’s home pageConal Elliott has been working (and playing) in functional programming since 1980. He especially enjoys applying semantic elegance and rigor to library design and optimized implementation. He invented the paradigm now known as “functional reactive programming” in the early 1990s, and then pioneered compilation techniques for high-performance, high-level embedded domain-specific languages, with applications including 2D and 3D computer graphics. The latter work included the first compilation of Haskell programs to GPU code, while maintaining precise and simple denotation and powerful composability, as well as a high degree of optimization. Conal earned a BA in math with honors from the College of Creative Studies at UC Santa Barbara in 1982 and a PhD in Computer Science from Carnegie Mellon University in 1990. He previously worked as software architect at Sun Microsystems, graphics researcher at Microsoft Research, principal engineer at Tabula Inc (on chip specification and compiling Haskell to hardware for massively parallel execution), and distinguished data/AI scientist at Target. He has also coached couples and led conscious relationship workshops together with his partner Holly Croydon, with whom he now lives on 20 acres in the woods in the California Gold Country.

Conal is currently writing a book on how to design scalably reliable and efficient software and hardware with extremely simple specifications and machine-checked correctness, as well as mentoring and collaborating in this general area. For publications, CV, professional blog, etc, see http://conal.net.