[catnaroek]

> You can have weakly/dynamically typed functional languages (most lisps for example)

I would call Racket a functional language. Common Lisp? Nope.

> Haskell the language also knows nothing at all about invariants

I'm aware. But I'm not talking about mechanically enforcing equational laws. I'm talking about the ability to state them in the first place. For this, you need a sufficiently rich value language, where, for example, the list [1,2,3] is always the list [1,2,3] regardless of where it resides in memory.

In JavaScript, [1,2,3] isn't a list. It's an expression that, when evaluated, constructs an object whose initial value is one particular list, but its value at another point in time might be a different list. Furthermore, if you evaluate [1,2,3] twice, you get completely different objects. Although the objects are first-class, the list values aren't, so you can't (soundly) formulate any equational laws about lists. And object identities have an equational theory so weak (“everything is equal to itself and nothing else”) that it's completely useless.

[clarus]

I think in any cases you will have to define your notion of equality in the mathematical language you use. Indeed, even in Haskell, the equality operator returns a Haskell boolean but not a proposition, and cannot cope with equality on functions (I guess).

[catnaroek]

> I think in any cases you will have to define your notion of equality in the mathematical language you use.

The point is that I can reason about equality of ML and Haskell expressions in ML and Haskell themselves, with a few minor extensions (e.g., the usual laws of arithmetic, applied to pure `int` expressions), whereas reasoning about equivalence of JavaScript programs requires carrying out the entire reasoning process in a separate metalanguage. The latter is obviously far more tedious, which is why programmers have largely given up on actually reasoning about JavaScript programs, preferring testing as an alternative.

> Indeed, even in Haskell, the equality operator returns a Haskell boolean but not a proposition,

Equality testing (a runtime operation, only valid for types with decidable equality) is different from propositional equality (a type constructor on its own, which can be used on any type). See https://existentialtype.wordpress.com/2011/03/15/boolean-bli... for details. Haskell doesn't have a propositional equality type constructor.

> and cannot cope with equality on functions (I guess).

Indeed, and, in any higher-order language, this is a feature, not a bug.

[clarus]

> whereas reasoning about equivalence of JavaScript programs requires carrying out the entire reasoning process in a separate metalanguage

I do not see how you can reason about Haskell in Haskell either, as this is a programming language and not a proof language (maybe I am missing something?).

> Haskell doesn't have a propositional equality type constructor.

This is what I meant. Since with both Haskell and JavaScript you will need to define a propositional equality, in my experience this does not help that much to have a better decidable equality.

[catnaroek]

> I do not see how you can reason about Haskell in Haskell either, as this is a programming language and not a proof language (maybe I am missing something?).

http://www.haskellforall.com/2013/12/equational-reasoning.ht...

http://www.haskellforall.com/2014/07/equational-reasoning-at...

The reasoning is entirely carried out by replacing Haskell expressions with contextually equivalent ones.

> Since with both Haskell and JavaScript you will need to define a propositional equality

No, you need much more than a propositional equality to be able to reason about JavaScript programs. If you try to use Haskell-style equational reasoning on JavaScript objects, you can only pick between your reasoning being trivial (because every object reference is only equal to references to physically the same object) or unsound! So if you want a more useful notion of program equivalence, you'll have to use a separate logic (e.g. Hoare logic) or axiomatic system (e.g. Dijkstra's predicate transformer semantics) for reasoning about imperative programs.