3 ms·

Test suites are awesome

drdaeman 13y ago
Running tests, even with coverage and quickcheck does not replace static verification. At very best, such tests can assert that program should probably work with some known probability. In contrast, strong statically-checked typing may be used prove that program produces results correctly to the extent type system may express the necessary proof.
- alayne 13y ago
  Most type systems in statically typed languages can't make that guarantee. For example I can use Java reflection to call a method, change the method's parameters, and my code will only fail at runtime.
  - SCdF 13y ago
    That's kind of silly. If you're using Java and altering method signatures at runtime using reflection you're either in a very niche field where perhaps you shouldn't be using Java, or you're nuts. Just because you can get around a feature doesn't invalidate that feature. I'm not sure how I feel about static typing in Java, but it does do what OP talks about, because by default you're not playing devils advocate with reflection.
    - alayne 13y ago
      This problem happens with Spring all the time in Java which uses reflection. It's certainly not "silly" or a "niche field".
      - Buttons840 13y ago
        I agree. With Java + Spring + XML you can get one language for the price of two! How useful is Java's type checking when one typo in an XML file breaks your program? At least in Python I can follow the logic of the language and find where the mistake is. Spring's XML files don't have such logic and usually all you have is a confusing traceback to work with.
    - quacker 13y ago
      I'm not sure how I feel about static typing in Java, but it does do what OP talks about, because by default you're not playing devils advocate with reflection. Static typing can guarantee the functionality of quite a lot of code, but it cannot do this for any arbitrary piece of code. As an example, no compiler in any language can know what whether a user will numbers or garbage, when you're expecting numbers. You need to check for an exception in Java even in this simple case.
- nostrademons 13y ago
  When you're dealing with real-world systems you're always dealing with "probably work with some known probability". The hardware might burn out, or someone might trip over the cable, or a cosmic ray might randomly flip a bit and make your program go haywire. A proven-correct program doesn't help when you can't trust the physical infrastructure it runs on. Instead, you need to figure out what level of reliability you require and then work out a strategy to get there. Static-checking can be one element of this strategy, since you can use it to eliminate whole classes of bugs. But I've usually found that architectural solutions like canaries, automatic restarts, feature disablement, fallback codepaths, etc. are more effective at reducing errors per programmer-hour spent on them, and when you have those the reliability thresholds for the actual code you write can be much looser. (You probably still want to verify the hell out of the framework code that implements these architectural mechanisms, though.)

Running tests, even with coverage and quickcheck does not replace static verification. At very best, such tests can assert that program should probably work with some known probability. In contrast, strong statically-checked typing may be used prove that program produces results correctly to the extent type system may express the necessary proof.

alayne 13y ago
Most type systems in statically typed languages can't make that guarantee. For example I can use Java reflection to call a method, change the method's parameters, and my code will only fail at runtime.
- SCdF 13y ago
  That's kind of silly. If you're using Java and altering method signatures at runtime using reflection you're either in a very niche field where perhaps you shouldn't be using Java, or you're nuts. Just because you can get around a feature doesn't invalidate that feature. I'm not sure how I feel about static typing in Java, but it does do what OP talks about, because by default you're not playing devils advocate with reflection.
  - alayne 13y ago
    This problem happens with Spring all the time in Java which uses reflection. It's certainly not "silly" or a "niche field".
    - Buttons840 13y ago
      I agree. With Java + Spring + XML you can get one language for the price of two! How useful is Java's type checking when one typo in an XML file breaks your program? At least in Python I can follow the logic of the language and find where the mistake is. Spring's XML files don't have such logic and usually all you have is a confusing traceback to work with.
  - quacker 13y ago
    I'm not sure how I feel about static typing in Java, but it does do what OP talks about, because by default you're not playing devils advocate with reflection. Static typing can guarantee the functionality of quite a lot of code, but it cannot do this for any arbitrary piece of code. As an example, no compiler in any language can know what whether a user will numbers or garbage, when you're expecting numbers. You need to check for an exception in Java even in this simple case.
nostrademons 13y ago
When you're dealing with real-world systems you're always dealing with "probably work with some known probability". The hardware might burn out, or someone might trip over the cable, or a cosmic ray might randomly flip a bit and make your program go haywire. A proven-correct program doesn't help when you can't trust the physical infrastructure it runs on. Instead, you need to figure out what level of reliability you require and then work out a strategy to get there. Static-checking can be one element of this strategy, since you can use it to eliminate whole classes of bugs. But I've usually found that architectural solutions like canaries, automatic restarts, feature disablement, fallback codepaths, etc. are more effective at reducing errors per programmer-hour spent on them, and when you have those the reliability thresholds for the actual code you write can be much looser. (You probably still want to verify the hell out of the framework code that implements these architectural mechanisms, though.)