4 ms·

> Sigh. You can write undecidable programs, but you don't want to. What does “undecidable program” even mean? The label “undecidable” applies to decision probl

> Sigh. You can write undecidable programs, but you don't want to. What does “undecidable program” even mean? The label “undecidable” applies to decision problems: https://en.wikipedia.org/wiki/Decision_problem https://en.wikipedia.org/wiki/Decision_problem > If it can't decide if a driver is memory-safe and API safe in some number of minutes, it quits, and Microsoft won't sign the driver. About 5% of drivers hit this problem, and need some rewriting. We're talking about the universe of C++ programs that meet the Core Guidelines, not just drivers.

coldtea 10y ago
>What does “undecidable program” even mean? It's pretty clear what it means in this context, especially after the Halting problem was mentioned earlier in the thread, and the parent wrote about MS driver verification program "deciding whether a driver is memory-safe".
- catnaroek 10y ago
  > It's pretty clear what it means in this context Sorry, no. Imprecise use of jargon is one of the main ways how technical discussions get derailed. So I shall insist on precise use of terminology.
  - coldtea 10y ago
    >Imprecise use of jargon is one of the main ways how technical discussions get derailed. Yes. And the other main way is insistence on pointless pedantic distinctions.
    - catnaroek 10y ago
      To clarify: Given a general (co)recursively enumerable problem, it's possible to come up with several semi-deciders, which won't necessarily diverge on the same inputs. So, even if I charitably interpret “undecidable program” as “program for which a static analysis tool diverges or otherwise runs into trouble”, we still need to know what specific static analysis tool we're talking about, in order to talk about what programs will be problematic for the tool. Now, I'm aware that Animats mentioned a concrete static analysis tool, the Windows Static Driver Verifier. But, without any knowledge of the specifics of how it internally works, you can't design your program to pass the verification.

coldtea 10y ago

>What does “undecidable program” even mean? It's pretty clear what it means in this context, especially after the Halting problem was mentioned earlier in the thread, and the parent wrote about MS driver verification program "deciding whether a driver is memory-safe".

catnaroek 10y ago
> It's pretty clear what it means in this context Sorry, no. Imprecise use of jargon is one of the main ways how technical discussions get derailed. So I shall insist on precise use of terminology.
- coldtea 10y ago
  >Imprecise use of jargon is one of the main ways how technical discussions get derailed. Yes. And the other main way is insistence on pointless pedantic distinctions.
  - catnaroek 10y ago
    To clarify: Given a general (co)recursively enumerable problem, it's possible to come up with several semi-deciders, which won't necessarily diverge on the same inputs. So, even if I charitably interpret “undecidable program” as “program for which a static analysis tool diverges or otherwise runs into trouble”, we still need to know what specific static analysis tool we're talking about, in order to talk about what programs will be problematic for the tool. Now, I'm aware that Animats mentioned a concrete static analysis tool, the Windows Static Driver Verifier. But, without any knowledge of the specifics of how it internally works, you can't design your program to pass the verification.