[tom_mellior]

> Just the correspondence between static type safety and the halting problem.

I'm not sure if you are saying that there cannot be programming languages with decidable static type systems. Because there are programming languages with decidable static type systems. Typically you cannot encode Turing machines in the type system, so you don't get the kind of problem you seem to be talking about. (But you haven't really explained what you are talking about.)

[mnarayan01]

  // ... Well typed things ...
  if (arbitrary_well_typed_function()) {
    v = 0xF00 + "bar"
  }
  // ... Well typed things ...

Let's say this program is well typed iff `arbitrary_well_typed_function()` is falsy. If a static type checker can not compute `arbitrary_well_typed_function`, it needs to make a trade-off which a dynamic type checker need not.

[tom_mellior]

OK. Yes, static type systems need to make trade-offs. If this was your entire point, your original talk about undecidability was hiding it well.

[mnarayan01]

You got my point in your first comment in this thread. Unless that comment was the result of hours of striving, it doesn't seem as if the point was hidden well. If you did spend hours working at it, then I apologize and commend you on your success.