Formal methods are a means, not an end. To become useful and accepted, computer science theory must be packaged and become invisible. Tool builders need to understand both the formalism and their end-users. Domain-specific tools provide a promising vehicle to deliver theory to practitioners.
Ever higher levels of specification provide increased opportunities for formal methods. Specifications based on constraints can use theorem provers to generate suitable code. Most domains tend to have design rules that can be checked using deductive or model-checking techniques. Domain-specific languages appear to be an effective delivery vehicle for formal methods. This, in turn, should reduce the cost and improve the quality of software.
Maybe domain-specific tools will eventually lead to a new software development paradigm, one where software technology empowers everyone to become a programmer in her field.
While the FCG experience provides only one data point, the existence of commercial tools (e.g. those cited above) is evidence that suggests that automatic code generation is accepted by practitioners. Domain engineers like to be in control rather than having to depend on software engineers.
Today software engineers are expected to play experts in all areas from human-computer interfaces to fluid dynamics to fly-by-wire systems. Software engineers cannot play all these roles and if they do, poor software is a necessity. Instead, software engineers should be tool builders. They are uniquely qualified to make computers accessible to other disciplines and to empower engineers in other fields to express their designs.
We have already seen how spreadsheet programs have made almost every computer user into a programmer. Obviously, not everyone is successful in programming their spreadsheets. But for disciplines where spreadsheets are in common use, their programming has already become part of the standard curriculum. In the long term, engineers in many disciplines will become programmers: domain specific programming will become part of the curriculum and standard practice in their discipline. Given the increasing proliferation of software, this development seems inevitable.
There is a good chance that such a development will also alleviate some of the problems of requirements analysis and capture. Requirements are often the interface between practitioners is different disciplines that speak different languages use different defaults and different common assumptions. If the requirements analyst and the programmer are experts in the same do discipline there is much less change of miscommunication.