People are missing the point of your post, which is a bit of a shame. The point is that `foo p n` returns an integer when `n` is the sum of two positive integers that both satisfy `p`. `bar n` holds when `n` is prime. Thus `foo bar` always returns an integer iff Goldbach's conjecture is true. You point is that no one knows how to prove Goldbach's conjecture therefore no formal methods can prove that `foo bar` never crashes.

If the dependent typing proponents in this thread responded to your point rather than picking holes in your usage of the words "composition" and "terminate" then they might make some interesting counterpoints. For example, they might say

1. "We don't expect dependent types to be able to prove everything (of course), we only expect them to be approximately as good as any other proof method for almost any property of interest", or

2. "What do you mean "you can easily prove almost any property of interest about each of them in isolation"? Does "property of interest" have a specific definition? How about `bar (factorial (10101010))`? Is that `True`? Is it not a "property of interest"? Is it not "in isolation"? How about "there exists n such that `bar m == False` for all m > n"? How would you "easily" prove that?

Personally I'm not a dependent typing proponent so 1 is just my wild speculation. I am interested in your response to 2 though.