4 ms·

I guess this is as good a place as any, but has anyone used Microsoft's Lean before (http://leanprover.github.io/ http://leanprover.github.io/)? How does it com

by ah312 10y ago

I guess this is as good a place as any, but has anyone used Microsoft's Lean before (http://leanprover.github.io/ http://leanprover.github.io/)? How does it compare to Coq? I'm really interested in getting started with formal verification, but I have a more "engineering" background and don't really know where to start. Coq, Isabelle, Lean... There's quite a few of these tools out there!

pron 10y ago
Most of the tools you mentioned are general theorem provers. They can be used for formal verification of software, but they are mostly research tools. Isabelle is probably the most production quality of those you mention. Industrial-grade formal verification tools -- designed for use by engineers and made to handle larger, more complex software -- include Z, TLA+, B-Method, Why3, SPIN, SCADE. My personal favorite is TLA+. You can start verifying real software in TLA+ in the same amount of time it would take you to get through the first one or two chapters in a book about Coq, and the size and complexity of systems you can affordably specify and verify are larger than you could ever hope to do in Coq. If you absolutely must have end-to-end verification, namely you must verify that global program correctness properties are preserved all the way to the machine code, then you should probably use SCADE if you're writing embedded real-time software; otherwise, consider Isabelle.
- sheepmullet 10y ago
  Have you used Z? How does it compare to TLA+? I'm thinking of trying out TLA+ this holidays to spec a couple of algorithms at work.
  - pron 10y ago
    > Have you used Z? How does it compare to TLA+? I haven't used it but I've seen some examples of it. In many ways it is similar to TLA+, and Lamport says it's a nice, mathematical language. From an aesthetic point of view, it is less elegant: it has many more built-in concepts. From a pragmatic point of view, I think it does not support concurrency at all. Before creating TLA+, Lamport had intended to add TLA to Z for concurrency. This was the result: https://research.microsoft.com/en-us/um/people/lamport/pubs/pubs.html#tlz https://research.microsoft.com/en-us/um/people/lamport/pubs/... Anyway, here's a comparison by Lamport: https://research.microsoft.com/en-us/um/people/lamport/pubs/spec-book-chap.pdf https://research.microsoft.com/en-us/um/people/lamport/pubs/... > I'm thinking of trying out TLA+ this holidays to spec a couple of algorithms at work. Cool. Apart from being very useful, it's a lot of fun.

by ah312 10y ago

pron 10y ago

Most of the tools you mentioned are general theorem provers. They can be used for formal verification of software, but they are mostly research tools. Isabelle is probably the most production quality of those you mention. Industrial-grade formal verification tools -- designed for use by engineers and made to handle larger, more complex software -- include Z, TLA+, B-Method, Why3, SPIN, SCADE. My personal favorite is TLA+. You can start verifying real software in TLA+ in the same amount of time it would take you to get through the first one or two chapters in a book about Coq, and the size and complexity of systems you can affordably specify and verify are larger than you could ever hope to do in Coq. If you absolutely must have end-to-end verification, namely you must verify that global program correctness properties are preserved all the way to the machine code, then you should probably use SCADE if you're writing embedded real-time software; otherwise, consider Isabelle.

sheepmullet 10y ago
Have you used Z? How does it compare to TLA+? I'm thinking of trying out TLA+ this holidays to spec a couple of algorithms at work.
- pron 10y ago
  > Have you used Z? How does it compare to TLA+? I haven't used it but I've seen some examples of it. In many ways it is similar to TLA+, and Lamport says it's a nice, mathematical language. From an aesthetic point of view, it is less elegant: it has many more built-in concepts. From a pragmatic point of view, I think it does not support concurrency at all. Before creating TLA+, Lamport had intended to add TLA to Z for concurrency. This was the result: https://research.microsoft.com/en-us/um/people/lamport/pubs/pubs.html#tlz https://research.microsoft.com/en-us/um/people/lamport/pubs/... Anyway, here's a comparison by Lamport: https://research.microsoft.com/en-us/um/people/lamport/pubs/spec-book-chap.pdf https://research.microsoft.com/en-us/um/people/lamport/pubs/... > I'm thinking of trying out TLA+ this holidays to spec a couple of algorithms at work. Cool. Apart from being very useful, it's a lot of fun.