4 ms·

We regard "this program is hard to test" as a problem that's worth refactoring to fix; why shouldn't we regard "this program is hard to verify" the same way?

by rntz 9y ago

phkahler 9y ago
But "this language is hard to verify" should not trump the usability of the language. The verification only needs to be done once, while the language will be used to write code again and again. If it doesn't negatively affect the language users then sure, change it to make verification easier.
- monocasa 9y ago
  You need to reverify when you change the code too. Otherwise you could make the same arguments about testable code.
- nine_k 9y ago
  It depends on the cost of a defect. A language used for aircraft control software is going to have much stricter requirements for static analysis that a language used to create a website with cute pictures of kittens — even if happens to be the very same language.
- emn13 9y ago
  You're not verifying a language, you're verifying a program (or some part of one). Sure- that part in this instance may be implementing a language standard library, but who cares? That program also has tests, docs, types and all the other things people use to convince themselves of correctness. It really is like unit testing. There too you could make the argument that in some cases untestable code might be worth it if the alternative is an api that's hard to use. And there too an api may well be used many orders of magnitudes more frequently than it is changed. I think you have to decide that on a case by case basis (at least, I can't think of any convincing general argument there).
weberc2 9y ago
This is a good question. I'm inclined to say that the value proposition for testing is better than for verification. First of all, if your unit is hard to test, it is likely to cause other issues, but probably more importantly, testing finds a lot more bugs per unit effort than formal verification. That last point is based exclusively on my intuition and it could well be wrong--it would be good to hear from people with more experience with both testing and formal verification. Also, now that I think about it, the value proposition isn't fixed for all applications. Testing is the better value proposition if you need to catch the easiest 95% of your bugs (arbitrary number for example purposes), but if you need to catch 99.999% of your bugs, the testing effort may likely be much greater than the formal verification effort. That said, open source projects like Rust get tons of testing for free by virtue of being very, very popular, so I'm not sure how to weigh one against the other.

We regard "this program is hard to test" as a problem that's worth refactoring to fix; why shouldn't we regard "this program is hard to verify" the same way?

by rntz 9y ago

We regard "this program is hard to test" as a problem that's worth refactoring to fix; why shouldn't we regard "this program is hard to verify" the same way?

phkahler 9y ago

But "this language is hard to verify" should not trump the usability of the language. The verification only needs to be done once, while the language will be used to write code again and again. If it doesn't negatively affect the language users then sure, change it to make verification easier.

monocasa 9y ago
You need to reverify when you change the code too. Otherwise you could make the same arguments about testable code.
nine_k 9y ago
It depends on the cost of a defect. A language used for aircraft control software is going to have much stricter requirements for static analysis that a language used to create a website with cute pictures of kittens — even if happens to be the very same language.
emn13 9y ago
You're not verifying a language, you're verifying a program (or some part of one). Sure- that part in this instance may be implementing a language standard library, but who cares? That program also has tests, docs, types and all the other things people use to convince themselves of correctness. It really is like unit testing. There too you could make the argument that in some cases untestable code might be worth it if the alternative is an api that's hard to use. And there too an api may well be used many orders of magnitudes more frequently than it is changed. I think you have to decide that on a case by case basis (at least, I can't think of any convincing general argument there).

weberc2 9y ago

This is a good question. I'm inclined to say that the value proposition for testing is better than for verification. First of all, if your unit is hard to test, it is likely to cause other issues, but probably more importantly, testing finds a lot more bugs per unit effort than formal verification. That last point is based exclusively on my intuition and it could well be wrong--it would be good to hear from people with more experience with both testing and formal verification. Also, now that I think about it, the value proposition isn't fixed for all applications. Testing is the better value proposition if you need to catch the easiest 95% of your bugs (arbitrary number for example purposes), but if you need to catch 99.999% of your bugs, the testing effort may likely be much greater than the formal verification effort. That said, open source projects like Rust get tons of testing for free by virtue of being very, very popular, so I'm not sure how to weigh one against the other.