Quality: Making better software

It is often feared that software produced with the aid of an automated tool must suffer in efficiency or other measures of quality. In fact, the automation of software production can result in software that is superior to what can be produced by hand. For example, some of the software produced by KIDS, the predecessor of Specware, has been orders of magnitude faster than the best software for the same task produced by conventional methods. An automated tool can apply sophisticated transformations that may obscure the clarity of the code but improve its performance while preserving its correctness--guaranteed--in the same way that register allocation and general compiler optimization is typically done better by machine.