mikedodds · HackerTrans

il y a 4 ansdiscuss

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 though, some of which seems a bit unrealistic to me. There's a long, long way to go before theorem proving is practical as a tool for general programming, rather than in ultra-important niches like core crypto libraries.

mikedodds

il y a 4 ansdiscuss

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 verification / static analysis space. There's also a lot going on in blockchain. It's definitely becoming harder to hire people with FM skills, so in that sense, I think it's a great space to get into.

The downside is that the space is quite fragmented and a lot of tools have a high skill bar. If I was starting out, I'd probably focus on static analysis (eg. Infer or something similar - https://github.com/facebook/infer) because those tools tend to be easier to learn, and they have the potential to scale to really big systems. In contrast, Coq is a fine tool, but most people learn it by going to grad school which isn't useful short term career advice.

There are lot of great interviews with practitioners on the Galois podcast, Building Better Systems - that might be a good place to start exploring: https://www.stitcher.com/show/building-better-systems

mikedodds

il y a 4 ansdiscuss

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 opinion) to target the places where you can achieve the best bang for buck.

For system reliability at scale, I think that stronger type systems and systematic testing techniques are probably the best choice. Anyway, that puts the system in a much better state if you want to apply formal verification later.

mikedodds

il y a 4 ansdiscuss

I'm the author of this article. I'd be happy to answer questions if anyone has them.

mikedodds

il y a 5 ansdiscuss

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 what we do here: https://galois.com/blog/2021/02/2020-year-in-review/

The tool we use most often for proofs is called SAW: https://saw.galois.com/

mikedodds

il y a 5 ansdiscuss

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 simple core logic that could (in principle) be checked by a human. But the sheer scale of such proofs means they can't be meticulously checked. Proof tools are just the same as e.g. compilers - they can do things humans can't do because to do so would be so incredibly time consuming and tedious.

mikedodds

il y a 5 ansdiscuss

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 proof tool that is production-ready that targets Go, Swift, and Kotlin.

One thing I will say is that proof is usually an expensive technique, and not just for the reasons in my post. Even setting up a proof can be demanding. So it's worth asking where in the project it's worth applying this kind of assurance? For example, Galois often applied proofs to cryptography, which are security critical and self-contained in small pieces of code. Proof and formal methods aren't one tool, but rather a toolbox that can solve different assurance problems. There's a big difference from a scalable static analysis like Infer and a fine-grained proof tool like Coq or Galois' SAW tool.

One easy place that formal methods can be useful is in modeling features of a project design for consistency. E.g. this is useful for protocols, state machines and similar. This means you can 'debug your designs' before building them into software. If that sounds like it might useful, I would suggest taking a look at Hillel Wayne's website: https://www.hillelwayne.com

mikedodds

il y a 5 ansdiscuss

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 solving this is possible. E.g. Galois have had proofs in CI at AWS for several years that rerun on code changes - you can read about our approach here: https://link.springer.com/chapter/10.1007/978-3-319-96142-2_.... And elsewhere in the comments Talia Ringer posted about her research, which is very promising as well.

I think there's a tight connection between 'proofs the programmer can understand' and self-repair / automation. The aim should really be to clear away a lot of the scaffolding that's currently needed and hand it off to solvers, and leave programmers to do what they are best at, i.e. understand the meaning of the code. Type checking is a great example of a lightweight formal method that disguises most of the sophisticated automation hiding behind the scenes.