These MS language developers play for keeps don't they? First Spec#, now F*... But seriously, this is good stuff. I wonder how long it's going to take for this

These MS language developers play for keeps don't they? First Spec#, now F*... But seriously, this is good stuff. I wonder how long it's going to take for this kind of proof-driven code to reach mainstream programmers? Decades I imagine.