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

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.