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 whycombagator on Thursday March 04, 2021 @02:45PM (#26347197)

I think the biggest hurdle to a piece of software like this would be what database technology to use. /s

In all seriousness, the idea is very interesting.

I haven’t given this much thought, and maybe I don’t fully understand the proposed idea, but how would you deal with improvements/advancement to already solved things? Like when the fenwick tree was invented

Or how do you deal with competing solutions to a problem like quicksort vs mergesort?

[ Parent | on HN ]

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

Great questions. Well off the top of my head, you could just post multiple solutions to the same problem specification. Just like you can have multiple (valid) answers to the same StackOverflow question.

That's why it would be awesome if you also added performance/memory characteristics to each solution you posted - then you could easily see which one is better for your situation.

Actually, even better - the memory/performance constraints could/should arguably be part of the problem formulation in the first place.

[ Parent | on HN ]