I am curious about how they will define correctness. With many parts in a system, code can look correct in its small unit, but not until it is running in the real world, is it obviously wrong.