Automated Reasoning at Amazon: A Conversation | Hacker News Reader

Automated Reasoning at Amazon: A Conversation

amazon.science

96 pointskelsier111 comments

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

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 !

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...

I thought FLoC was Google's Federated Labeling of Cohorts? This is too much acronym overloading for me.

I wonder which came first.

This one -- its first occurrence was in '96, several years before Google-the-company was founded.

https://www.floc2022.org/history

> I’m particularly excited to meet the new generation of scientists who have entered the field, to see the world afresh through their eyes. This is such an amazing time to be in the field of automated reasoning.

Indeed

I wasn't familiar with this area, and it's so cool to hear about Moore's law progress on solving SAT, and how SAT is like the drosophila model. To me "automated reasoning" brings to mind reasoning with large language models.

What is the link to the drosophila model?

Apologies if it's obvious, I just started looking at SAT solvers so I'm relatively ignorant on the area.

I loosely mean how drosophila in biology is a relatively simple yet representative model that is easy to study that yields some insights about other systems.

Funny, automated reasoning was to AI, in the good old fashioned days, what deep learning is today, in terms of perceived significance and hype.

Is there any field that isn't being hoovered up by AWS?

Reply on news.ycombinator.com