3 ms·
This Dafny thing seems absolutely cool. I didn't check the details but a 30 seconds read tells me that if it could generate rust code (it can Java, C, so it's n
by wiz21c 4y ago
This Dafny thing seems absolutely cool. I didn't check the details but a 30 seconds read tells me that if it could generate rust code (it can Java, C, so it's not unbelievable), then we're in for a better world !
- picardo 4y agoDafny's verification system can be too rigorous for high performance and rapidly changing codebases. S3 team had a paper[1] last year on how they verified ShardStore using a lightweight formal verification system. Since the system was written in Rust, they wrote their verifier in Rust, as well. [1] https://assets.amazon.science/07/6c/81bfc2c243249a8b8b65cc2135e4/using-lightweight-formal-methods-to-validate-a-key-value-storage-node-in-amazon-s3.pdf https://assets.amazon.science/07/6c/81bfc2c243249a8b8b65cc21...