Perhaps the problem is that static typing is confused with how some languages implement it. It can, and has, been implemented such that it dramatically improves compilation, correctness, static analysis and documentation without making code horrendously verbose.
Powerfully-typed languages also work much better for structured editing.
http://docs.idris-lang.org/en/latest/tutorial/interactive.ht...
Most of the time what people hate with static languages is type annotations.
What will blow their minds is a language that is both a) type safe and b) easy to type (i.e. what gives dynamic languages their flavor).
Luckily we're getting to a point (Scala) where this is mainstream.
Scala can be quite concise but we do have to be explicit with type signatures, and that only increases as we go up the abstraction ladder.
A strict Haskell with a decent module system, or a modern SML that borrows some nice-to-haves from Haskell and Scala would be my ideal language.
Mind blowing is the amount of output and obscurity of the error message you get from the type checker. It's harder to understand the error message than to debug the program if compiled "unsafely".
With time the way I approach code is also much more and abstract. You look at diagonal invariants more than code itself.