Software side there's a lot that can be proven and said about small sections of programs. I think a sibling commenter talked about an ISO standard related to t

Software side there's a lot that can be proven and said about small sections of programs. I think a sibling commenter talked about an ISO standard related to that (And I think it covers some hardware bits). My layman's understanding of it is that it's a way to specify as many assumptions about how the code will be run, where, and what side effects it will have and no others. That makes for a really nice set of assertions but the end effect is that you can't say anything about certain kinds of programs; i.e. This program is safe, That program can't be safe, and then these programs are unknowable. Godel should never have been allowed to publish anything.