Hacker News 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.

View on HN

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.

https://arxiv.org/abs/1706.08605

Sorry I forgot the link!

https://leanprover.github.io/

Reply on news.ycombinator.com