Advantages and limits of formal approaches for ultra-high dependability

The paper discusses the advantages and limits of formal approaches to software development for achieving ultra-high dependability of critical computer systems. Among the issues addressed are: what is a formal specification? What can be done with it? What is correctness? What kind of certainty comes from a proof? And from testing? The paper does not claim to answer these questions: rather it is a formulation of the author´s reflections and perplexities in this area