Somewhat, yes. A specification framework is there to help bridge the semantic gap between what you are trying to achieve in the real world and the world of bit

Somewhat, yes. A specification framework is there to help bridge the semantic gap between what you are trying to achieve in the real world and the world of bit-banging if you will. And even if you forget a part of a specification (like saying a sorting function needs to leave behind a sorted collection but forgetting to mention that the input and output collection need to contain the exact same elements or that the input collection needs to be finite for the function to terminate), you'll still have a notion of "incremental correctness". That's why I added in the part with what specifying "cryptographic strength" would mean (e.g.: strong against what exactly?). You could leave that or time-critical properties (e.g.: this function encrypts x bits in y seconds) out and retain the notion of "functional correctness" (i.e. the ciphertext always corresponds to what the definition says it should be). When you're writing code you'll (most of the time :)) have an idea of what you're trying to achieve. Formal specification should enable you to write that down in convenient form.