3 ms·

Rust has simple unit testing built into the language. And in Ada/Spark, tests can be a first class verification tool, alongside formal verification. We should

Rust has simple unit testing built into the language. And in Ada/Spark, tests can be a first class verification tool, alongside formal verification. We should go a lot further though. IMO, a unit that does not pass a spec/test should cause a compile time error. Testing systems should facilitate and converge with formal verification. Where possible, property based testing should be used and encouraged. And debugger tools should be able to hone in on areas where the result diverges from expectations.

cbanek 9y ago
^ This. And another example of something I'd want checked by the language is exception throwing / handling. It's another one of those places where code coverage won't help you unless you already know what you're looking for. Languages are getting better about it, but in general, handling errors is hard.
tjalfi 9y ago
Force.com doesn't allow you to deploy code to production unless at least 75% of the statements are executed[0]. I wish my employer had a similar requirement. [0] https://developer.salesforce.com/docs/atlas.en-us.apexcode.meta/apexcode/apex_testing_best_practices.htm https://developer.salesforce.com/docs/atlas.en-us.apexcode.m...
chriswarbo 9y ago
> IMO, a unit that does not pass a spec/test should cause a compile time error. We can achieve this in dependently-typed languages like Idris. First we define a datatype 'Equal x y', which will represent the proposition that expression 'x' is equal to expression 'y': data Equal x y where Refl : (x : _) -> Equal x x There are two things to note: - There is only one way to construct a value of type `Equal x y`, which is to use the constructor we've called `Refl`. - `Refl` only takes one argument, `x` (of arbitrary type `_`), and it only constructs values of type `Equal x x`. This is called "reflexivity", thus the name `Refl`. Hence if we use the type `Expr x y` anywhere in our program, there is only one possible value we can provide that might typecheck (`Refl x`), and that will only typecheck if `Expr x x` unifies with `Expr x y`, which will only happen if `x` and `y` are the same thing; i.e. if they are equal. Thus the name `Equal`. This `Equal` type comes in the standard library of all dependently typed languages, and is widely used. To use it for testing we just need to write a test, e.g. `myTest`, which returns some value indicating pass/fail, e.g. a `Boolean`. Then we can add the following to our program: myTestPasses : Equal myTest True myTestPasses = Refl myTest This will only type-check if `Equal myTest myTest` (the type of `Refl myTest`) unifies with `Equal myTest True`, which will only be the case if `myTest` evaluates to `True`.

cbanek 9y ago

^ This. And another example of something I'd want checked by the language is exception throwing / handling. It's another one of those places where code coverage won't help you unless you already know what you're looking for. Languages are getting better about it, but in general, handling errors is hard.

tjalfi 9y ago

Force.com doesn't allow you to deploy code to production unless at least 75% of the statements are executed[0]. I wish my employer had a similar requirement. [0] https://developer.salesforce.com/docs/atlas.en-us.apexcode.meta/apexcode/apex_testing_best_practices.htm https://developer.salesforce.com/docs/atlas.en-us.apexcode.m...

chriswarbo 9y ago

> IMO, a unit that does not pass a spec/test should cause a compile time error. We can achieve this in dependently-typed languages like Idris. First we define a datatype 'Equal x y', which will represent the proposition that expression 'x' is equal to expression 'y': data Equal x y where Refl : (x : _) -> Equal x x There are two things to note: - There is only one way to construct a value of type `Equal x y`, which is to use the constructor we've called `Refl`. - `Refl` only takes one argument, `x` (of arbitrary type `_`), and it only constructs values of type `Equal x x`. This is called "reflexivity", thus the name `Refl`. Hence if we use the type `Expr x y` anywhere in our program, there is only one possible value we can provide that might typecheck (`Refl x`), and that will only typecheck if `Expr x x` unifies with `Expr x y`, which will only happen if `x` and `y` are the same thing; i.e. if they are equal. Thus the name `Equal`. This `Equal` type comes in the standard library of all dependently typed languages, and is widely used. To use it for testing we just need to write a test, e.g. `myTest`, which returns some value indicating pass/fail, e.g. a `Boolean`. Then we can add the following to our program: myTestPasses : Equal myTest True myTestPasses = Refl myTest This will only type-check if `Equal myTest myTest` (the type of `Refl myTest`) unifies with `Equal myTest True`, which will only be the case if `myTest` evaluates to `True`.