4 ms·
Yeah clarity is nice but no, sometimes we want less power. Until some one invents the sufficiently oracular compiler power often prevents various effort saving
by Avshalom 11y ago
Yeah clarity is nice but no, sometimes we want less power.
Until some one invents the sufficiently oracular compiler power often prevents various effort saving/performance boosting tricks, which is what 2/3 of the article is giving evidence of. Also: formally verifiable code and static analysis.
- nickpsecurity 11y agoThe most powerful language I know of is LISP. Guess what one of most field-proven verification tools uses and verifies? LISP via ACL2. There were also hardware kits like DDD that did correct by construction hardware from LISP specs. So, power != hard to verify. One should subset, though, for best results.
- Avshalom 11y ago>One should subset, though, for best results. ... So giving up power produces better results?
- PeCaN 11y agoNaturally, 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 agoHard 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 agoGiving 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 agoAs 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 agoThe latter were my exact words here: https://news.ycombinator.com/item?id=10572044 https://news.ycombinator.com/item?id=10572044 (see second half)
- kd0amg 11y agoGuess what one of most field-proven verification tools uses and verifies? LISP via ACL2. The dialect of lisp that ACL2 verifies is not very powerful at all.
- nickpsecurity 11y agoIt can be integrated into LISP or transformed into forms of Turing complete languages. It doesn't have to be powerful to be used powerfully. :) Part of my recurring them that you can have both worlds.
- kd0amg 11y agoAny language's code can be integrated or transformed into some Turing-complete language. That doesn't make a language powerful. You don't see anyone raving about how amazing the language of variable-free arithmetic expressions is, but that's already integrated into most languages people would call "powerful." The idea that ACL2 verifies a powerful language is outright false. ACL2's verified language is stripped down (no first-class functions, nontermination, exceptions, etc.) because added power makes it too hard to verify.
- nickpsecurity 11y agoAlright I'll give you that. My main argument is for a language powerful enough for both solving problems concisely and creating DSL's should be used with DSL's for common or hard problems. The DSL's or the language can be subject to verification.