I'm not really convinced that this is true. I think you're brushing up against Rice's theorem, which is that proving arbitrary properties about arbitrary progra

I'm not really convinced that this is true. I think you're brushing up against Rice's theorem, which is that proving arbitrary properties about arbitrary programs is equivalent to the halting problem. That's why we constrain languages with type systems, which limits any typed language from expressing arbitrary turing complete programs. Proof assistance is sort of irrelevant. Types and proofs are related, as denoted by the curry howard correspondance. The real issue with "throwawaymaths"' point is that they're saying "use proof assistants" to people who are using proof assistants. SEL4 is a terrible example of a success story, as it took ages to complete, and then there was immediately a bug found in a class they weren't looking for - because rice's theorem. They're clearly advocating for the use of specific and explicit proof assistants, which is fine and a totally reasonable thing to advocate for, but in no way is related to rust or the discussion, which is why I chose not to engage.