Programs and proofs: A molecular toolchain

Abstract

Molecular programming is an exciting field that combines techniques from biology, chemistry, and computer science to achieve remarkable results at the molecular scale. Most conventional engineering techniques do not apply apply at nanoscale; to create nanoscale structures, we must often program them to assemble themselves. We identify two challenges in this domain.

First, design complexity: the molecular formalisms that we use to design nanoscale systems are powerful but complex. What abstractions can we create to access this power in a way that is straightforward for humans to understand and reason about? We present ALCH, an imperative language that compiles into the chemical reaction network-controlled tile assembly model.

Second, verification: if we want to use nanotechnological devices in industry and medicine, we must be able to prove that they are safe, and function as expected. In this work, we focus on verification via machine-checkable mathematical proofs; we discuss two efforts to apply this technique to chemical reaction networks (CRNs). In one effort, we incorporate machine-checked proofs into a larger verification process to augment model checking results. In a subsequent effort, we encode CRN semantics from the ground up in a machine-checkable proof language and fully verify a rateless CRN with a population-induced phase transition. We attempt to apply a variety of other verification techniques to this CRN to address the larger question of what role machine-checked proofs have to play in molecular verification.