3 ms·

- It's like asking why can't we connect together all software ever written so each software problem only needs to be coded once. Ideally you could, but you can'

- It's like asking why can't we connect together all software ever written so each software problem only needs to be coded once. Ideally you could, but you can't. The same way there's different programming languages (with major and subtle differences), different libraries that do similar things, different APIs, different data structures etc. all attempting to improve on something, formal verification has competing languages, logics, tools etc. You can't just take a PHP library and use it as if it was a JavaScript library, the same way you can't take a proof in Isabelle and use it in a Coq proof. - Correctness proofs of even simple algorithms can be research grade problems that take several person years of effort from (hard to find) experts, so you're not likely to get casual Stack Overflow style contributions because of the order of magnitude difference in time and expertise required. - The time required to verify correct software will come at a major cost to other factors like features and speed. I don't think 100% correctness is a driving factor for many domains like web servers, browsers and IDEs, so your database of correct software isn't going to be widely used until it catches up on other factors.

cloogshicer 6y ago
Thank you very much for the answer! Could you elaborate on the last (now first, after edit) point you made? Sorry if the question is naive, I don't know much about this topic. Why can't you do that?
- seanwilson 6y ago
  So picture trying to take a C snippet and using it inside a JavaScript project. On top of the different language syntax, each language has different definitions on equality, strings, arrays, numbers, control flow, pointers etc. so there's no simple mapping that would let you translate the C snippet into a snippet a JavaScript interpreter would understand and if you're not careful with your mapping you're going to get bugs. Similarly with theorem provers, on top of just the syntax, they each have their own definitions for equality, data structures etc. that don't have simple mappings, as well as differences in the basic proof axioms all proofs must be built on. Both specifications and their proofs won't map easily between theorem provers which you'll have to reconcile somehow.
  - cloogshicer 6y ago
    Thanks for the explanation!

cloogshicer 6y ago

Thank you very much for the answer! Could you elaborate on the last (now first, after edit) point you made? Sorry if the question is naive, I don't know much about this topic. Why can't you do that?

seanwilson 6y ago
So picture trying to take a C snippet and using it inside a JavaScript project. On top of the different language syntax, each language has different definitions on equality, strings, arrays, numbers, control flow, pointers etc. so there's no simple mapping that would let you translate the C snippet into a snippet a JavaScript interpreter would understand and if you're not careful with your mapping you're going to get bugs. Similarly with theorem provers, on top of just the syntax, they each have their own definitions for equality, data structures etc. that don't have simple mappings, as well as differences in the basic proof axioms all proofs must be built on. Both specifications and their proofs won't map easily between theorem provers which you'll have to reconcile somehow.
- cloogshicer 6y ago
  Thanks for the explanation!