Kinda like a knife -- it's a very useful tool if used well and a very painful tool if mishandled.
Code will always have bugs, and you cannot truly understand how something written in a Turing complete language will behave without running it.
> very painful tool if mishandled
Part of being a skilled craftsman is choosing the right tools, which includes understanding and respecting their limits. The language for writing contracts makes all state mutable by default, has ambiguous operators that change behavior depending on storage location or if the operand was a literal, and doesn't defined the order of evaluation for expressions, to name just a few of it's design problems[1]. This isn't a "useful tool:", it's a strong indicator of a another fractal of bad design[2].
There are also other contract languages aimed to solve some of the limitations you mention, like Tezos/Michelson [2][3], which facilitate formal verification.
The issues you point out are certainly valid, but I believe people in the space are cognizant of them and are working on solutions.
It's limiting, but you can still have many of the fancier features by baking standard versions of them into the language/stdlib itself.
> I believe people in the space are cognizant of them and are working on solutions.
The problem with that is that this isn't a bug or engineering problem that we can solve with impossibly talented devs and a sufficiently large r&d budget. Questions about any non-trivial semantic behavior of a program (such as, "will the program halt"[2]) are known[3] too be undecidable[4].
[1] according to LangSec, the grammar needs to be deterministic context-free (or simpler). Anything more complex is undecidable.
[2] https://en.wikipedia.org/wiki/Halting_problem