Your opinion is common here. However, you can't just say your opinion is the consensus and that makes people who have other experiences wrong, end of debate. Popularity doesn't indicate truth. I'm sorry you haven't seen it working well, but there are counterexamples where people are productive with a relatively low number of issues.
Inb4 you move the goalposts for "at scale". This is an operating system with capability-based access control which is not something that most operating systems even have.
Also the cryptographic constraints are part of the proof system.
at scale, it is not possible for humans to hand-write C programs that are free of segmentation fault class errors
this is not controversial or in any way arguable