3 ms·

> I gave you an example: Sieve. I said "of wide utility". BTW, I don't know Sieve, but if it has regular expressions then reasoning about it is also infeasible

• vidarh 9y ago
  > I said "of wide utility". And they are of wide utility, even though they may not satisfy your expectations to just how wide utility you want. But that is exactly the point - they're not meant to. The claim I made, and that others here have made, that you've been arguing against is not about general purpose languages. I've pointed that out several times. On the contrary the point is explicitly that there are benefits in isolating parts of problems and explicitly avoiding general purpose languages exactly because I agree that you won't gain much from trying to find weaker models for general purpose languages. So when you keep bringing up more general computation, you keep arguing against a point I at least have not made. I've never disputed that there is little to gain from trying to weaken the computational models for general purpose computation. What we can do, and often do is to reduce the practical problems of working on these systems by lifting subsets of problems out of general purpose languages and into much weaker special purpose environments. Since you keep bringing up regular expressions, for example: > but if it has regular expressions then reasoning about it is also infeasible ... this is exactly one of the reasons why Sieve doesn't have them (at least not the base language) - it's limited to basic wildcards ("","?", specific strings). On top of that the implementation is allowed to terminate execution after an implementation defined number of execution steps, so it does not need to even deal with the worst case for a wildcard engine if someone tries to feed it pathological strings. > I don't know what "a wide range of tasks" means, but even regular expressions are not limited enough for general reasoning. Anything that requires regular expressions and beyond is already infeasibly verified in the general case. I've repeatedly pointed out that the entire goal of these languages is to prevent* general reasoning. That is a feature, not a flaw. > No. I'm talking about arbitrary programs in whatever language you give me. ... in which case you're not addressing the comments of mine that you've replied to, and we're in violent agreement about something that is irrelevant to my argument.
  • pron 9y ago
    > What we can do, and often do is to reduce the practical problems of working on these systems by lifting subsets of problems out of general purpose languages and into much weaker special purpose environments. A language that has no variables, no loops and no subroutines (and no regexps) is as far as you can go while remaining feasibly verifiable. There aren't many other options. What portion of our applications can be written in such languages? That people add extensions to Sieve only shows that its trusted portion isn't widely-enough useful even for the task of filtering email. It's not a question of general-purpose vs. DSL. Regardless of what the language is for, with no loop, subroutines and variables there is very little you can do. > I've repeatedly pointed out that the entire goal of these languages is to prevent* general reasoning. That is a feature, not a flaw. It's not important, but that's not what I meant by general reasoning or arbitrary computation. What I meant is that no matter the language you give me (assuming it's useful enough etc.), answering arbitrary questions about arbitrary programs in that language is not feasible. For example, regular expressions do not allow "arbitrary computation" in the Turing completeness sense, yet it is infeasible to feasibly answer arbitrary questions about arbitrary regular expressions, such as the question "are two regular expressions equivalent?" This is a very important question about regular expressions, but it cannot be feasibly answered for arbitrary regular expressions.
    • vidarh 9y ago
      > A language that has no variables, no loops and no subroutines (and no regexps) is as far as you can go while remaining feasibly verifiable. There aren't many other options. What portion of our applications can be written in such languages? That people add extensions to Sieve only shows that its trusted portion isn't widely-enough useful even for the task of filtering email. Most extensions to Sieve still retain the same constraints. A few don't, sometimes because peoples needs are different: E.g. someone using it for their own mail server or a corporate mail server where it is possible to yell at the person who turned their mail script into a fork bomb has very different requirements from one that lets "anyone" sign up, for example. That's a good reason for why the extension mechanism is there. As for examples of other things you can do: There are a number of templating languages, for example, that can be demonstrated to always terminate and otherwise be feasible to reason about. I've personally written such template engines also because it was a useful way of preventing the developers from doing stupid things (the ingrates then tried to sneak in a directive to embed a perl interpreter behind my back at one point). You can do a lot more than you might think in such engines by e.g. providing primitives for filtering and iteration over nodes in input graphs (as long as you can't mutate the collections, and there are appropriate termination guarantees e.g. by preventing loops) Another highly useful example that springs to mind is BPF, which while it started as a basic packet filter (e.g. for tcpdump) is increasingly powering much more functionality on Linux for e.g. tracing, and such as for example kernel level enforcement of system call constraints (you can define filters to apply to subsequent code that e.g. outright rejects certain system calls, or applies comparisons to the system call arguments to decide whether to allow or reject them). But I'd say the question you're asking is the wrong one, though. The original point was that when approaching a problem, there is substantial value to be had by asking "how can I subdivide this problem so that as much as possible can be restricted to a less powerful subset?" The Rule of Least Power, basically. Often you will end up with dynamic subsets that are hard to reason about, but as part of the process you can usually confine the parts that are hard to reason about to a smaller portion of the code and reduce the magnitude of the problem, and gain the ability to reason about the rest. You don't even need to create full blown languages to get this effect - changing the way you write code and effectively create a DSL in the form of API's can often achieve the same effect, but isolating "dangerous" functionality to separate languages often makes it harder to violate the requirements. > It's not important, but that's not what I meant by general reasoning or arbitrary computation. What I meant is that no matter the language you give me (assuming it's useful enough etc.), answering arbitrary questions about arbitrary programs in that language is not feasible That'd be reasonable apart for setting it up for a No True Scotsman with your "assuming it's useful enough etc.". As we've seen with your objections to Sieve, the languages I'm talking about appears to be languages you don't find "useful enough." Since your objections applies to a different set of languages than those I'm talking about, your objections are moot.