Are engineering standards for public buildings evil because they stifle architects' freedom to design whatever crazy structures tickle their fancy?
The physical analogy is good because even there one can see that there are different standards --- and, unlike what the "safe software" community seems to promote, engineers are not doing the equivalent of making every building strong enough to withstand a nuclear war and calling anything less "unsafe".
This also brings up another difference with software: the "absoluteness". In the physical world, no security is perfect. Locksmiths exist, and with enough determination, essentially anything can be broken into. But in the software world, with good encryption, that can never occur. Provably correct software can be employed for effectively unbreakable DRM and un-rootable/jailbreakable user-hostile devices, of which there is (fortunately) no similar real-world analogy I can think of.
Nobody's saying you can't do that; that sounds rather dystopian, a society where pointer arithmetic is illegal!
Given that there are attempts at even prohibiting Turing-completeness[1][2], I would not be surprised if that eventually happens. As it is, I'm sure there are already people who would consider you suspicious if you write software in an "unsafe" language, and from there it is not far to complete prohibition.
So... you're saying it's unethical to invent tools that can be used to write software that works as intended and contains no exploitable bugs, because that software could then be used as a tool of oppression?
You can extend that absolutist argument to say that inventing anything that could be used as a tool of oppression is unethical. Like, inventing plumbing may have done great things for human society, but it was ultimately unethical because when the police came to take away your general-purpose computer they used a pipe to hit your kneecaps until you told them where it was. Or, how about this: developing any society beyond the level of the most primitive hunter-gatherer tribe is unethical, because what are governments if not the agents of oppression themselves?
This is the sort of abstract position that can't really be argued with in a vacuum, so I'm not going to try. But it's also not a useful ethic for building a modern society free of large-scale oppression, because it completely ignores the practical realities of doing so.
In the mean time, buggy, exploitable software is out there in the real world hurting real people every day.
> ... making every building strong enough to withstand a nuclear war and calling anything less "unsafe".
Yes. Except the equivalent in software is using something like Coq, where your intention is proven to be correct. (You even mention provably correct software in the next paragraph...) And yes, it would be awesome if we could prove every program, because all we would be doing is proving that the programmer's intent is correctly coded into the software, which doesn't limit freedom of expression at all. (I would argue that such is actually an even stronger form of expression, as it's afterwards impossible to misconstrue your intent.)
> Given that there are attempts at even prohibiting Turing-completeness[1][2], I would not be surprised if that eventually happen...
Rust is not one of these, and no one but you seems to have this in mind. So it's a bit of a strawman to be throwing it out here, no? But yes, obviously such a language would limit your freedom of expression.
The physical analogy is good because even there one can see that there are different standards --- and, unlike what the "safe software" community seems to promote, engineers are not doing the equivalent of making every building strong enough to withstand a nuclear war and calling anything less "unsafe".
This also brings up another difference with software: the "absoluteness". In the physical world, no security is perfect. Locksmiths exist, and with enough determination, essentially anything can be broken into. But in the software world, with good encryption, that can never occur. Provably correct software can be employed for effectively unbreakable DRM and un-rootable/jailbreakable user-hostile devices, of which there is (fortunately) no similar real-world analogy I can think of.
Nobody's saying you can't do that; that sounds rather dystopian, a society where pointer arithmetic is illegal!
Given that there are attempts at even prohibiting Turing-completeness[1][2], I would not be surprised if that eventually happens. As it is, I'm sure there are already people who would consider you suspicious if you write software in an "unsafe" language, and from there it is not far to complete prohibition.
"The road to hell is paved with good intentions."
[1] http://boingboing.net/2012/08/23/civilwar.html
[2] http://boingboing.net/2012/01/10/lockdown.html