This is a talk about how we can generate single transferable votes counting code from a logical specification automatically using advanced computer aided verification methods.
It is based upon a PhD dissertation but I think I made it non-technical.
I will first explain single transferable vote counting and the parlous state of computer-counting code implemented by various Election Commissions from around Australia. I will then explain how we used Coq to specify a "vanilla" version of single transferable voting as a proof-calculus and used it to extract a computer program which not only counts votes according to this specification but also produces a certificate during the count. The specification of the certificate is derived from the counting rules. We have proved, in Coq, that if the certificate is correct with respect to its specification, then the result it encapsulates must be correct with respect to the relevant specification of single transferable voting. The certificate is designed so that an average third-year computer science student could write a computer program to check the correctness of the certificate.