Are there any languages that automatically (as in, deliberately) lend themselves to automated error detection? I feel like it's either not possible or so possible that Haskell is the answer.
* static (not necessarily explicit) typing
* no dynamic metaprogramming (static OK)
* no "eval"
* no first-class functions (second-class OK)
* no prototype-based OOP (class-based OK)
* no mutable variables (lexical shadowing OK)
* no mutable values, or very strict aliasing rules
* no unbounded recursion
* no dynamically defined structures
Of course you can perform useful static analysis with only some of these guidelines met. e.g. Erlang's Dialyzer does pretty well with dynamic typing, first-class functions, and unbounded recursion, because these features generally aren't abused in Erlang. (Though this took a hit recently due to the recent introduction of the `maps` feature, which was designed in such a way as to encourage violating that last guideline, despite proposals for a similar feature which would not have violated it.)
Surprisingly, C also meets all but two of these guidelines, and, although it is an egregious violator of those both, it is somewhat amenable to static analysis (see Coverity).
JavaScript, on the other hand, is notoriously difficult to statically analyze, since it not only permits code to violate all the above guidelines, but it's common for code to violate all of them.
On that topic though, it is notable that Erlang's Dialyzer, unlike most static analysis tools and type systems, guarantees no false positives; it only reports errors via code paths it can prove are taken. This makes it very easy to integrate into existing development workflows.
[1] https://en.wikipedia.org/wiki/Cyclone_(programming_language)
[2] https://en.wikipedia.org/wiki/SPARK_(programming_language)
As a person who works at a large organisation focused on correctness, there are some crazy intersections between what "error" means, what programs do, and how humans work. In general, if you can clearly define what "error" means, you can mostly solve it with a sufficiently good language. That is not so easy.
The "automatic"[1] hammers we seem to have are good type systems and "Design By Contract" (think Eiffel, but having a strong proof assistant is a much more powerful case). In this case, I'm discussing the problem from a security point of view:
Some examples in order of difficulty:
* Process errors outside software; OK, these are usually not the programmer's fault. For example, Amazon account hijacking via customer service. No way to point-fix; DBC or typing won't help you.
* Software interaction with humans; I've seen regexes to disallow shipping (e.g. for identity documents) to P.O boxes, which allow the input "POSTAL BOX" rather than a variant of "PO BOX", "P.O BOX", "POSTAL BOX", "LOCKED BAG" or so on. The problem is that the data will be eventually interpreted by a human, who will correct the error and ensure delivery. AFAICT not fixable with DBC or typing - you need a business process improvement here.
* Ambient or environmental changes. The call you used to make to a third-party library or binary was secure, but now it isn't. For example, your app used RC4 or $RANDOM_BINARY, and it used to be secure, but now it isn't because your environment changed out from under you. Now your code needs a countermeasure or a fix.
* Subtle business logic errors such as missing a permissions check on private profile or data views - probably only fixable with proof or DBC, type system is not the right hammer here although maybe with effort you can sort of do it. Probably encoding rapidly changing business rules into your types is not a good idea though.
* Obvious business logic errors, e.g. allowing -1 books to be ordered in an online store; fixable with a good type system or DBC. (e.g. type "Quantity" is a natural number rather than a machine type).
* XSS or SQLI - should be fixed by type system alone in a sufficiently advanced language.
It's mostly the relatively trivial stuff at the bottom of this stack of possible errors which is fixable by good programming languages, assuming of course that your DBC logic or way you structure your typing is correct.
As a total aside, what would be really interesting to me would be a powerful "business process definition language", which could map data flow between systems and humans - and actually describe the real-world information flows when a user contacts customer support to reset their password. If that could interact with contracts or proofs in individual applications, my world would be rocked.
[1] Not requiring humans to check when changes happen, although obviously human effort is required during system definition.