This is interesting in that if you can use channels as described by the CSP book[1] you could build a kernel that is guaranteed to be free of concurrency bugs.
This would be important because even if you have proven the functional correctness of a kernel, that typically excludes the concurrency aspect.
This would be important because even if you have proven the functional correctness of a kernel, that typically excludes the concurrency aspect.
[1] (https://www.cs.cmu.edu/~crary/819-f09/Hoare78.pdf)