If you have been trained in the use of formal methods (FM) for programming:
- How useful have you found it?
- What did your FM training involve (e.g. a course, a book)?
- What FM tools do you use?
- What advantages in speed/quality has it given you compared to not using FM?
- What kind of software do you create with FM?
- And if you don't directly use FM now, was it at least worth learning??
I'm curious to hear as many experiences/opinions on FM as can be found in this community; I'm starting to read up on it and want to know more.
Programming and software development/engineering are some of the newest human skills/professions on Earth, so not surprisingly, the field is immature — that shows in our field's main output, as code that is typically late and error-prone. Industry immaturity is also shown by the wide margin (at least 10:1) in productivity between average and top coders. Such dismal facts are well covered in the literature, and introduced by books like Steve McConnell's Code Complete.
The use of formal methods (FM) has been proposed by major figures in software/CS (e.g. the late E. Dijkstra) to address (one of) the root causes of errors: the lack of mathematical rigour in programming. Dijkstra, for instance, advocated for students developing a program and its proof together.
FM seems to be much more prevalent in CS curricula in Europe compared to the US. But in the past few years, new "lightweight" FM approaches and tools like Alloy have attracted some attention. Still, FM is far from common usage in industry, and I'm hoping for some feedback here on why.
As of now (10/14/2010), of the 6 answers below, no one has clearly argued for the usage of FM in "real world" work. I'm really curious if someone can and will; or perhaps FM really does illustrate the divide between academia (FM is the future!) and industry (FM is mostly useless).