3 ms·
I'm fond of formal methods, but I'll offer the usual counter-example: Formal methods struggle to scale up to real-world problems. There is no formally verified
by MaxBarraclough 5y ago
I'm fond of formal methods, but I'll offer the usual counter-example:
Formal methods struggle to scale up to real-world problems. There is no formally verified TCP/IP stack. There is no formally verified TLS or SSH implementation. That's despite how immensely useful and reusable such implementations could be (that is to say, high demand, and yet no supply).
As I understand it we're not even close to being able to develop a formally verified TLS implementation, but if we were, it would likely take the form of an internationally acclaimed PhD thesis, akin to CompCert. It still wouldn't mean formal methods are cheap and easy.
- TheOtherHobbes 5y agoIt's astounding that core security infrastructure isn't formally designed and certified, and isn't available as standardised - certified - drop-in elements. A top decile PhD thesis is not a high bar in engineering. It's how most disciplines evolve. "Not invented here" is not a credible explanation for why CS feels a need to be different.