Break

The genetic code is at the center of biological engineering and modifying the genetic code allows us to regulate gene expression to generate biologics or engineer specific proteins. Genomic software facilitates this process by processing large datasets beyond the cognitive abilities of people. However, genomic software is vulnerable to human error during its translation from pseudocode to code. Eliminating bugs is pertinent to keeping the software robust and “correct”. Traditionally, debugging has been done through writing up test cases and quizzing the software to see if it outputs the desired response. We propose a new approach through rigorous, mathematical proof. Test cases are vulnerable to human mistranslation like code, but proofs logically follow from strict axioms embedded within the software.

Lean 4 is a functional programming language that also facilitates computer-checked math proofs. By thinking of the genetic code as a function that maps 4^3 codon sets to 20 amino acids, we can define several properties about itself and prove them. Using Lean 4, we prove the redundancy and non-overlapping nature of the genetic code as a minimal working example for the uses of provable functions to biological engineering.