A Modern Compiler for the French Tax Code (PDF) (via lobste.rs).

Relevant: Catala is a domain-specific programming language designed for deriving correct-by-construction implementations from legislative texts.