I am well aware of most of the efforts you've linked, and those are what my comment was about.

> There are certain problems that are incredibly difficult to solve (often undecidable) in the context of some generic language

That statement is objectively wrong. Was the use of undecidable here intentional?

> That statement is objectively wrong. Was the use of undecidable here intentional?

It was intentional, and here's a proof (sketch) that it's objectively right. Consider the question of whether a procedure's return value (if it halts) will be a string?

We can prove that this question is undecidable in Python, by considering procedures of the form:

    def foo():
      if bar():
        return "hello"
      else:
        return 123

The answer to our question will be true if 'bar' returns a truthy value (or doesn't halt), or false if 'bar' returns a falsy value. Since the truthiness of bar's return value (if it halts) is a non-trivial property of the (partial) function it implements, it is undecidable for arbitrary 'bar' (via Rice's theorem). QED.

Yet in Java this question is trivially decidable, since all return values must have the same static type; i.e. procedures like the above aren't valid Java programs, and this can be determined statically, so they present no difficulties.

In this particular case, Java's static type system makes this a trivial question about the procedure's syntax; rather than a non-trivial question about the (partial) function it implements.

This same argument applies to all sorts of DSLs too. Many use a similar type-based approach, e.g. linear types forbid expressions like 'if (bar()) { free(myMemory); }'.

Others work by providing an extra semantics, alongside the normal result-calculating one; e.g. incremental lambda calculus has a semantics for calculating changes; differentiable languages (e.g. provided by machine learning libraries) have a semantics for calculating derivatives; probabilistic programming languages have a semantics for sampling and induction; etc. We generally can't apply these semantics to other languages, due to the existence of language constructs which don't exist in that semantics (e.g. exceptions, or GOTO, or whatever).

I thought you were talking about the actual problems - the ones that you use a programming language to solve.

But here it's really comparing apples vs oranges. Of course you can find questions that don't have a definitive answer for programs (or program parts) written in any programming language. Much more so in a less rigid language. That doesn't say anything about problem solving abilities, though.

> This same argument applies to all sorts of DSLs too. Many use a similar type-based approach, e.g. linear types forbid expressions like 'if (bar()) { free(myMemory); }'.

That's nice, but the concern I expressed in my original post is - at what cost?

Ah, I suppose there was a conflation between (roughly) "business problem" versus "computer science problem".

It's completely true that all Turing-complete languages can solve the same set of computer science problems (e.g. recognising certain grammars, implementing certain partial functions, etc.). Of course, actually coming up with such solutions can vary between e.g. Brainfuck versus Java.

I was focusing more on "real world problems" or "business problems", e.g. allowing users to query a server, or adding a plugin mechanism to a game, or distributing an application across multiple locations, etc. These are not "computer science problems" (akin to, say, recognising a grammar) since they're underspecified; we're free to make various choices about what counts as correct, including the input format.

These examples are particularly well-suited to solutions involving a language (e.g. a query language), as opposed to something less expressive (e.g. a pre-determined list of options). For such "real world problems" our choice of language can be the difference between a trivial solution or an undecidable quagmire. For example, in the case of querying we could give users a pure language (with a timeout); that's trivially safe from effects, as well as being immune to many side-channels (no shared state, etc.). If we instead allowed users to write queries using Python, we'd face the impossible task of detecting which programs are safe to run on our server (unless we only provide a safe sub-set of the language; which is just a round-about way of saying we should create a custom language!).

> the concern I expressed in my original post is - at what cost?

Yes, there's always a cost for these things. In my experience, this usually involves explicitly encoding our reasoning/assumptions into a form the language will accept (e.g. type annotations, if they can't be inferred; refactoring some generic loop to fit a certain pattern; etc.). However, that's not all bad, since our programs capture more of our intent, and will warn us if we're wrong (either immediately, or after some refactoring invalidates our assumptions).

These tradeoffs certainly exist on a spectrum, and the location of the "bang for buck" sweet spots varies depending on the domain. It's usually not worth encoding a correctness proof into Coq's type system; yet it usually is worth encoding our control flow into structured programming rather than GOTOs. There's a whole heap of techniques in between, with varying tradeoffs, which make more or less sense depending on the domain, external constraints, etc.

Nicely put! It's important to be aware of the spectrum ranging from very rigid and introspectable, to very flexible. We should not be religious about approaches, and it is certainly a good idea to consider new approaches. But there are other economic forces unrelated to this spectrum - for example, it can be a good idea to just stay with old and proven tech because of better tooling, compatibility and familiarity.