Words like "any effects" and "safe" have broader meanings than the way they are used in type systems. I ask that you be a bit more precise in your advocacy.
I can replace a sorting method having O(N log N) time with one having O(N^2) time, without changing the type. But it will certainly have an effect on my system, and if the run-time is too long, may result in an unsafe system (eg, in a real-time control system which requires a maximum response time).
While I know what you mean, "bad code" includes things like unacceptable performance.
I also find it hard to understand how to apply type systems to algorithms. What is the type of an algorithm which returns a graph diameter, and how does it differ from one returning the graph eccentricity or other graph property?
(That's where "same values for the same arguments" comes in, but that's that hard part of the problem, yes?)
I can replace a sorting method having O(N log N) time with one having O(N^2) time, without changing the type. But it will certainly have an effect on my system, and if the run-time is too long, may result in an unsafe system (eg, in a real-time control system which requires a maximum response time).
While I know what you mean, "bad code" includes things like unacceptable performance.
I also find it hard to understand how to apply type systems to algorithms. What is the type of an algorithm which returns a graph diameter, and how does it differ from one returning the graph eccentricity or other graph property?
(That's where "same values for the same arguments" comes in, but that's that hard part of the problem, yes?)