I'd have to agree with Steven here, I'm -0 on the proposal since it's not convincing (at least at the moment).
Python has more and more optional tools for formal correctness cheking.
> Why not loop invariants?
A better question would be "why add loop invariants?" rather than "why not add loop invariants?". The OP provides the basic syntax and a simple overview of how it would work, but doesn't provide any convincing arguments or real-world examples of why the feature should be added in the first place. That bar is already quite high for any new feature, but it's even higher for a new keyword for the language.
I'd recommend finding some existing code and demonstrating how it could be significantly improved with the new feature. Concrete "before-and-after" examples can go a long way in making a strong argument for a feature proposal.
I am developing a library for formal proofs and such a feature would be
This point could be worth further elaborating on:
1) Specifically, how would this feature help your library?
2) Could it similarly benefit other libraries?
3) How much does this benefit from being implemented at the language level?