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.
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.
> 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.
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.
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.
--------------
[1] https://aws.amazon.com/blogs/security/protect-sensitive-data... [2] https://github.com/dafny-lang/dafny