Your claim that the Linux Kernel Mailing List is representative of OSS discussion forums suggests limited knowledge. I always found the LKML to be much better than most other forums.

It has wifi, just read the link

The methodology is the best you can do; proving anything is basically establishing that two descriptions are equivalent.

With formal systems you usually have one definition that written to make it obviously correct and another that is more "pragmatic". In the case of propositional logic the obviously correct formalization is truth tables which are completely untractable to work with for large numbers of variables but are very simple conceptually. The "pragmatic" formalization is the logical connectives like and, or, implication etc that we normally think of as propositional logic. When they prove that propositional logic is sound they mean that all propositions give the same result as a truth table when evaluated and when they prove it is complete they mean that all truth tables give the same result as a proposition and thus propositional logic and truth tables both formalize the same concept.

There is no concept of "correct" in formal systems because it is inherently an informal concept meaning it does what it is supposed to do.

A machine-checked proof means they are checking that the implementation in C is consistent with the specification written in Haskell. Your confidence that the kernel is correct is exactly your confidence that the specification in Haskell is correct. The C code is 7500 lines, I wonder how big the Haskell code is. This has nothing to do with Godel's incompleteness theorem as correct doesn't mean anything even close the formal definition of complete.

Obviously you were trying to write C in Ada; I agree, that would be truly awful.

I don't think the active/passive synchronisation provided by Ada is the solution for using multiple cores efficiently but since I keep seeing people reinvent the same solution in Java there must be something useful about it. I found Ada quite easy to learn as it is remarkably consistent although that is the result of it being designed by just a couple people working closely together.

When I was in St. Petersburg I had better luck finding older people who spoke French or German as those languages had had more emphasis on them 40 years ago when English really wasn't taught at all.