Earlier quoted context omitted.
> testing should be built into the language itself I wonder what that would look like...
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 to…
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 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