I'm confused: you say that transparency and verification are the same thing, but your examples only seem to support that transparency enables verification. Is that closer to what you were trying to say?
Type signatures in a strongly typed language can be seen as a method of ensuring that the compiler proves that certain errors cannot occur, while also giving a human reading the program a better sense of what various functions do.
Yes! A programming language does this by restricting the set of programs that you can write, disallowing both correct and incorrect programs in the process. It has to, because it's infeasible (uncomputable, to be precise) to tell whether a program will actually hit "certain errors". For example, suppose that searchForCounterexampleToRiemannHypothesis() will run forever if the Riemann Hypothesis is true, and return true if it finds a counterexample. (This is a function you could write, I think.) Then if the Riemann Hypothesis is true, this program:
if (searchForCounterexampleToRiemannHypothesis()) {
"string" / "stringy" // type error
}
is a perfectly fine infinite loop that never attempts to divide "string" by "stringy". Nevertheless, a (static) type system will overzealously disallow this perfectly dandy program because it can't tell any better.
So type systems weaken the language. While that example was concocted, there are more realistic examples where you have to go out of your way to satisfy the conservative type checker. But, to your point (and against my point in the beginning), they weaken the language by requiring type annotations that make the language easier for the type checker to reason about (verification), and also easier for people to understand (transparency). There is a tradeoff between verification&transparency and expressiveness.
I'm confused: you say that transparency and verification are the same thing, but your examples only seem to support that transparency enables verification. Is that closer to what you were trying to say?
Yes! A programming language does this by restricting the set of programs that you can write, disallowing both correct and incorrect programs in the process. It has to, because it's infeasible (uncomputable, to be precise) to tell whether a program will actually hit "certain errors". For example, suppose that
searchForCounterexampleToRiemannHypothesis()will run forever if the Riemann Hypothesis is true, and returntrueif it finds a counterexample. (This is a function you could write, I think.) Then if the Riemann Hypothesis is true, this program:is a perfectly fine infinite loop that never attempts to divide "string" by "stringy". Nevertheless, a (static) type system will overzealously disallow this perfectly dandy program because it can't tell any better.
So type systems weaken the language. While that example was concocted, there are more realistic examples where you have to go out of your way to satisfy the conservative type checker. But, to your point (and against my point in the beginning), they weaken the language by requiring type annotations that make the language easier for the type checker to reason about (verification), and also easier for people to understand (transparency). There is a tradeoff between verification&transparency and expressiveness.