Unityping. Now every useful function is automatically not total!
> I find it has very clean semantics; it is strongly typed
Of course it is strongly typed! All expressions have type Univ.
> programs are commonly written in a way that preserves referential transparency
All my C++ programs are commonly written in a way that preserves referential transparency, and clearly distinguishes between objects that are meant to be mutated (non-const) from those that are not meant to (const). That still does not make C++ a pleasant language to program in.
> The limited dynamic scope may be somewhat unpleasant though, but that's its flexibility.
Spooky action at a distance. Me no like. :-(
> As for macros, they are merely functions that transform expressions. They can be somewhat unpleasant to read, but they are basically that.
Meh. The only total languages are used for formal verification, you'll always have to settle for less to get Turing-completeness.
> Of course it is strongly typed! All expressions have type Univ.
Have you used PHP? You'll come to appreciate the differences between the different "unityped" languages.
> All my C++ programs are commonly written in a way that preserves referential transparency, and clearly distinguishes between objects that are meant to be mutated (non-const) from those that are not meant to (const). That still does not make C++ a pleasant language to program in.
Does that say anything about Lisp? Nope, not at all. It isn't like C++ is comparable to Lisp, despite the efforts put by C++ programmers to wrest safety from a language designed as a superset of the language of cowboy-coders par excellence, its true nature as an imperative language with raw pointers may rear its head at any point. Not to say that Lisp has had more facilities up to this point than C++ to write referentially transparent programs.
> Spooky action at a distance. Me no like. :-(
Depends on the Lisp. Common Lisp's global variables are mutable and dynamic. Me no like either. In Racket and Clojure you can declare variables to be explicitly dynamic, and they can be rebound within special blocks, locally, sort of. Not that it's something anyone should use frequently.
Unityping. Now every useful function is automatically not total!
> I find it has very clean semantics; it is strongly typed
Of course it is strongly typed! All expressions have type Univ.
> programs are commonly written in a way that preserves referential transparency
All my C++ programs are commonly written in a way that preserves referential transparency, and clearly distinguishes between objects that are meant to be mutated (non-const) from those that are not meant to (const). That still does not make C++ a pleasant language to program in.
> The limited dynamic scope may be somewhat unpleasant though, but that's its flexibility.
Spooky action at a distance. Me no like. :-(
> As for macros, they are merely functions that transform expressions. They can be somewhat unpleasant to read, but they are basically that.
Will the result typecheck?