4 ms·

how do they verify that the third party libraries they are going to use actually do what they promise to do in all cases?

AnimalMuppet 13y ago
"Trust, but verify"? Test the libraries to the degree of confidence that you need. (There was a link here a few days ago that advocated testing an algorithm with all possible floats, because there's only 4 billion of them. If you really need the library function to work the way you expect, that level of testing is not out of line.)
- tluyben2 13y ago
  If you need your unit tests 'show' that 4 billion floats are giving the desired answer, creating some formal proof instead doesn't seem far fetched either. I guess it all depends what you are writing things for; personally I would like to see the radiation equipment in hospitals to have formally verified software on board. The fact that 'this is not feasible' which is management speak for 'this is too expensive' remains to be kind of a depressing truth for me when we're talking lives. For non life threatening stuff the crap people deliver now is ok-ish as no-one seems to want to pay (or ask) for anything better. I'm just wondering how you validate something is non life threatening; a bug in some financial handling code could be life threatening if someone loses all because of it and kills himself? As I reached the ripe old age of almost 40, I get requests to review code quite a lot and it makes me want to take up gardening instead. It pays a lot less but at least I can kick my alprazolam habit.
lmkg 13y ago
In Dijkstra's world, there is no 'real software' but what has been mathematically proven correct. Horribly unworkable in practice, but man, having core libraries & frameworks be formally verified sounds like utopia.
- thibauts 13y ago
  Mathematically proving correct is possible if you have a formal mathematical definition to prove against. So what you're doing is translating the problem from one language to another. This is not the same at all as programming to solve user's problems where the only formal definition is the program itself. The most we can do in this respect is proving the correctness of small parts of ours programs with tests, i guess.

AnimalMuppet 13y ago

"Trust, but verify"? Test the libraries to the degree of confidence that you need. (There was a link here a few days ago that advocated testing an algorithm with all possible floats, because there's only 4 billion of them. If you really need the library function to work the way you expect, that level of testing is not out of line.)

tluyben2 13y ago
If you need your unit tests 'show' that 4 billion floats are giving the desired answer, creating some formal proof instead doesn't seem far fetched either. I guess it all depends what you are writing things for; personally I would like to see the radiation equipment in hospitals to have formally verified software on board. The fact that 'this is not feasible' which is management speak for 'this is too expensive' remains to be kind of a depressing truth for me when we're talking lives. For non life threatening stuff the crap people deliver now is ok-ish as no-one seems to want to pay (or ask) for anything better. I'm just wondering how you validate something is non life threatening; a bug in some financial handling code could be life threatening if someone loses all because of it and kills himself? As I reached the ripe old age of almost 40, I get requests to review code quite a lot and it makes me want to take up gardening instead. It pays a lot less but at least I can kick my alprazolam habit.

lmkg 13y ago

In Dijkstra's world, there is no 'real software' but what has been mathematically proven correct. Horribly unworkable in practice, but man, having core libraries & frameworks be formally verified sounds like utopia.

thibauts 13y ago
Mathematically proving correct is possible if you have a formal mathematical definition to prove against. So what you're doing is translating the problem from one language to another. This is not the same at all as programming to solve user's problems where the only formal definition is the program itself. The most we can do in this respect is proving the correctness of small parts of ours programs with tests, i guess.