Are tests made from formal or informal spec? I saw a project where they where generated from a the formal spec and that never made sense to me.
Is the verification step manual or can it be automated?
If it is manual, we now have 3 things to maintain and keep in sync. The problem of a possible mismatch between informal spec and code has just been moved between the informal and the formal spec. What did we gain?
If the verification step can be automated completely then why write any code at all? Just let it be generated from the spec automatically. If we fold those two steps into one the situation is the same as before; we have a high level description of our problem which a compiler turns into a low level representation that can be executed by a machine. What did we gain?