Explicit typing hurts the signal:noise of the code. I’d like to have invariants and pre/post-conditions, inferred or verified where possible, visually separated

Explicit typing hurts the signal:noise of the code. I’d like to have invariants and pre/post-conditions, inferred or verified where possible, visually separated from the expressions that do the important work (comments to the right, a block below the body, whatever).