I think it would imply that it is a Turing incomplete language. So, it would not be able to express certain programs, but all the computation you can represent is mathematically shown to reduce to a termination point.
I know with idris there is also a progress evaluator for otherwise general recursion that proves that your input is always "getting smaller". Not sure if charity has the same deal or not.
Regardless, it isn't turning complete, but the interesting part is how far you can get in a sub turing environment.
afaik it is still in relatively active development