[aconz2]

I hear you on expressiveness of using the language. Of course (and as you mention) the strength of restricting the expressiveness is that it becomes decidable in some amount of acceptable time for most programs.

I agree with your last sentiment but I don't think it has to be any less "formal" than something like Coq. I just think we shouldn't be so concerned with proving all properties of a program before running. And then we can turn the knob to adjust how much to prove during vs. before running.