Lambda the Ultimate

On the safety critical mailing list an interesting discussion is taking place, about formal methods. Me, having interest in them, was surprised by the following statement of Nancy Leveson:

Virtually every software-related accident I have heard about in the past 30 years (and I've seen a lot of them) occurred while the software was "performing as specified."

http://www.cs.york.ac.uk/hise/safety-critical-archive/2009/0310.html

(Ariane 5 was not among them, then)

She also writes:

There is a reason that formal methods have not been widely adopted for the past 40 years that academics have been telling practitioners they must use them. Before they are used, the researchers will have to provide:
1. Languages and tools that can be used by a wide range of engineers with only a bachelor's degree. They
cannot be usable only by a small group of Ph.D. mathematicians.
2. Extentions of the techniques to the things they don't cover. Formal methods have been very oversold. They do not handle many of the most important problems.
3. Careful demonstration and experimentation to show that formal methods are less error-prone and more effective than less formal methods for the hardest parts of the problem -- not just the parts that they work best on.

http://www.cs.york.ac.uk/hise/safety-critical-archive/2009/0321.html

and

My students were very fine mathematicians. But they were not pilots or engineers--it required the latter to find the errors my students could not. Formal methods experts cannot and should not be "gurus" outside their field. Most software-related accidents are caused by errors in the requirements specification -- not typos or simple things to find, but misunderstanding basic things about the controlled system and the behavior of the computer. That requires a domain expert, not a mathematician.

http://www.cs.york.ac.uk/hise/safety-critical-archive/2009/0325.html

So the aim is to have formal languages that domain experts do understand. Which of your favourite FM languages stands this test?

Some of them are based on LISP notation which is very compsci-biased. Still, these systems (PVS, ACL2) are used mostly in actual verifications. Isabelle and Coq have more user-friendly notation but it is a question whether these can bridge the gap. Some might call them "cryptic".

What are your favourite languages in this sense?