Coming Soon: Machine-Checked Proofs in Everyday Development

Re:Coming Soon: Machine-Checked Proofs in Everyday Development by skybrian on Saturday December 30, 2017 @10:07PM (#16039121)

What progress has been made recently in making writing proofs easier? Are there any research projects targeting mainstream programmers?

[ Parent | on HN ]

Re:Coming Soon: Machine-Checked Proofs in Everyday Development by slack3r on Sunday December 31, 2017 @05:57AM (#16040138)

Check out Ur/Web (http://www.impredicative.com/ur/).

It has been used by a "mainstream programmer" to build a RSS feed reader.

[ Parent | on HN ]

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 ]