> There is a general purpose programming model which supports verification at a very fine grained level, encompassing both computation and effects

Of course there is (synchronous programming), but it may not necessarily be the best fit for all situations, either, and FP may well be more appropriate for sequential programs. Personally, I don't have a problem with not using the "best" at all times. I do have a problem with insisting that some formalism is "best". Like Church wrote, there is simply no such thing.

> I'm a bit puzzled by why you're combative against the Haskell community

My only problem is with claims that either state that Haskell is universally/objectively superior to other approaches because it possesses some property or other or with claims that mistake features of a specific formalism with those of computation in general.

> How do we really get the feel for the benefits of this model? Sure, I can struggle through tutorials on TLA, white papers on Daedalus, and the Eve live demo, but from the little I've seen it's not yet obvious to me how they solve my problems as a day-to-day jobbing programmer.

That's OK. I'm not trying to sell you this approach or make you an advocate for it. I just want people to stop equating FP with "math", as it is certainly not the only "mathematical" approach to programming, nor make claims about its universal superiority.

> The benefits of Haskell, on the other hand, became clear to me after browsing the Haskell Reddit and noticing that pretty much every post solved a problem I was currently having in my Python codebase.

That's great! Haskell works great for some people in some cases, and may not be the best for everyone in every case. You can still advocate for Haskell and tell people how elegant you find the approach and how well it solved your problems. Just don't make universal claims that can't be backed up.

> Does the model you're describing really handle polymorphism and higher order functions?

Polymorphism and higher-order functions are not concepts in computation; they're concepts in functional programming. A model where computations are not represented as functions, obviously has other means of expressing things. For example, dynamical systems are normally expressed using first-order ODEs only, but they can still express any system, even one where the derivative is itself a dynamical process, and so you'd think is a "higher order" system. When you have forms of composition other than function composition, your objects are just different.

Having said that, TLA+ has polymorphism and higher-order functions (only that's not how you represent computation).

> Given that polymorphism and higher order functions are known to be incompatible with set theoretic models I remain sceptical.

I assume you referring to TLA+, which uses set theory as the "data logic". When people say that polymorphism doesn't have a set-theoretic model, they mean that a polymorphic function, say `id :: a -> a`, cannot correspond to a set theoretic function. That doesn't mean it cannot be represented as something else. But, as you're talking about set theory, and so, I assume, referring to formal methods like TLA+, I have to say that I'm not sure at all what the status of polymorphism is in type-theory based proof assistants, which, like TLA+ but unlike Haskell, must be consistent. For example, in Lean, the id "function is:

universe u
def id {α : Sort u} (x : α) := x

Now, even after playing with Lean for a few weeks, I'm still not sure what kind of object `id` is, but I'm pretty sure it cannot be a function. The reason for that universe thing is that, unlike in Haskell, you cannot have a type of all types, as, just like in set theory, this leads to contradiction. That is the reason polymorphic "functions" are not set-theoretic functions, but I'm not sure they're type theoretic functions, either. On the other hand, you can have a function that is polymorphic not over all types, but over all types of a certain universe that doesn't include the type of the function itself, but you certainly can represent a polymorphic function like that as a set-theoretic function. So, set theories and type theories are consistent theories, and while I'm not a logician and I could be very wrong about this, I believe that types in consistent type theories do have set models (I know that's the case for Lean, at least).

BTW, if you want to write something similar to the above Lean definition in TLA+, you'd write:

Id(u) ≜ [x ∈ u ↦ x]

and use it as `Id(Nat)[5]` -- just like in Lean, except the type is not inferred. Of course, you wouldn't do that in practice, as you could simply define

Id(x) = x

which is polymorphic over all sets. It can do that because it's not a function but an operator.