mikedodds

3 ms·

1.
by mikedodds 4y ago
I love Dafny - we've worked on it in the past in fact. Theorem proving is definitely something that's being applied in industry - our crypto verification project uses Coq in some places. There's definitely a lot of hype thoug
2.
by mikedodds 4y ago
Great question! Formal methods groups in industry are growing rapidly and popping up in surprising places. Amazon's group is probably the most famous, but I think pretty much every big tech company has something going on in the formal
3.
by mikedodds 4y ago
Our approach for cryptographic systems is pretty much gradual verification. We target high risk or worrisome systems and verify piece by piece. It works! Formal verification is a relatively expensive technique so it's necessary (in my
4.
by mikedodds 4y ago
I'm the author of this article. I'd be happy to answer questions if anyone has them.
5.
by mikedodds 6y ago
Author here. If anyone isn't familiar with Galois, we're a consultancy that does a lot of formal methods and proof, which is why it would be great if proofs were easier to manage :) If you're curious, you can get a sense of w
6.
by mikedodds 6y ago
I don't know if there are proofs unsuited to human minds, but for machine proofs, there's no essential difference between what a proof assistant like Coq can do, and what a human brain can do. Ultimately Coq boils down to a very s
7.
by mikedodds 6y ago
This is a great question, and unfortunately the existing proof tools are very fragmented when it comes to target languages. E.g. there are a lot of C / LLVM and Java tools, a few C++ tools, a few Rust tools. I don't know of any pr
8.
by mikedodds 6y ago
Author here. This post is definitely more of a problem statement than a solution. I don't think this area gets enough attention and I'd like more people to think about it! However, I think there are some good reasons to think solv