Coq is interactive theorem prover, which comes with its own programming language Gallina.
If we wanted to write function that calculates resulting blood type based on two gene alleles, we could do it as following.
Start by defining types that represents alleles and resulting blood type:
Inductive BloodTypeAllele : Type :=
| BloodTypeA
|...