Pre-RFC: Extending where clauses with limited formal verification

I think fully supporting value semantics at compile time turns inevitably a language into a theoretic impractical one, for the following reasons:

  • undecidability
  • slow compilation
  • tight coupling of code aka fragile code problem

The latter problem leads to overspecification akin to the exception system enumerating all the exception which can occur. Updating such signatures leads to a cascade of errors.

Tracking value state is also hard, e.g. you pull out an element of a list and want to apply that element to a function expecting the element to be five forcing the compiler to track the current state of the list. I think runtime contracts are more valuable, you aren't perfect with them, but you can improve safety with linting and the linting process don't have to be perfect opposed to a type system.

2 Likes