4 ms·

The most optimistic summary of your argument that I can produce is "There is a general purpose programming model which supports verification at a very fine grai

• pron 9y ago
  > 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.
  • tome 9y ago
    > > 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) So you say! And I'm keeping an open mind on it but I still don't grasp what it's useful for in the life of a day-to-day jobbing programmer like myself. > Polymorphism and higher-order functions are not concepts in computation Let's leave polymorphism to one side for a moment, but higher-order "programming"/"computation"/whatever is definitely a concept that's more widely applicable than just in functional programming. Any time you "manipulate a computation" you are doing "higher-order" computation. The universal Turing machine is an example of "higher-order" computation and the proof of the halting lemma requires "higher-order" computation. Now it's possible that the models you are describing do not allow you to abstract over computation and thus are not "higher-order". If that's the case then either they are weaker than needed to talk about computation in general or they are very remarkable demonstrations that higher-order computation is generally not needed in practice!
    • pron 9y ago
      > Any time you "manipulate a computation" you are doing "higher-order" computation. Ah, this is something I specifically address in my TLA+ post series, probably because I heard it come up from you and others. Higher-order is strictly a formal property, i.e., it is a quality of a description of a system, not of a system itself. The best example is from continuous dynamical system. If the derivative of a system is a dynamical system itself, using one formalization you get a higher-order ODE. But people usually prefer describing all dynamical systems using first-order ODEs. The system of equations is first-order, but it still describes a "system that modifies a system". How? Because the "higher-order" function composition can be expressed as first-order composition of a different kind. Instead of writing: x'' = 2 you can write: x' = y ∧ y' = 2 So this first-order composition corresponds to a higher order system in a world with only one variable. You don't even have to take my word about TLA. Robin Milner, who was one of the leading advocates and theoreticians of functional programming, moved in the eighties from the lambda calculus to process calculi. He still insisted on algebraic composition, but process calculi are "first-order" yet still equivalent to the lambda calculus. Instead of a function taking a function, you have two processes composed in parallel. > Now it's possible that the models you are describing do not allow you to abstract over computation and thus are not "higher-order". If that's the case then either they are weaker than needed to talk about computation in general or they are very remarkable demonstrations that higher-order computation is generally not needed in practice! Not only do they allow to abstract over computation, they organize all computations into a lattice. I.e. if computation b is an abstraction of a (or a is a refinement of b), then a ≤ b in the lattice. So instead of saying that b is a parameterized computation, and that there exists some x s.t. a = b(x), we have that nice order relation; order and nondeterminism are used instead of parameterization. In fact, in TLA this is even used for first-order computations. Instead of saying that F is a computation parameterized by some natural number parameter, we say that F has a "degree of nondeterminism freedom" of a dimension of natural numbers. That's one of the greatest strengths of such formalisms, as this greatly simplifies formal verification (and one of the reasons why synchronous languages are the languages most amenable so far to formal verification).
• hwayne 9y ago
  > 1. 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. 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. With respect to TLA+, here's how I'd say it solves problem as a day-to-day jobbing programmer: you know the saying "Weeks of programming can save you hours of planning?" TLA+ is a tool to make planning less tedious and error prone. You can write your plan as a specification, then check if that specification actually meets your required invariants. If you're expecting to write a couple dozen lines of code, TLA+ is probably not gonna help a lot. If you're expecting to write a couple thousand lines of code, it can save you a ton of pain. But you still have to implement your specification correctly, and that's where things like ADTs can help quite a lot.