What I need is the proof that the program is correct. Bugs will show up as gaps or inconsistencies in the proof. But, in the absence of even an attempt at a proof, all I can do is throw the program to the dogs.
I've never yet had the luxury of working in a language that admitted formal proofs of correctness. Do you mean informal "proofs" like unit tests?
When a bug occurs (perhaps because your tests did not anticipate every edge case) how do you determine where the problem code is located without a stack trace?
I know that it doesn't usually point to the line of code that is problematic, but it usually gives you a starting point for your deductions...
> I've never yet had the luxury of working in a language that admitted formal proofs of correctness.
You don't need much from your language, except for a formal semantics. But, even if your language of choice doesn't have one, you can stick to a subset of it that is easy to formalize: no first-class procedures (or things that can simulate them, such as dynamic method dispatch), no non-local control flow operators (e.g. raising and handling exceptions), no non-lexical variables, just statically dispatched procedures and structured control flow constructs (selection and repetition, i.e., pattern matching and recursion).
> When a bug occurs (perhaps because your tests did not anticipate every edge case) how do you determine where the problem code is located without a stack trace?
By reasoning about every statement's intended and actual preconditions and postconditions, i.e., predicates on the program's free variables. At some point, the intended and actual preconditions of a statement-postcondition pair won't agree. But this is unreasonably hard if you need to reconstruct these preconditions and postconditions completely from scratch.
It seems pretty useless to even try to formally verify a program when all of the dependencies that are necessary to do anything useful are not formally verified. Where do I find a formally verified TCP/IP stack, a formally verified database, a formally verified HTML/CSS renderer, etc.?
I've found unit tests for system libraries like this before. The idea is that you run them each time you upgrade your framework, but in practise you run them every time (slowing down your debug loop) and managers use them to inflate the effectiveness of your actual tests, which is obviously measured in "number of unit tests" rather than %coverage (or, better still, %possible input values to each line)
Sorry, I proposed unit testing as a real-world formalisation of requirements in an earlier post, and you didn't contradict me. What automated system would you use for this instead?
Automated, huh? There is no replacement for using your brain, and reasoning abstractly about the preconditions and postconditions of program fragments.
When a bug occurs (perhaps because your tests did not anticipate every edge case) how do you determine where the problem code is located without a stack trace?
I know that it doesn't usually point to the line of code that is problematic, but it usually gives you a starting point for your deductions...