Formal verification is needed but syntactic sugar is not inherently the problem. The problem is that there a a million gotchas because it looks high level, but isn't.

Defaulting to `storage` instead of `memory` for variables is one huge issue that can let you silently corrupt your contract.

Lack of builtin manipulation of datatypes, weird types that are cumbersome to use correctly...

I am not equipped to exhaustively lament it as a language, but it is not a pleasant experience.