A formally verified compiler for a simple language with numbers and sums - View it on GitHub