I think Lisa Lippincott's research is a good start for the theory of
general procedural proofs of this nature.

G

On Thu, Apr 22, 2021, 22:01 Ville Voutilainen via Std-Proposals <
std-proposals_at_[hidden]> wrote:

> On Thu, 22 Apr 2021 at 23:53, Thomas Neumann
> <tneumann_at_[hidden]> wrote:
> >
> > > The idea generalizes:
> > >
> > > 1) ..while the result of an operation with particular characteristic
> > > $foo on an object X is within its lifetime..
> > > 2) ..operations with another particular characteristic $bar on X are
> ill-formed
> >
> > this would be useful, too, but goes far beyond what I propose. And I am
> > not even sure how we can ensure something like this if the code in
> > question is in separate compilation unit, I think this would require
> > extensive changes to the type system.
>
> I would think you can't truly ensure the borrowing or the lack of need
> for it in the presence
> of separate TUs either. Yeah, sure, in the example you showed, passing
> a reference to another
> function is ill-formed without explicit borrowing.. ..but that
> explicit borrowing is annoying
> when a programmer "knows" that it's not necessary.
>
> > > how to try and fit that general idea into C++. I would wager a guess
> > > that it would be more attractive if it can do more
> > > than just the borrowing you illustrate. On the other hand, if it tries
> >
> > My proposal is more limited in that I only want to support borrowing as
> > discussed here:
> >
> > https://doc.rust-lang.org/book/ch04-02-references-and-borrowing.html
> >
> > But note that borrowing is a very powerful concept. When we combine that
> > with controlled pointers (e.g., smart pointers that can either prove
> > that the access is safe or introduce runtime checks), we can eliminate
> > all memory bugs. As Rust has demonstrated. And I think that is extremely
> > useful. The price, of course, is that this requires some changes to
> > coding style.
>
> I understand that, but memory is just memory. It's an important
> resource, but it's just
> one kind of resource. I would hate to paint ourselves into a corner
> when going for memory safety,
> and then failing to use that same path for resource safety.
> --
> Std-Proposals mailing list
> Std-Proposals_at_[hidden]
> https://lists.isocpp.org/mailman/listinfo.cgi/std-proposals
>