News for hackers. Stuff that matters.

A comment on Coming Soon: Machine-Checked Proofs in Everyday Development. Parent comment

Re:Coming Soon: Machine-Checked Proofs in Everyday Development by agentultra on Sunday December 31, 2017 @12:19AM (#16039469)
Plenty of advances in logic and category theory have enabled dependently typed languages to be both theorem prover and practical implementation language.

See Lean.

[ Parent | on HN ]
Re:Coming Soon: Machine-Checked Proofs in Everyday Development by vladf on Sunday December 31, 2017 @12:57AM (#16039564)
I'm interested but "Lean programming languages" and its varieties are difficult to Google. Would you mind posting a complete reference?
[ Parent | on HN ]
Re:Coming Soon: Machine-Checked Proofs in Everyday Development by cf on Sunday December 31, 2017 @01:19AM (#16039617)
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

[ Parent | on HN ]
Re:Coming Soon: Machine-Checked Proofs in Everyday Development by agentultra on Sunday December 31, 2017 @09:03AM (#16040574)
Sorry I forgot the link!

https://leanprover.github.io/

[ Parent | on HN ]