Automated Reasoning at Amazon: A Conversation

Re:Automated Reasoning at Amazon: A Conversation by picardo on Monday August 08, 2022 @05:39PM (#32391394)

The hype is well-deserved. The Automated Reasoning Group is doing some remarkable things. Zelkova[1] is making policy compliance a breeze. And the institutional support for Dafny[2] -- a verification aware programming language -- is bringing program verification to the masses. Really envious of them.

--------------

[1] https://aws.amazon.com/blogs/security/protect-sensitive-data... [2] https://github.com/dafny-lang/dafny

[ Parent | on HN ]

Re:Automated Reasoning at Amazon: A Conversation by wiz21c on Tuesday August 09, 2022 @05:07AM (#32395676)

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 !

[ Parent | on HN ]

Re:Automated Reasoning at Amazon: A Conversation by picardo on Tuesday August 09, 2022 @09:12AM (#32397331)

Dafny'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/81bfc2c243249a8b8b65cc21...

[ Parent | on HN ]