Re: [TYPES] "Proofs of life"

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

I should have mentioned earlier that there's an accompanying video, with 
proof visualization and more:

	http://ceqea.sourceforge.net/extras/instructionalPoL.mp4


On 11/7/18 10:37 AM, Rene Vestergaard wrote:
> "Proofs of life: molecular-biology reasoning simulates cell behaviors 
> from first principles" is now available at http://arxiv.org/abs/1811.02478
> 
> The work springs from computer-verified reasoning and establishes wider 
> utility by means of a reasoning-computation correspondence, including 
> for long-standing critical problems in biology that have defied standard 
> approaches.
> 
> Sincerely,
> Rene
> 
> -----
> 
> ESSENCE
> Mathematics-style correctness works for molecular biology and enables 
> phenotype and life-cycle prediction from genotypes. Formally, 
> reductionist science involves constructive reasoning, i.e., executable 
> simulation.
> 
> SIGNIFICANCE
> Axiomatic reasoning provides an alternative perspective that allows us 
> to address long-standing open problems in biology. Our approach is 
> supported by meta-theory and likely applies to any reductionist discipline.
> 
> ABSTRACT
> Science relies on external correctness: statistical analysis and 
> reproducibility, with ready applicability but inherent false 
> positives/negatives. Mathematics uses internal correctness: conclusions 
> must be established by detailed reasoning, with high confidence and deep 
> insights but not necessarily real-world significance. Here, we formalize 
> the molecular-biology reasoning style; establish that it constitutes an 
> executable first-principle theory of cell behaviors that admits 
> predictive technologies, with a range of correctness guarantees; and 
> show that we can fully account for the standard reference: Ptashne, A 
> Genetic Switch. Everything works for principled reasons and is presented 
> within an open-ended meta-theoretic framework that seemingly applies to 
> any reductionist discipline. The framework is adapted from a 
> century-long line of work on mathematical reasoning. The key step is to 
> not admit reasoning based on an external notion of truth but work only 
> with what can be justified from considered assumptions. For molecular 
> biology, the induced theory involves the concurrent running/interference 
> of molecule-coded elementary processes of physiology change over the 
> genome. The life cycle of the single-celled monograph organism is 
> predicted in molecular detail as the aggregate of the possible 
> sequentializations of the coded-for processes. The difficult question of 
> molecular coding, i.e., the specific means of gene regulation, is 
> addressed via a detailed modeling methodology. We establish a 
> complementary perspective on science, complete with a proven correctness 
> notion, and use it to make progress on long-standing and critical open 
> problems in biology.