<p><a href="https://coq.inria.fr/">Coq</a> is interactive theorem prover, which comes with its own programming language Gallina.</p>
<p>If we wanted to write function that calculates resulting blood type based on two gene alleles, we could do it as following.</p>
<p>Start by defining types that represents alleles and resulting blood type:</p>
<pre><code>Inductive BloodTypeAllele : Type :=
  | BloodTypeA
  | BloodTypeB
  | BloodTypeO.

Inductive BloodType : Type :=
  | TypeA
  | TypeB
  | TypeAB
  | TypeO.</code></pre>
<p>Mapping between them is defined as follows:</p>
<pre><code>Definition bloodType (a b : BloodTypeAllele) : BloodType :=
  match a, b with
  | BloodTypeA, BloodTypeA =&gt; TypeA
  | BloodTypeA, BloodTypeO =&gt; TypeA
  | BloodTypeA, BloodTypeB =&gt; TypeAB
  | BloodTypeB, BloodTypeB =&gt; TypeB
  | BloodTypeB, BloodTypeA =&gt; TypeAB
  | BloodTypeB, BloodTypeO =&gt; TypeB
  | BloodTypeO, BloodTypeA =&gt; TypeA
  | BloodTypeO, BloodTypeB =&gt; TypeB
  | BloodTypeO, BloodTypeO =&gt; TypeO
  end.</code></pre>
<p>Notice that the only way of getting <code>TypeO</code> blood is for both alleles to be <code>BloodTypeO</code>.</p>
<p>We can state theorems about the code:</p>
<pre><code>Theorem double_O_results_O_type :
  bloodType BloodTypeO BloodTypeO = TypeO.
Proof.
  reflexivity.
  Qed.</code></pre>
<p><code>double_O_results_O_type</code> states that <code>bloodType BloodTypeO BloodTypeO</code> will have value of <code>TypeO</code>. There’s also attached proof for this theorem.</p>
<p>Second theorem is longer:</p>
<pre><code>Theorem not_double_O_does_not_result_O_type :
  forall (b1 b2 : BloodTypeAllele),
  b1 &lt;&gt; BloodTypeO \/ b2 &lt;&gt; BloodTypeO -&gt;
  bloodType b1 b2 &lt;&gt; TypeO.
Proof.
  intros.
  destruct b1.
  - destruct b2.
    + discriminate.
    + discriminate.
    + discriminate.
  - destruct b2.
    + discriminate.
    + discriminate.
    + discriminate.
  - destruct b2.
    + discriminate.
    + discriminate.
    + destruct H.
      * simpl. contradiction.
      * simpl. contradiction.
Qed.</code></pre>
<p>It states that if <code>bloodType</code> is applied with anything else than two <code>BloodTypeO</code>, the result will not be <code>TypeO</code>. Proof for this is longer. It goes through each and every combination of parameters and proves that the result isn’t <code>TypeO</code>. Mathematician could write this as: ∀ b1 b2, b1 ≠ BloodTypeO ∨ b2 ≠ BloodTypeO → bloodType b1 b2 ≠ TypeO.</p>
<p>If code above is in module called <code>Genes</code>, we can add following at the end to instruct compiler to emit Haskell code:</p>
<pre><code>Extraction Language Haskell.
Extraction Genes.</code></pre>
<p>Resulting code is as follows:</p>
<pre><code>data BloodTypeAllele =
   BloodTypeA
 | BloodTypeB
 | BloodTypeO

data BloodType =
   TypeA
 | TypeB
 | TypeAB
 | TypeO

bloodType :: BloodTypeAllele -&gt; BloodTypeAllele -&gt; BloodType
bloodType a b =
  case a of {
   BloodTypeA -&gt; case b of {
                  BloodTypeB -&gt; TypeAB;
                  _ -&gt; TypeA};
   BloodTypeB -&gt; case b of {
                  BloodTypeA -&gt; TypeAB;
                  _ -&gt; TypeB};
   BloodTypeO -&gt;
    case b of {
     BloodTypeA -&gt; TypeA;
     BloodTypeB -&gt; TypeB;
     BloodTypeO -&gt; TypeO}}</code></pre>
<p>Now we have Haskell code that started in Coq, has two properties formally verified and is ready to be integrated with rest of the system.</p>
<p>Further reading:</p>
<ul>
<li><a href="https://softwarefoundations.cis.upenn.edu/">Software Foundations</a></li>
<li><a href="https://cel.archives-ouvertes.fr/file/index/docid/459139/filename/coq-hurry.pdf">Coq in a Hurry</a></li>
</ul>
