3 ms·
If you see my comment, it proposes using large infosys style teams. You don't need graduates per se, just people who have an intuition for logic and math, of wh
by ampdepolymerase 7y ago
If you see my comment, it proposes using large infosys style teams. You don't need graduates per se, just people who have an intuition for logic and math, of which there are plenty. Plus you can prove isolated pieces e.g. TCP/IP stacks instead of end-to-end. It would not be as beneficial as full formal verification but it is still a large step in securing the most vulnerable targets such as IoT, industrial control systems, financial services etc.
- pron 7y agoThe problem is that the training required for "proof monkeys" is higher than for programmers, so they'll be even more expensive (plus you need to know the specified C semantics to prove C code, something even many/most C programmers don't know), and second, the proving effort is not something that can usually be done separately and after-the-fact. The program needs to be written in a way informed by the proving effort. Moreover, every time the program is changed, the amount of proof that needs to be rewritten could be large, especially if the programmers are unfamiliar with the proofs. Hopefully, there are more efficient formal methods than the one that is currently the least efficient of them all.