Comment by uecker
4 days ago
I was thinking for implementing borrow-checker like rules for C but after I have seen what SMT solver can do I think it is not necessary to constrain the language in this way.
4 days ago
I was thinking for implementing borrow-checker like rules for C but after I have seen what SMT solver can do I think it is not necessary to constrain the language in this way.
Yeah, the problem with the lifetimes profile vision, is the lack of acknowledgement of how MSVC and clang-tidy have struggled to achieve the Core Guidelines ideas for lifetimes (since 2015), without additional annotations.
MSVC requires SAL and clang has equally added extensions for type annotations.
The WG21 politics killed the Safe C++ proposal with the P3466 paper,
"(Re)affirm design principles for future C++ evolution"
https://www.open-std.org/jtc1/sc22/wg21/docs/papers/2024/p34...
> Do not add a feature that requires viral annotation
However it is quite clear, that without changing language semantics, for the lifetimes profile to be actually useful, as shown by MSVC and clang experience, we would need to have [[profile:lifetime(something)]] in plenty of places.
Not only would that be more verbose than what Rust and Safe C++ proposal, it would still require placing those annotations on the standard library (yet another complaint from the anti-Safe C++ proposal folks), and naturally violate the paper that was voted for as the design principles for future C++ evolution.
However in regards to how to check for C and C++ lifetime issues, at least if the source code is fully available, I have had some good experience with AI tools doing code review, like CoPilot on Visual Studio.
Maybe that is possible way forward, moreso if the code isn't being fully written by humans.
Regarding C specifically, what about having Frama-C's ACSL as some kind of ISO C annex?
Compilers would just ignore the annex and whoever wants to implement it, can already do this. And I also think ACSL is too complex for what is needed and also not well integrated with the rest of the language.
IIRC Rust's borrow checker analysis is more or less a subset of what SMT solving is capable of. It's "just" a question of tradeoffs made with respect to performance, complexity, precision, etc.
It is a really tiny and trivial subset of what model checkers can do. Model checkers can often prove memory safety of entirely unmodified C code. The problem is that this still runs into complexity problems and does not scale to non-toy programs. But this would also really be very far at the other end of the borrow checker that would require rewriting everything into a very specific form a borrow checker accepts.. IMHO a middle ground with some annotations is realistic and would be far more convenient than a borrow checker when supported by good tooling.
> The problem is that this still runs into complexity problems and does not scale to non-toy programs.
Right; that is why Rust's borrow checker was designed to be intraprocedural only. That obviously is a tradeoff of its own: now functions need to be annotated to convey information across function boundaries, and the annotations picked will influence what can and cannot be expressed.
> IMHO a middle ground with some annotations is realistic and would be far more convenient than a borrow checker when supported by good tooling.
I'd be interested in seeing what such a middle ground looks like, particularly in respect to what tradeoffs it makes!
10 replies →
A borrow checker can do more harm than good in some cases. An arguable example of that is https://fasterthanli.me/articles/a-rust-match-made-in-hell .
Your background is C as I understand it, and C does not really have issues with temporaries as they are known in C++ and Rust.
My understanding:
C compound literals have invariable and relatively long lifetimes, namely to the end of the local block, and to shorten those lifetimes, one has to put the expression with the compound literal in a new, smaller local block. The advantage of those long lifetimes is that lifetimes are typically long enough for it not to cause issues in C. C also does not have RAII.
Both C++ and Rust have varying lifetimes of temporaries and have RAII. Both C++ and Rust have had messes with lifetimes, C++23 changed lifetime rules for the range-initializer expression of range-based for-loops, and Rust changed lifetimes rules in Rust 2024 such that whether a specific piece of Rust code has a deadlock or not, depends on its edition, and editions are generally not specified per-file but per-project.
Temporary lifetime extension can be tricky for both developers and language designers.
But the borrow checker can make it worse in some situations, for it can push developers towards bug prone designs that have greater risks of deadlocks, just to satisfy the borrow checker. The borrow checker also mostly enabled the language designers to go wild with lifetimes, since they did not have to worry as much about UB as long as they were in the not-unsafe subset, so the issues with deadlocks might be worse in practice than if they had been more careful and restrained with lifetimes.
It can also be very subtle whether Rust code has deadlocks or not. One of these Rust programs has a deadlock, the other does not. The difference is the presence and absence of temporary lifetime extension, as per the "{}".
https://play.rust-lang.org/?version=stable&mode=debug&editio...
https://play.rust-lang.org/?version=stable&mode=debug&editio...
4 replies →