Re: Follow-up on Linux-kernel code accessibility

[Paul E. McKenney]

On Fri, Dec 19, 2025 at 07:51:47AM +0100, Julia Lawall wrote:
> Maybe we're not looking for an instant understanding methodology.  Rather
> a machine checkable way to document the invariants that exist in the head
> of the developer, and for some bounded amount of time in the head of the
> person who has tried to reconstruct them.

I like that goal.  Much easier to evaluate the results than for
improving learning, for one thing.

> There are different levels of specifications that one can write.  In Japan
> Imentioned how for the enable-disable ftrace function, I enumerated all of
> the permutations of the if tests, resulting in hundreds of lines of
> specifications, but after two failed attempts, the third attempt yielded
> both valid specifications and some insight into what the function was
> doing.  This insight could potentially be used to make some higher level
> specifications that would be even more concise than the current
> English-language ones.  Maybe the low-level ones could be made
> automatically in many cases, or regenerated automatically from some hints.
> But the low-level ones may be needed to make the bridge between the code
> and the high-level specification.

If it was easy, we would already be doing it?  ;-)

							Thanx, Paul