> I'm pretty sure it would. Why do you think it would not?

Languages like Coq require you to prove a function halts before it will compile. Yes, for an arbitrary function it can be arbitrarily difficult or impossible to prove termination. In most cases though, termination proofs aren't that complex (e.g. "it halts because the collection gets smaller each recursive call").

Besides, you're argument is basically sounding like "because you can't prove all functions halt it's a waste of time proving any functions halt". See the sel4 OS for an impressive example of what formal proofs can do.

I intended the program to clearly have a type error on the last line, where the string "foobar" is assigned to a variable that has been declared to be of integer type. (In hindsight, I guess it is ambiguous whether the imaginary pseudo-language we are communicating in types variables, as most static languages do, or values, as most dynamic languages do, and in the latter case it would type check. I should have done something that is a type error in either case, like `x = x / "foo"`.) My intent was to show that even though the desirable property 'does not encounter type errors in execution' is reducible to the halting problem in general, and in this particular case, is reducible to a famous conjecture, static type checkers can calmly and soundly verify that programs have this property! They do so by verifying a strictly stronger property, necessarily rejecting some programs that have the desirable property but accepting only programs that have it. A dependently typed language which can express properties like termination does the same thing, rejecting some programs that terminate but accepting only programs that terminate. In particular, they will accept only programs where YOU provide them with (at least an adequate sketch of) a formal proof of the property.

In general, when writing programs, we ought to develop at least a very informal argument for why they have the properties we want them to have. To the extent that they are correct, these informal arguments could be formalized. It's possible to imagine that with future technology, formalizing these arguments with the assistance of powerful tooling will actually be easier than reasoning about them informally, in the same way that you often find running and inspecting your lisp program easier than reasoning about it without assistance. As far as I know, neither computability theory or any other theoretical obstacle rules this out; it is just (perhaps far) beyond the state of the art.

Perhaps you have mistaken me for an absolutist advocate of static typing or formal methods, which I guess is reasonable in the context of the thread. I'm not at all: I've experienced plenty of joy and pain (and bugs) in both static and dynamic languages, and have had more experience and success with advanced testing methods than with formal ones. At this moment, I'm writing a testing tool in a dynamic language! I just wanted to clear up a technical misconception, because I have seen fields held back before by widely misunderstood impossibility results.

Happy lisping!