[mike_hock]

Explicit types are a form of assertion. In the example

    { let y = g(x); f(y) }

I do not want to assert anything on the type of y but in

    {
        let y: Foo = g(x);
        // Do complex stuff with y
        f(y)
    }

I wrote the middle part with a specific mental model of what y is, and if that changes, I want to review that section to make sure that the semantics still match what I thought they were and does not just happen to be valid syntactically.

I do not want some automated tool to either strip assertions from my code, nor do I want it to synthesize assertions from a static analysis run of a particular version of the code. If I'm just gonna mindlessly remove all assertions and re-synthesize them on every refactor, they're useless.