TIL there's a proven-correct compiler for standard ML! https://cakeml.org/ This is an incredible feat, and uses validated ISA models.