Ask HN: Why aren't we building a database of formally verified software?

Re:Ask HN: Why aren't we building a database of formally ver... by hirple on Thursday March 04, 2021 @02:43PM (#26347182)

I guess Coq/Lean standard libraries fit this definition.

[ Parent | on HN ]

Re:Ask HN: Why aren't we building a database of formally ver... by cloogshicer on Thursday March 04, 2021 @02:49PM (#26347260)

Exactly, I got this idea from a talk about Lean: https://www.youtube.com/watch?v=Dp-mQ3HxgDE

[ Parent | on HN ]

Re:Ask HN: Why aren't we building a database of formally ver... by seanwilson on Thursday March 04, 2021 @05:17PM (#26349223)

You should look at this like software development. New programming languages come out that try to solve the problems of all the previous languages and unify everyone to code and be productive in the same ecosystem...until another language comes out etc.

It's very hard to get everyone to agree how code plus mathematics should be written. There's a lot of fragmentation and ongoing attempts to unify.

[ Parent | on HN ]