3 ms·

>One should subset, though, for best results. ... So giving up power produces better results?

by Avshalom 11y ago

PeCaN 11y ago
Naturally, if you give up Turing completeness, you can have excellent 100% verified results. Sometimes yeah, it's easier to prove things about simpler systems.
nickpsecurity 11y ago
Hard to say as nobody has pushed it to the full extent. Giving up complexity gets better results for verification. So, you use a simple subset of the powerful language. That subset might still be more powerful than many languages but a bit less powerful and complex than the original. Complexity, ease of modelling, and state explosion are the real issues in verification.
angelbob 11y ago
Giving up power makes it easier to write good tools. That's one reason that IDE support for Java is amazing, but IDE support for JavaScript isn't nearly as good - JavaScript allows and encourages way more freeform do-it-however runtime unverified stuff. Java locks everything down with a lot more "must be compile time" and static type system conventions. You can permit the dynamic stuff as an alternative (as Java more or less does.) But if people actually use it, it screws up the tools' ability to introspect into your code. As a result, less-dynamic formats like HTML and CSS get better tooling, as a rule, because the tools have an easier job to do. And highly-dynamic languages like JavaScript and Ruby have terrible tools support, because they make the tools' lives quite difficult because of their language and library design.
- spion 11y ago
  As you can clearly see from your example, power is entirely different from being amendable to tooling and static analysis. This whole thing is just a false dichotomy.
  - nickpsecurity 11y ago
    The latter were my exact words here: https://news.ycombinator.com/item?id=10572044 https://news.ycombinator.com/item?id=10572044 (see second half)

3 ms·

>One should subset, though, for best results. ... So giving up power produces better results?

by Avshalom 11y ago

>One should subset, though, for best results. ... So giving up power produces better results?

PeCaN 11y ago
Naturally, if you give up Turing completeness, you can have excellent 100% verified results. Sometimes yeah, it's easier to prove things about simpler systems.
nickpsecurity 11y ago
Hard to say as nobody has pushed it to the full extent. Giving up complexity gets better results for verification. So, you use a simple subset of the powerful language. That subset might still be more powerful than many languages but a bit less powerful and complex than the original. Complexity, ease of modelling, and state explosion are the real issues in verification.
angelbob 11y ago
Giving up power makes it easier to write good tools. That's one reason that IDE support for Java is amazing, but IDE support for JavaScript isn't nearly as good - JavaScript allows and encourages way more freeform do-it-however runtime unverified stuff. Java locks everything down with a lot more "must be compile time" and static type system conventions. You can permit the dynamic stuff as an alternative (as Java more or less does.) But if people actually use it, it screws up the tools' ability to introspect into your code. As a result, less-dynamic formats like HTML and CSS get better tooling, as a rule, because the tools have an easier job to do. And highly-dynamic languages like JavaScript and Ruby have terrible tools support, because they make the tools' lives quite difficult because of their language and library design.
- spion 11y ago
  As you can clearly see from your example, power is entirely different from being amendable to tooling and static analysis. This whole thing is just a false dichotomy.
  - nickpsecurity 11y ago
    The latter were my exact words here: https://news.ycombinator.com/item?id=10572044 https://news.ycombinator.com/item?id=10572044 (see second half)