5 ms·

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 possib

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.

jldugger 11y ago
Sure -- C is a great way to let programmers produce error ridden code that compiles.
colanderman 11y ago
Certain languages lend themselves better to static analysis than others. Some qualities (there are others) that simplify static analysis include: * 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.
- coderdude 11y ago
  Thanks for that response. I didnt expect to get that much useful information.
- apaprocki 11y ago
  Even though static analysis of C/C++ works reasonably well in Coverity (at least enough to buy and use the product), there are enough false positives and corner cases that make the thought of "automatic" fixes unrealistic. It finds serious bugs but it also gets tripped up on certain patterns without modeling or embedding pseudo-pragmas for it to process.
  - colanderman 11y ago
    Yes I know. But parent was asking about detection, not correction (which the OP is about). 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.
- Splines 11y ago
  Pardon if this is a naive question, but are there languages designed with static analysis in mind?
  - tormeh 11y ago
    Kotlin, designed by the Intellij-people. Maybe Ceylon? Don't remember.
  - tormeh 11y ago
    Kotlin, designed by the Intellij-people. Maybe Ceylon? Don't remember.
  - colanderman 11y ago
    There are, but they're not too widely used. Cyclone [1] and SPARK [2] are two examples. Of course many others may have been designed in such a way that they are easily analyzable, without that explicitly being a goal. [1] https://en.wikipedia.org/wiki/Cyclone_(programming_language) https://en.wikipedia.org/wiki/Cyclone_(programming_language) [2] https://en.wikipedia.org/wiki/SPARK_(programming_language) https://en.wikipedia.org/wiki/SPARK_(programming_language)
- riyadparvez 11y ago
  What is wrong with first-class functions other than function-pointer indirect jumps? If that is the problem, then polymorphism (virtual functions) should also be in the list.
xyzzy123 11y ago
I think it depends on what you mean by "error". Certainly Haskell is not a silver bullet here. 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.
krylon 11y ago
There is a subset of Ada called SPARK that is intended to allow for at least some degree of automated formal verification. Which is not quite the same as automated error detection, but I would assume if your code passes the verification, the chance of bugs hiding in it is pretty much nil (assuming, of course, the verifier is not buggy itself).

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.

jldugger 11y ago

Sure -- C is a great way to let programmers produce error ridden code that compiles.

colanderman 11y ago

Certain languages lend themselves better to static analysis than others. Some qualities (there are others) that simplify static analysis include: * 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.

coderdude 11y ago
Thanks for that response. I didnt expect to get that much useful information.
apaprocki 11y ago
Even though static analysis of C/C++ works reasonably well in Coverity (at least enough to buy and use the product), there are enough false positives and corner cases that make the thought of "automatic" fixes unrealistic. It finds serious bugs but it also gets tripped up on certain patterns without modeling or embedding pseudo-pragmas for it to process.
- colanderman 11y ago
  Yes I know. But parent was asking about detection, not correction (which the OP is about). 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.
Splines 11y ago
Pardon if this is a naive question, but are there languages designed with static analysis in mind?
- tormeh 11y ago
  Kotlin, designed by the Intellij-people. Maybe Ceylon? Don't remember.
- tormeh 11y ago
  Kotlin, designed by the Intellij-people. Maybe Ceylon? Don't remember.
- colanderman 11y ago
  There are, but they're not too widely used. Cyclone [1] and SPARK [2] are two examples. Of course many others may have been designed in such a way that they are easily analyzable, without that explicitly being a goal. [1] https://en.wikipedia.org/wiki/Cyclone_(programming_language) https://en.wikipedia.org/wiki/Cyclone_(programming_language) [2] https://en.wikipedia.org/wiki/SPARK_(programming_language) https://en.wikipedia.org/wiki/SPARK_(programming_language)
riyadparvez 11y ago
What is wrong with first-class functions other than function-pointer indirect jumps? If that is the problem, then polymorphism (virtual functions) should also be in the list.

xyzzy123 11y ago

I think it depends on what you mean by "error". Certainly Haskell is not a silver bullet here. 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.

krylon 11y ago

There is a subset of Ada called SPARK that is intended to allow for at least some degree of automated formal verification. Which is not quite the same as automated error detection, but I would assume if your code passes the verification, the chance of bugs hiding in it is pretty much nil (assuming, of course, the verifier is not buggy itself).