## OCaml Marrakech STV presentation [Martin Keegan](http://mk.ucant.org/) [@mk270](http://twitter.com/mk270)

## Electronic vote counting in OCaml * Background * Mission * Why OCaml? * [The code](https://github.com/cusu/stv-tools)

## Background * UK votes by paper * Cambridge University internal voting system * particular system: Single Transferable Vote (STV) * OpenSTV * informal verification

## UK voting * elections since 1265, regular since 1295 * government printed ballots since 1880s * majority rule since 1918 * paper counted by hand with scrutiny

## Single Transferrable Vote * rank options in order of preference * multiple vacancies to elect * multiple dialects, informally specified * [BLT files](org-board-2012.blt.txt)

## ERS97 dialect * rounded to fixed-point arithmetic * specified in [reasonable text definition](ers97-extract.txt) * definition lacks separation-of-concerns * invariants can be inferred

## Fauxpen Source system * OpenSTV - taken proprietary in 2011 * archived at https://github.com/OpenTechStrategies/openstv

## Cambridge University voting system * used for various internal elections * not used for formal governance of UofC itself * contains an OpenSTV instance that must be replaced * system has been subject to security analysis

## OCaml * explainable guarantees through types * invariants through opaque types * key constraint is economics of verification

## Restricted subset of OCaml * no ocamllex * no ppx / camlp4 * extremely limited use of mutable state * idiomatic * simplicity conserves verification effort