3 ms·
Shen seems pretty cool, but there are lots of other things out there that are also cool. When licensing is such a big deal, I think its bizarre license is reaso
by JoelMcCracken 14y ago
Shen seems pretty cool, but there are lots of other things out there that are also cool. When licensing is such a big deal, I think its bizarre license is reason to steer away from Shen.
It not being "free software" is pretty debatable imo. Maybe not free with a capitol f, but free enough as an academic language.
- kd0amg 14y agofree enough as an academic language Constructing derivatives of other languages is a pretty common thing for PL academics to do.
- mjn 14y agoFor better or worse, it's not that uncommon for licenses to complicate it. To take one prominent example, Microsoft Research's Z3 is completely proprietary: source-code is available but you cannot make any derivative works of it (except in-house without distribution). The famous Q array-processing language is also completely proprietary. Less restrictively, it's common for things to be released under an "academic use only" or "noncommercial use only" license.
- kd0amg 14y agoAnd the papers I've read about array languages don't base their languages on Q. I haven't done much reading on theorem provers, but I suspect I'll see a lot more papers about things derived from ACL2 or Coq than from Z3.