It has been used by a "mainstream programmer" to build a RSS feed reader.
Plenty of advances in logic and category theory have enabled dependently typed languages to be both theorem prover and practical implementation language.
See Lean.
I'm interested but "Lean programming languages" and its varieties are difficult to Google. Would you mind posting a complete reference?
I think this is a good application paper for Lean showing how you can use it to develop machine learning algorithms.