CakeML is a formally verified implementation of a subset of Standard ML which generates native code. Not sure about what it optimises though.