I think it would be nice if there will be a world where you can express such a problem in a decidable mini-language where the compiler can deduce that the answe

I think it would be nice if there will be a world where you can express such a problem in a decidable mini-language where the compiler can deduce that the answer will be n(n+1)/2. :)