On Thu, 22 Jan 2026 at 06:13, Eliot Courtney <[email protected]> wrote:
> On Thu Jan 22, 2026 at 12:26 PM JST, John Hubbard wrote: > > On 1/21/26 6:59 PM, Eliot Courtney wrote: > >> + // The area is contiguous and we leave an empty slot > before `rx`. > >> + // PANIC: since `rx > tx` we have `rx - tx - 1 >= 0` > >> + // PANIC: since `tx < rx < MSGQ_NUM_PAGES && > after_tx.len() == MSGQ_NUM_PAGES - tx`: > >> + // `rx - 1 <= MSGQ_NUM_PAGES` -> `rx - tx - 1 <= > MSGQ_NUM_PAGES - tx` > >> + // -> `rx - tx - 1 <= after_tx.len()` > > > > Hi Eliot, > > > > Documentation nit: the proofs are great, but the above just does > > not go into my head easily, because it's a proof, rather than a > > sentence. > I had a look now and I agree that it looks like plain English is the > defacto standard for the PANIC comments, so I will update them. > > But, I wonder what people think about this. IMO it makes sense to have > SAFETY and PANIC comments as rigorous proofs (where practical and > possible) to match the level of work the compiler does for us in the > infalliable areas of the code - if an issue occurs, unsafe or panicking > code is often the root cause IMO. Writing these in plain English is > easier to read but also harder to verify that the proof is correct and > harder to verify if there are any implicit assumptions. I am on the road, apologies for the formatting/HTML. This is something that we have discussed back and forth. Please take a look at Benno’s proposal at: https://lore.kernel.org/all/[email protected]/ (He may have a newer link) Cheers, Miguel
