I'd have to agree with Steven here, I'm -0 on the proposal since it's not convincing (at least at the moment).

haael wrote:
> 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
> handy.

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?




On Tue, Mar 17, 2020 at 11:00 PM Steven D'Aprano <steve@pearwood.info> wrote:
On Tue, Mar 17, 2020 at 06:12:56PM +0000, haael wrote:
>
> Python has more and more optional tools for formal correctness cheking.

Are you talking about third-party applications?


> Why not loop invariants?

Wrong question :-)

Adding new language features to Python isn't "default allow", adding
every new feature that somebody suggests unless there is a reason not to
add it. It is "default deny" -- new features have to be justified before
they will be added, and even if they are justified, they still might not
be added if:

- the costs of the new feature outweigh the benefit;
- there is sufficient opposition and insufficient support;
- or nobody is interested enough to do the work.

So the better question is:

*Why add loop invariants as a language feature requiring a new keyword?*


> Loop invariant is such a statement that if it was true before the loop
> iteration, it will also be true after the iteration. It can be
> implemented as an assertion of an implication.
>
>
>     now_value = False
>     while running_condition(...):
>         prev_value = now_value
>         now_value = invariant_condition(...)
>         assert now_value if prev_value else True
>
>
> Here for ellipsis we can substitute any values and variables.

An actual real-world example would be more convincing.


> I propose the new syntax:
>
>     while running_condition(...):
>         invariant invariant_condition(...)
>
>
> The keyword 'invariant' is allowed only inside a loop.

There are other kinds of invariants than just loop invariants. Can you
justify why loop invariants are more important than other invariants?

Can you point to other languages that offer loop invariants, but not
other invariants or contracts such as preconditions and postconditions?

For comparisons sake, this is how Eiffel handles loop invariants:

https://www.eiffel.org/doc/eiffel/ET-_Instructions#Loop_invariants_and_variants

--
Steven
_______________________________________________
Python-ideas mailing list -- python-ideas@python.org
To unsubscribe send an email to python-ideas-leave@python.org
https://mail.python.org/mailman3/lists/python-ideas.python.org/
Message archived at https://mail.python.org/archives/list/python-ideas@python.org/message/SJ7PHT3SZPQL3DZTNBANA5K4XKG6N3OK/
Code of Conduct: http://python.org/psf/codeofconduct/