On Thu Jan 22, 2026 at 2:07 PM JST, Eliot Courtney 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 see there are some guidelines about SAFETY: comments but not about > PANIC: comments in Documentation/rust/coding-guidelines.rst.
Would be interesting to have Miguel/Alice and the core team's opinion on this IMHO.
