Formal methods have a great way of forcing people to think about the properties they expect of their systems. While there’s obviously value in proofs and model checking, in my experience the biggest benefit to me has been clarity around requirements.

Well, I found learning coq a really big investment (time and mental-wise)… I tried twice and left a bit frustrated, the simpler proofs are really simple, the harder ones are really hard. I wouldn’t dismiss the fact that it may be just too hard for me to grasp though.

However, if you like software verification, but find the proving process boring, there’s always the subject of SMTs (Z3, CVC4), automated theorem provers (ACL2) and such (coq is rather a proof assistant, you need to do the proof manually). You don’t need to learn coq to have fun with software verification!

[EDIT]

I forgot to mention Idris, which aims to be a sort of “usable coq”.

In my limited use of it (mostly limited to a grad course taken some years ago), I found ACL2 more towards the proof-assistant side of things also. It does have some automated theorem proving, but it only succeeds fully automatically for very simple things. For anything non-trivial (not even meaning big Real Software, even simple algorithms-textbook algorithms) you have to hand-hold the prover quite a bit, which requires digging into the details of the proving process. A lot of getting a proof to “go through” consists of strategically giving it rewrite rules, induction schemes, etc. The people who are really good with ACL2 seem to have a lot of black-art type knowledge of it.

Fabrice, thanks for the reply - this is the sort of overview I was looking for.

I have some experience with Haskell - read a lot of papers & code but have only written toys. I’ve seen Idris around and algebraic effects are definitely intriguing.

From the sounds of it, Coq isn’t quite what I’m really looking for. I might try out some of those really simple proofs you’re talking about to get a feel for it and then move onto learning more about SMT and Idris.

Software verification is definitely the goal, for me :)

Depending on what you mean by “software verification”, you should also look at TLA+ and Promela/Spin. They aim at a different space from Coq, but in my experience tend to be better at the set of things that many working coders find useful.

[Comment removed by author]

Formal methods have a great way of forcing people to think about the properties they expect of their systems. While there’s obviously value in proofs and model checking, in my experience the biggest benefit to me has been clarity around requirements.

This is the most interesting thing I’ve seen in a while. I wonder if my time is better invested in learning Coq than Haskell..

Well, I found learning coq a really big investment (time and mental-wise)… I tried twice and left a bit frustrated, the simpler proofs are really simple, the harder ones are really hard. I wouldn’t dismiss the fact that it may be just too hard for me to grasp though.

If you want to learn programming-language-theory oriented coq there’s a

de factostarting point: http://www.cis.upenn.edu/~bcpierce/sf/current/index.html and you may continue with http://adam.chlipala.net/cpdt/However, if you like software verification, but find the proving process boring, there’s always the subject of SMTs (Z3, CVC4), automated theorem provers (ACL2) and such (coq is rather a proof assistant, you need to do the proof manually). You don’t need to learn coq to have fun with software verification!

[EDIT]

I forgot to mention Idris, which aims to be a sort of “usable coq”.

In my limited use of it (mostly limited to a grad course taken some years ago), I found ACL2 more towards the proof-assistant side of things also. It does have some automated theorem proving, but it only succeeds fully automatically for

verysimple things. For anything non-trivial (not even meaning big Real Software, even simple algorithms-textbook algorithms) you have to hand-hold the prover quite a bit, which requires digging into the details of the proving process. A lot of getting a proof to “go through” consists of strategically giving it rewrite rules, induction schemes, etc. The people who are really good with ACL2 seem to have a lot of black-art type knowledge of it.Fabrice, thanks for the reply - this is the sort of overview I was looking for.

I have some experience with Haskell - read a lot of papers & code but have only written toys. I’ve seen Idris around and algebraic effects are definitely intriguing.

From the sounds of it, Coq isn’t quite what I’m really looking for. I might try out some of those really simple proofs you’re talking about to get a feel for it and then move onto learning more about SMT and Idris.

Software verification is definitely the goal, for me :)

Depending on what you mean by “software verification”, you should also look at TLA+ and Promela/Spin. They aim at a different space from Coq, but in my experience tend to be better at the set of things that many working coders find useful.

Thanks, I’ve toyed around with TLA+ and have started digging into the book. Haven’t heard of Promela/Spin - will take a look.

[Comment removed by author]

Thanks. I’ve got some Haskell & ML experience. I don’t mind cliffs :)