[kragen]

> I really don't like reading these dimwitted screeds.

this 'dimwitted screed' is by the primary author of rtlinux, which was to my knowledge the first instance of running linux under a hypervisor, and the leader of the small team that ported linux to the powerpc in the 90s. he has also written a highly cited paper on priority inheritance. if you disagree with him, it is probably for some reason other than his dimwittedness

i can't specifically testify to his knowledge of modern proof theory, but his dissertation was on 'a modal arithmetic for reasoning about multilevel systems of finite state machines', and his recent preprints include 'standard automata theory and process algebra' https://arxiv.org/abs/2205.03515 (no citations), 'understanding paxos and other distributed consensus algorithms' https://arxiv.org/abs/2202.06348 (one citation), and 'the meaning of concurrent programs' https://arxiv.org/abs/0810.1316 (draft, no citations), so i wouldn't bet too much against it

i'm interested to hear what you've written on modern logic and proof theory to understand your perspective better