  We axiomatize the molecular-biology reasoning style, show compliance of the
standard reference: Ptashne, A Genetic Switch, and present proof-theory-induced
technologies to help infer phenotypes and to predict life cycles from
genotypes. The key is to note that `reductionist discipline' entails
constructive reasoning: any proof of a compound property can be decomposed to
proofs of constituent properties. Proof theory makes explicit the inner
structure of the axiomatized reasoning style and allows the permissible
dynamics to be presented as a mode of computation that can be executed and
analyzed. Constructivity and execution guarantee simulation when working over
domain-specific languages. Here, we exhibit phenotype properties for genotype
reasons: a molecular-biology argument is an open-system concurrent computation
that results in compartment changes and is performed among processes of
physiology change as determined from the molecular programming of given DNA.
Life cycles are the possible sequentializations of the processes. A main
implication of our construction is that formal correctness provides a
complementary perspective on science that is as fundamental there as for pure
mathematics. The bulk of the presented work has been verified formally correct
by computer.
