[polityagent]

Safely and automatically renaming a function, local or global variable does not require a type system (see clojure and many other dynamic languages). Only renaming an instance field on a class needs it (because then all accesses on an object must be renamed, which requires knowledge of the type of your variables).

Incidentally programming in a more functional style reduces the need for this kind of thing. it doesn't eliminate it though so it can still be a source of runtime bugs when typos creep in, that's a trade off you have to make.

[polityagent]

Unit tests for business logic and specifications for data shape can help to catch those typos as a side effect of the other benefits they bring. However typo catching will never be as solid as in a typed language, I've decided I'm ok with that as long as I'm not programming something that could kill someonev if it crashes.

[tsimionescu]

If you're writing an application that could kill someone if it crashes, you'd better not be relying on the type system to catch those crashes for you, since it will only catch the most obvious ones.

For any life-critical system you want first and foremost to have a battery of end-to-end tests that run the software on the target hardware under various operating conditions. No amount of software-only testing/formal methods will give you this part.

Then, you want to have a formal specification of your program that can be run through a model checker - this would be the industry standard, though, if you have a team of PhDs at your disposal, you could also try to go with full formal verification a la Coq.

Finally, you want unit testing, integration testing, and possibly a type system to help day-to-day development. But do note, none of these should be critical for assuring the system works as indended - if typos in your code aren't caught by your end-to-end tests, what hope is there that they will catch complex dynamic behaviors?

[speedplane]

> If you're writing an application that could kill someone if it crashes, you'd better not be relying on the type system to catch those crashes for you, since it will only catch the most obvious ones.

Safety critical systems are quite different from the vast majority of software systems, and raising them as an example in a general programming argument isn't really fair. There already are safety critical certifications that are mandatory for many aviation and healthcare related applications. They generally utilize heavy testing, model checking, and supporting documentation. Very few commercial industries operate with this much attention to quality, basically because it's too expensive.

[tsimionescu]

The GP had raised them, that's the only reason I commented about this.

You are right though, the standard for that type of software is very different from regular programming.

Still, we shouldn't forget that even the strongest typing can't substitute testing. Most likely, even if you had a formally proved system, which is already much, much more difficult than any other kind of regular software development practice, you would still want some amount of testing to go with that system before putting it in production.

[polityagent]

Yes I agree

[thrower123]

It doesn't require it, but by all indications it makes the tooling much easier to write when there is a type system and it's constraints reducing the surface area.