Optimizing the SW development algorithm

Warning: this article contains simplifications so read on with care :)

This is a sketch of an algorithm for the test driven sw development process:

while not client.isHappy()
  specification = client.writeSpecification()
  if specification.isExecutable()
    executableSpecification = specification
  else
    executableSpecification =  programmer.formalize(specification)
    // executableSpecification must be readable by client
    client.verify(executableSpecification)

  if productionSystem.canExecute(executableSpecification)
    productionSystem.add(executableSpecification)
  else
    allTests.add(executableSpecification)

    while not testFramework.doAllTestsPass(allTests)
      productionSystem = programmer.code(productionSystem, allTests)

How could this process be optimized? Here are some suggestions, from the easiest to the most difficult:

Introduce an executable language for expressing specifications by example. Now the programmer isn't needed to write the specification, and the client doesn't need to verify his/her own creation:

while not client.isHappy()
  executableSpecification = client.writeSpecification()

  if productionSystem.canExecute(executableSpecification)
    productionSystem.add(executableSpecification)
  else
    allTests.add(executableSpecification)

    while not testFramework.doAllTestsPass(allTests)
      productionSystem = programmer.code(productionSystem, allTests)

If the problem happens to be one of those that are difficult to specify formally, this is the best we can do. Otherwise, we have a formal and executable specification, so the production system can use the specification as such:

while not client.isHappy()
  executableSpecification = client.writeSpecification()
  productionSystem.add(executableSpecification)

Whoops:

Warning: unused variable: programmer