We don't have too many things on our wishlist describing changes to the compilation process itself, so here's one: importing a module to forbid potentially infinite loops and recursion:
In other words, if a loop or a recursive call is obviously non-terminating (as the two above), it produces a compile-time error.
Of course, this runs headlong into the Halting Problem (and things become a lot less obvious)... so the module flags up all potentially infinite loops and recursions as compile-time errors.
I think this should be tempered with two mechanisms for making the program compile again.
One is a blanket @terminates annotation. Basically silencing the error for that one.
The other is a "variant" (the opposite of an "invariant"). I think this concept comes from Eiffel, but I need to double-check that. The idea is to have an actual variable in the program that decreases with every iteration, but never goes below 0. The value is a kind of witness to the well-foundedness of the loop or recursion. (TODO: Check more details/examples on this.)
We don't have too many things on our wishlist describing changes to the compilation process itself, so here's one: importing a module to forbid potentially infinite loops and recursion:
In other words, if a loop or a recursive call is obviously non-terminating (as the two above), it produces a compile-time error.
Of course, this runs headlong into the Halting Problem (and things become a lot less obvious)... so the module flags up all potentially infinite loops and recursions as compile-time errors.
I think this should be tempered with two mechanisms for making the program compile again.
@terminatesannotation. Basically silencing the error for that one.