My only point of reference for how they work is, admittedly, this article. I'm far from knowledgeable about formal methods but, in my understanding, if they're writing provably correct programs the code should, by definition, contain no 'errors'. (That is, it should always "do the thing right". There's no guarantee they've designed it to "do the right thing". Design errors may be exactly what the article is talking about.)
I'm not sure exactly what you mean when you say "every single possible input is tested". I would claim that this is not only impractical but impossible. The range of possible inputs to a system is infinite. This may sound pedantic, but in my experience as a software tester all sorts of failures often pop up when you look even slightly outside the range of values that seems sensible/likely/exhaustive for a given input.
Comments
My only point of reference for how they work is, admittedly, this article. I'm far from knowledgeable about formal methods but, in my understanding, if they're writing provably correct programs the code should, by definition, contain no 'errors'. (That is, it should always "do the thing right". There's no guarantee they've designed it to "do the right thing". Design errors may be exactly what the article is talking about.)
I'm not sure exactly what you mean when you say "every single possible input is tested". I would claim that this is not only impractical but impossible. The range of possible inputs to a system is infinite. This may sound pedantic, but in my experience as a software tester all sorts of failures often pop up when you look even slightly outside the range of values that seems sensible/likely/exhaustive for a given input.