4 ms·
Perhaps because formal verification is hard & very expensive? For starters, where does an open source project come up with an entire compute farm...
by sliverstorm 13y ago
Perhaps because formal verification is hard & very expensive?
For starters, where does an open source project come up with an entire compute farm...
- betterunix 13y agoYou can do formal verification with tools like Coq using a laptop. The real issue is that writing a formal specification is hard even for small problems; writing a formal spec for something like TLS would be harder than actually implementing TLS.
- sliverstorm 13y agoCool! I do hardware, I guess software is probably easier to compute.
- betterunix 13y agoAh, you might have been thinking of techniques basic on SAT and ATPG solving. What makes software different is this: https://en.wikipedia.org/wiki/Curry-Howard_Correspondence https://en.wikipedia.org/wiki/Curry-Howard_Correspondence Basically, checking a proof of correctness for software is equivalent to type checking (for a very fancy type system).