A new, nondeterministic floating-point source semantics and a proof-of-concept connection to the CakeML verified compiler.