If we could define our software in a precise, clear way, it may be possible to take that definition and transform it, over a series of steps, into the actual program. This turns out to be remarkably similar to what a compiler does--and compilers can, in theory, be demonstrated as correct.
This technique is sometimes called transformational specification. Its challenge: That precise definition will need to be interpreted by some sort of program. In order to make the specification precise, it needs to be written in code, and that code will probably have errors.
As an academic discipline, the formal specification for finding the largest element in an array of integers requires roughly 600 small transformations, expressed in predicate calculus. That is complex enough that a graduate student in computer science might write a transform to, say, add up the change in your pocket or sort and count it, but it can't be used for practical software development.
Behavior-Driven Development: Code That Looks Like English
Like transformational specification, behavior driven development (BDD) also separates the spec from the code. Like its older cousin, BDD begins by writing examples of what the software will do in high-level language that looks more like English than most traditional code.
Here's an example in Given/When/Then format:
Given a logged-in user
When I add item 12345 into my shopping cart
And I click order
Then I see the order screen with item 12345
To implement this, the transformational program would need to know what the shopping cart is, what logged in means, what the order button is and so on. These types of Given/When/Then statements can be very valuable and can be compiled, with a human coming along afterward to define the keywords "shopping cart," "logged in" and so on.
These examples (but not a programmatic spec), defined up front, mean the programmer can know that, if he delivers the code to acceptance test and it meets some minimum standards of quality, then the code can "work" under precise condition. In some cases, the checks can run automatically with every build, so the build system can find some major regression errors immediately after commit.
Model-Based Testing: Intelligent Automation for Big, Obvious Errors