A provable language that can translate directly to OCaml, F#, C, WebAssembly, or VALE sounds lovely if it's not too painful to use. I hope the C translations follow CERT / MISRA. It would be a shame to prove the program correct then have a translation of it that's buggy. I'll have to read more about this later.
I have started looking into it for the same reasons. So far it feels like programming in F# but with nice tasty refinement types added. So fairly straightforward.