[ihm]

I think it is an exciting time for functional programming and formal methods: they seem to have found something of a home in the recent cryptocurrency boom, where people are recognizing that high-assurance really matters lest you lose millions of dollars.

Why people don't seem to worry as much about self-driving cars boggles the mind. One hopes the loss of human life would be as concerning as the loss of money. I think the issue is partly technological. As Leroy says, formal methods for certifying machine learning-produced models are pretty undeveloped whereas cryptocurrency protocols are 'traditional', 'algorithmic' programs and so more amenable to analysis with existing verification tools. I also think it is partly cultural in that machine learning practitioners seem often to be less aware of formal methods and the possibility of verifying software.

[haskellandchill]

I don’t see many options career wise however, I invested heavily in formal methods but I think it’s time for me to pivot to machine learning and data science to have higher paying job opportunities in NYC. I still believe it will have a major moment in the future and Proof Engineer will be a thing.

[auggierose]

Proof engineer is a thing. It's just that there are only a handful of them :)

[bagnalla]

Verification of machine learning models, especially w.r.t. robustness to so-called "adversarial examples" [1], is a major research topic at the moment. There are certainly people worrying about it in the machine learning community, but it appears to be a very difficult problem.

[1] https://arxiv.org/abs/1312.6199