11 ms·

Instead of having to think about every possible way a language might be used and account for it up front, languages with good metaprogramming facilities let the

Instead of having to think about every possible way a language might be used and account for it up front, languages with good metaprogramming facilities let the users them to fit their needs. This way the core language can stay small and focused while remaining flexible. While you don’t want everybody building their own language, userland extensibility can play a huge impact on the overall cleanliness of the language because new ideas can be tried out as libraries. If these ideas don’t pan out, the community moves on. Projects using these libraries will keep working, but the core language doesn’t end up accumulating cruft. I wrote about that in detail here: https://yogthos.net/posts/2017-10-03-MovingForwardByLettingGo.html https://yogthos.net/posts/2017-10-03-MovingForwardByLettingG...

mcguire 9y ago
...which is why Scheme has, like, 37 different, incompatible object systems. Everything has costs.
- eadmund 9y ago
  That's Scheme. Lisp, meanwhile, has one: CLOS. One is excellent for learning about things like hand-rolled object systems, and one is excellent for building large systems.
  - iak8god 9y ago
    Common Lisp has CLOS. I'm aware some purists don't think Scheme is a Lisp but, regardless of one's stance on this, there are most definitely other Lisps than Common Lisp.
    - YouAreGreat 9y ago
      Having called the result of Lisp standardization ANSI Common Lisp instead of just ANSI Lisp doesn't change the fact that the whole effort was all about standardizing Lisp. Moreover, why not just say Scheme or Clojure when talking about Scheme or Clojure? If ANSI C had been called ANSI Common C, would Java fans never cease to insist on calling Java a dialect of C?
      - iak8god 9y ago
        > the whole effort was all about standardizing Lisp There are more Lisps now than ever, so perhaps that was not as successful as was hoped. > why not just say Scheme or Clojure when talking about Scheme or Clojure? Why not just say "Common Lisp" when you mean Common Lisp, and "Lisp" when making true general statements that include other things that have always been considered Lisps? How are we to refer to Emacs Lisp without tying ourselves in knots if we refuse to say that "Lisp" includes it?
- shakna 9y ago
  You say that, but SLIB [0] is the canonical place to go with Scheme, which has the "Macroless Object System" [1], based on CLOS from Common Lisp. SLIB is included with Guile, and compatible with almost all Schemes. If a Scheme has an object system inbuilt, it is likely to be built around SLIB's. [0] https://people.csail.mit.edu/jaffer/SLIB https://people.csail.mit.edu/jaffer/SLIB [1] https://people.csail.mit.edu/jaffer/slib/Object.html#Object https://people.csail.mit.edu/jaffer/slib/Object.html#Object
- yogthos 9y ago
  Sure, it's not a guarantee that the language will stay small and focused, but it provides a path towards that. Clojure has been around for a decade now, and the core language has grown very little. I think it helps that Clojure is a BDFL driven language as opposed to being a design by committee.
catnaroek 9y ago
> languages with good metaprogramming facilities let the users them to fit their needs. No amount of metaprogramming can fix the intractability of proving programs correct in the base language, especially if the metaprogramming facilities leak identifiers like a sieve (unhygienic macros). > userland extensibility can play a huge impact on the overall cleanliness of the language because new ideas can be tried out as libraries. Instead of (uselessly!) trying new language features, how about trying to find usable proof principles for the language features that you already have?
- nickpsecurity 9y ago
  "No amount of metaprogramming can fix the intractability of proving programs correct in the base language" It's actually rare people need to do proofs. If they do, they can also prove the programs correct with a tool suited for it like Isabelle/HOL or Coq then extract them to the desired language. It's worked for extractions to ML, Haskell, Scheme, and recently C (see below). https://staff.aist.go.jp/tanaka-akira/succinct/slide-pro114.pdf https://staff.aist.go.jp/tanaka-akira/succinct/slide-pro114.... There's also been verified LISP's (Scheme48, LISP 1.5) and metaprogramming constructs. So, it could be done in or for a LISP-like language with metaprogramming. I even found two metaprogramming schemes for Coq recently. https://popl18.sigplan.org/event/coqpl-2018-typed-template-coq https://popl18.sigplan.org/event/coqpl-2018-typed-template-c... https://hal.inria.fr/hal-01637063/document https://hal.inria.fr/hal-01637063/document That brings me back to an old idea I was just discussing with someone about SPARK. I've pushed for using all high-value/low-cost methods on highly-assured programs before using proof to avoid wasting time on stuff easy to prove wrong. Heavy hitters from Verisoft to Data61 have been coming around to that idea using Alloy and property-based testing of specs respectively. Many of these formal languages also have crappy tooling on FOSS side versus mainstream stuff. So, I suggested embedding them in something like Racket to: get the IDE and REPL benefits for productivity; use combo of Cleanroom-style development, Design-by-Contract, contract-based testing, combinatorial testing up to 6-way (3-way minimum), and fuzz testing with contracts running; extracting to Rust, C and/or SPARK w/ their static analyzers or model checkers run on that code; fix any problems in logic in original with repeats of that process as much as necessary; final result extracted to something with certifying compiler to knock out that risk. I called the concept Brute-Force Assurance given one just throws CPU power and low-cost labor at the problem without much specialist skill required past what DbC or SPARK needs. That combined with basic methods for high-availability or fault-tolerance plus recovery should make for one hell of a high assurance system at a fraction of the cost of formal verification. And if you wanted proof, then that system would already be nearly flawless to begin with in a structure (i.e. Cleanroom) amenable to easy proof with ability to extract to semantics of your choosing. If not Racket, I had K Framework used for KCC Executable Semantics for C in mind for formal alternative. Regardless, every tech I just cited (except SPARK) has low cost, lowers defects, and was easy to pick up. The combo should really bottom out defects without slowing time-to-market down too much to be useful. That's what formal proof did almost every time it was tried in normal development, esp if using 3rd party libraries.

mcguire 9y ago

...which is why Scheme has, like, 37 different, incompatible object systems. Everything has costs.

eadmund 9y ago
That's Scheme. Lisp, meanwhile, has one: CLOS. One is excellent for learning about things like hand-rolled object systems, and one is excellent for building large systems.
- iak8god 9y ago
  Common Lisp has CLOS. I'm aware some purists don't think Scheme is a Lisp but, regardless of one's stance on this, there are most definitely other Lisps than Common Lisp.
  - YouAreGreat 9y ago
    Having called the result of Lisp standardization ANSI Common Lisp instead of just ANSI Lisp doesn't change the fact that the whole effort was all about standardizing Lisp. Moreover, why not just say Scheme or Clojure when talking about Scheme or Clojure? If ANSI C had been called ANSI Common C, would Java fans never cease to insist on calling Java a dialect of C?
    - iak8god 9y ago
      > the whole effort was all about standardizing Lisp There are more Lisps now than ever, so perhaps that was not as successful as was hoped. > why not just say Scheme or Clojure when talking about Scheme or Clojure? Why not just say "Common Lisp" when you mean Common Lisp, and "Lisp" when making true general statements that include other things that have always been considered Lisps? How are we to refer to Emacs Lisp without tying ourselves in knots if we refuse to say that "Lisp" includes it?
shakna 9y ago
You say that, but SLIB [0] is the canonical place to go with Scheme, which has the "Macroless Object System" [1], based on CLOS from Common Lisp. SLIB is included with Guile, and compatible with almost all Schemes. If a Scheme has an object system inbuilt, it is likely to be built around SLIB's. [0] https://people.csail.mit.edu/jaffer/SLIB https://people.csail.mit.edu/jaffer/SLIB [1] https://people.csail.mit.edu/jaffer/slib/Object.html#Object https://people.csail.mit.edu/jaffer/slib/Object.html#Object
yogthos 9y ago
Sure, it's not a guarantee that the language will stay small and focused, but it provides a path towards that. Clojure has been around for a decade now, and the core language has grown very little. I think it helps that Clojure is a BDFL driven language as opposed to being a design by committee.

catnaroek 9y ago

> languages with good metaprogramming facilities let the users them to fit their needs. No amount of metaprogramming can fix the intractability of proving programs correct in the base language, especially if the metaprogramming facilities leak identifiers like a sieve (unhygienic macros). > userland extensibility can play a huge impact on the overall cleanliness of the language because new ideas can be tried out as libraries. Instead of (uselessly!) trying new language features, how about trying to find usable proof principles for the language features that you already have?

nickpsecurity 9y ago
"No amount of metaprogramming can fix the intractability of proving programs correct in the base language" It's actually rare people need to do proofs. If they do, they can also prove the programs correct with a tool suited for it like Isabelle/HOL or Coq then extract them to the desired language. It's worked for extractions to ML, Haskell, Scheme, and recently C (see below). https://staff.aist.go.jp/tanaka-akira/succinct/slide-pro114.pdf https://staff.aist.go.jp/tanaka-akira/succinct/slide-pro114.... There's also been verified LISP's (Scheme48, LISP 1.5) and metaprogramming constructs. So, it could be done in or for a LISP-like language with metaprogramming. I even found two metaprogramming schemes for Coq recently. https://popl18.sigplan.org/event/coqpl-2018-typed-template-coq https://popl18.sigplan.org/event/coqpl-2018-typed-template-c... https://hal.inria.fr/hal-01637063/document https://hal.inria.fr/hal-01637063/document That brings me back to an old idea I was just discussing with someone about SPARK. I've pushed for using all high-value/low-cost methods on highly-assured programs before using proof to avoid wasting time on stuff easy to prove wrong. Heavy hitters from Verisoft to Data61 have been coming around to that idea using Alloy and property-based testing of specs respectively. Many of these formal languages also have crappy tooling on FOSS side versus mainstream stuff. So, I suggested embedding them in something like Racket to: get the IDE and REPL benefits for productivity; use combo of Cleanroom-style development, Design-by-Contract, contract-based testing, combinatorial testing up to 6-way (3-way minimum), and fuzz testing with contracts running; extracting to Rust, C and/or SPARK w/ their static analyzers or model checkers run on that code; fix any problems in logic in original with repeats of that process as much as necessary; final result extracted to something with certifying compiler to knock out that risk. I called the concept Brute-Force Assurance given one just throws CPU power and low-cost labor at the problem without much specialist skill required past what DbC or SPARK needs. That combined with basic methods for high-availability or fault-tolerance plus recovery should make for one hell of a high assurance system at a fraction of the cost of formal verification. And if you wanted proof, then that system would already be nearly flawless to begin with in a structure (i.e. Cleanroom) amenable to easy proof with ability to extract to semantics of your choosing. If not Racket, I had K Framework used for KCC Executable Semantics for C in mind for formal alternative. Regardless, every tech I just cited (except SPARK) has low cost, lowers defects, and was easy to pick up. The combo should really bottom out defects without slowing time-to-market down too much to be useful. That's what formal proof did almost every time it was tried in normal development, esp if using 3rd party libraries.