Timely Computation - A Formal Approach to Digital Circuit Design

Explore a thought-provoking conference talk from ICFP 2023 that delves into the fundamental question of "what is a digital circuit?" in relation to the analog nature of physical circuits. Discover how speaker Conal Elliott presents a simple informal definition and formalizes it using the Agda proof assistant. Learn about the concept of timely embedding of discrete information in continuous signals and how it forms the basis for defining computational circuits. Examine the compositionally correct methodology that maintains specification, implementation, timing, and correctness proofs throughout the circuit design process. Gain insights into the algebraic vocabulary and homomorphisms used to support compositionality. Understand how key transformations reveal the linearity of circuit timing, enabling practical and modular verified timing analysis. Explore the emphasis on simplicity and generality in specifications, minimizing circuit-specific definitions while highlighting a broadly applicable methodology for scalable, compositionally correct engineering through denotations and homomorphisms.