5 ms·

Has anything actually useful ever come out of this field of enquiry? To me it always seems like excessive formalism for its own sake without a useful real-worl

Has anything actually useful ever come out of this field of enquiry? To me it always seems like excessive formalism for its own sake without a useful real-world outcome. Would be happy to be wrong about this.

accurrent 5y ago
Not an expert but I've heard formal methods are used in Chip Design. Also https://compcert.org/ https://compcert.org/ a c compiler which uses formal verifcation. I tried some exercises in the series. Its pretty interesting thing to do (but very difficult to master), but yes I don't think its great for rapid software development. On the other hand for very very critical infrastructure or the case where you need your code to be right from the start (chip design, security protocols, etc.) it makes sense.
riedel 5y ago
What do you mean by field of enquiry? Formal verification has it's success stories, like seL4 (https://sel4.systems/ https://sel4.systems/). This series seems rather educational and seems to give you coq proofs for algorithms. I guess it depends on your needs and domain if you need to bother.
zozbot234 5y ago
The Rust borrow checker implements what amounts to a simplified application of separation logic (the topic of the latest volume in this series), and there's ongoing work to further extend its applicability so that, e.g. generic data structure implementations might be written in a verifiably safe manner. If you've ever written or otherwise relied on Rust software, you have indirectly used this work.
k__ 5y ago
As far as I know, formal methods are used in system design. AWS build some of it's services with their help.
BreakfastB0b 5y ago
Yes! Formally verified implementations of Elliptic Curve algorithms http://adam.chlipala.net/theses/andreser_meng.pdf http://adam.chlipala.net/theses/andreser_meng.pdf. Amazon has also made use of TLA+ and lightweight formal methods to prove the correctness of their distributed services such as S3 and DynamoDB which arguably underpin a large portion of the internet https://www.amazon.science/publications/how-amazon-web-services-uses-formal-methods https://www.amazon.science/publications/how-amazon-web-servi... The burden of using these extreme approaches is high, but there are definitely circumstances where it is warranted. Think of it as TDD on steroids.
danielam 5y ago
Apart from the intellectual clarity, you don't need to employ all of the tools in this text to benefit practically from some use of formal verification, etc. If you're using a statically typed language, you're likely already benefiting from at least some degree of verification. Your types encode your specification. One example close to home for me and from industry is a dependently typed language we are working on at my company that's used to encode validations and transformations for transaction reporting (other teams have also begun to use the language for other uses). Consistency is ensured by the type checker and the compiler subsequently generates the aforementioned transformation and validation functions that are used in production. This is admittedly a very niche application, but as I've already written, the use of static analysis admits a range of rigor—it's not either/or—so it's a question of determining the appropriate degree of formality for your particular case.
amw-zero 5y ago
The seL4 microkernel: https://sel4.systems/ https://sel4.systems/ The CompCert C compiler: https://compcert.org/ https://compcert.org/ TLS implementation in Firefox: https://blog.mozilla.org/security/2020/07/06/performance-improvements-via-formally-verified-cryptography-in-firefox/ https://blog.mozilla.org/security/2020/07/06/performance-imp... Elasticsearch model checks some of their core algorithms with TLA+: https://youtu.be/qYDcbcOVurc https://youtu.be/qYDcbcOVurc. Amazon is known to apply formal methods in varying forms to services like S3: https://www.amazon.science/publications/using-lightweight-formal-methods-to-validate-a-key-value-storage-node-in-amazon-s3 https://www.amazon.science/publications/using-lightweight-fo... Many components in airplane software is formally verified in some aspect.

accurrent 5y ago

Not an expert but I've heard formal methods are used in Chip Design. Also https://compcert.org/ https://compcert.org/ a c compiler which uses formal verifcation. I tried some exercises in the series. Its pretty interesting thing to do (but very difficult to master), but yes I don't think its great for rapid software development. On the other hand for very very critical infrastructure or the case where you need your code to be right from the start (chip design, security protocols, etc.) it makes sense.

riedel 5y ago

What do you mean by field of enquiry? Formal verification has it's success stories, like seL4 (https://sel4.systems/ https://sel4.systems/). This series seems rather educational and seems to give you coq proofs for algorithms. I guess it depends on your needs and domain if you need to bother.

zozbot234 5y ago

The Rust borrow checker implements what amounts to a simplified application of separation logic (the topic of the latest volume in this series), and there's ongoing work to further extend its applicability so that, e.g. generic data structure implementations might be written in a verifiably safe manner. If you've ever written or otherwise relied on Rust software, you have indirectly used this work.

k__ 5y ago

As far as I know, formal methods are used in system design. AWS build some of it's services with their help.

BreakfastB0b 5y ago

Yes! Formally verified implementations of Elliptic Curve algorithms http://adam.chlipala.net/theses/andreser_meng.pdf http://adam.chlipala.net/theses/andreser_meng.pdf. Amazon has also made use of TLA+ and lightweight formal methods to prove the correctness of their distributed services such as S3 and DynamoDB which arguably underpin a large portion of the internet https://www.amazon.science/publications/how-amazon-web-services-uses-formal-methods https://www.amazon.science/publications/how-amazon-web-servi... The burden of using these extreme approaches is high, but there are definitely circumstances where it is warranted. Think of it as TDD on steroids.

danielam 5y ago

Apart from the intellectual clarity, you don't need to employ all of the tools in this text to benefit practically from some use of formal verification, etc. If you're using a statically typed language, you're likely already benefiting from at least some degree of verification. Your types encode your specification. One example close to home for me and from industry is a dependently typed language we are working on at my company that's used to encode validations and transformations for transaction reporting (other teams have also begun to use the language for other uses). Consistency is ensured by the type checker and the compiler subsequently generates the aforementioned transformation and validation functions that are used in production. This is admittedly a very niche application, but as I've already written, the use of static analysis admits a range of rigor—it's not either/or—so it's a question of determining the appropriate degree of formality for your particular case.

amw-zero 5y ago

The seL4 microkernel: https://sel4.systems/ https://sel4.systems/ The CompCert C compiler: https://compcert.org/ https://compcert.org/ TLS implementation in Firefox: https://blog.mozilla.org/security/2020/07/06/performance-improvements-via-formally-verified-cryptography-in-firefox/ https://blog.mozilla.org/security/2020/07/06/performance-imp... Elasticsearch model checks some of their core algorithms with TLA+: https://youtu.be/qYDcbcOVurc https://youtu.be/qYDcbcOVurc. Amazon is known to apply formal methods in varying forms to services like S3: https://www.amazon.science/publications/using-lightweight-formal-methods-to-validate-a-key-value-storage-node-in-amazon-s3 https://www.amazon.science/publications/using-lightweight-fo... Many components in airplane software is formally verified in some aspect.