Of course it's true. There's a surjection from behivours to partial functions. Proving things about denotational semantics is obviously easier than proving things about operational semantics. It's just less useful.
> > I can't believe that state-based reasoning could ever displace expression-based reasoning, since (as seen in your own talk examples) even very short expressions can correspond to absolutely enormous spaces of possible states.
> This is just mathematically wrong, because if you think of the cardinality of functions you'd realize that it's the same as (normally bigger, actually) than that of sequences (e.g. the set of functions from the natural numbers to the natural numbers is exactly that of sequences of natural numbers).
I think you must have misunderstood. Here's a simple example. There are finitely many partial functions between finite sets A and B but infinitely many sequences of state transitions that take states in A to states in B.
TLA+ isn't, like, a 'better Haskell'. It's more of a 'better UML' or 'a better sack of flowcharts', especially when you are dealing with concurrency. It's an exhaustive checker on the spec.
You _can_ use it in the way pron is talking about, but that's not how most people outside academia use it that way.
I dislike the notion of "better" altogether when it comes to software. My point is that FP is not the only nor the most convenient way to reason about software. It has pros and cons, like any other approach; it sometimes very elegant, and sometimes less so. Preference is determined largely by a personal aesthetic preference. I have no qualms whatsoever with those who are more aesthetically drawn to the functional representation of programs. I have a problem with those claiming it is superior to other approaches without any reasonable justification. I am also extremely opposed to claims that people who prefer a non-pure-FP programming language over Haskell do that only because they don't know better. There are very good reasons to prefer either, and they're almost never universal, but depend both on the domain and the team.
Also, I'm not comparing TLA+ to Haskell, but rather TLA+ to Lean/Coq, and Eve to Haskell. Synchronous programming languages like Eve (or Esterel/SCADE for realtime systems) are to TLA+ what Haskell is to Lean/Agda (roughly).
> You _can_ use it in the way pron is talking about, but that's not how most people outside academia use it that way.
I think that you'll find that once you start specifying complex systems (like a distributed database), the refinement relations is extremely useful (in fact, pretty much essential), and is used in practice often (for whatever definition of often is reasonable for formal methods). It makes model-checking (and proofs, but those are rarely used outside academia) much more tractable. I used three levels of refinement, with refinement maps between them, when specifying a distributed database.
Refinement is the killer-feature that allows TLA+ to scale. For simple algorithms it is indeed overkill.
No, it is false. If all your functions were on simple types, then you would be correct (although the cardinality is still the same), but in order to express some programs using function semantics, you need to have higher-order functions, which vastly increase your state space.
> Proving things about denotational semantics is obviously easier than proving things about operational semantics. It's just less useful.
Again, what operational and denotational semantics are depends entirely on the formalism. The operational semantics of TLA don't even express the computation at all.
> There are finitely many partial functions between finite sets A and B but infinitely many sequences of state transitions that take states in A to states in B.
But the sequences exist in a lattice! I'm being very imprecise (to say the least; this is actually wrong, but conveys the idea) here, but just to give you an intuition, the sequence <1, 5, 6, 7, 8, 12, 0, 2, 1, 8, 6> is "smaller" in the lattice than the sequence <1, 6>. If your proposition is true for the latter, it is automatically true for the former. You never work with all possible sequences. In fact, there are infinite levels of them. Between any two states in a TLA+ behavior, there is an unbounded (yet finite) number of other states that are implicitly ignored. So what? The "state space" of which you reason is exactly the same as that of a "function" (assuming the function has enough information to prove the proposition, i.e., that it's not about complexity etc.).
> Be careful to pay attention to what lmm actually claimed. The claim was about "proof of properties of program fragments ... in "normal" industrial code ... ordinary webapps".
AFAIK, the only industrial grade, web programs etc., for which formal methods are used are Amazons AWS and some of Oracle's web services, that use TLA+. Whether or not someone uses Haskell, Haskell simply falls too short of "formal methods".
> Any language is referentially transparent if every expression is only denotationally equal to itself.
No, that's just not true. The only way that would work is if your denotation is the syntax itself, and that's just not what people mean when they talk about semantics in general. Template Haskell and Lisp are not referentially transparent. Regardless of what the denotation of term a is, you cannot replace it with any term b having the same denotation (and one exists unless your "denotation" is the syntax) while preserving the denotation of the complete expression.
> claiming the Java is referentially transparent is almost vacuous.
Except that the person who claimed it was Christopher Strachey in a seminal paper of programming language theory. No, it is not vacuous in the least.
> From there we conclude that Haskell's is more useful.
I know you very strongly believe that (and I do not), but there's neither the theoretical justification nor the empirical evidence (at least so far) to support that. From the fact that you can assign simple and clear semantics to some kinds of computation you most certainly cannot conclude that the formalism is more useful in general. It all comes down to aesthetics and pragmatics. You like Haskell better than Java (and I like Java better than Haskell), and you are more productive in Haskell than Java (and I'm more productive in Java). That's all. Unless we have evidence of either being universally more productive than the other, we simply cannot make such claims. And that's OK! You can evangelize Haskell showing people what you like about it and why you think it's great. I just don't like these sweeping claims that have no justification. This applies to everything, BTW, even to Scheme, ML, Java and TLA+ -- all of which I really like. I can rarely if ever bring myself to believe that some approach to software is universally (or close to it) better than others, unless there is some very compelling evidence.
> Do you know the precise time in the video?
No. I remember Leroy mentioning it at the very beginning, and then they discuss it at some later point, as well.
The info you have provided about TLA+ is extremely useful and I hope you can see that I have made a good faith effort to understand your point of view. However, I do not feel an equal effort back towards my position, so I'm afraid I'll have to leave it there.
> This is 100% false. Haskell's type system (without clever tricks such as singleton types) is so weak that the properties it "verifies" fall far, far below what is normally regarded as "formal verification".
Be careful to pay attention to what lmm actually claimed. The claim was about "proof of properties of program fragments ... in "normal" industrial code ... ordinary webapps".
Well of course, as long as you make the denotation fine grained enough! Any language is referentially transparent if every expression is only denotationally equal to itself. The point is that Haskell's equational theory is very rich and Java's isn't. From there we conclude that Haskell's is more useful. Whether it's useful enough is another issue, but claiming the Java is referentially transparent is almost vacuous.
> [4]: http://homepages.inf.ed.ac.uk/stg/Milner2012/Monday_Panel-ht....
To you know the precise time in the video?
Fundamentally, many pairs of real programs are equivalent at a coarse level and inequivalent at a finer level, so no formalism could ever escape that. We might have analysed programs X and Y in terms of their input and output and concluded they both print the same output when given the same input. But X uses mergesort and Y uses bubblesort. If we now want to compare the runtime of X and Y, we can't reuse our analysis, because fragments that we previously considered equivalent are no longer equivalent, symmetries that we previously made use of are now broken. The only way a formalism could let us reuse our analysis is if that formalism made us do all the work we'd do to compare the runtime even when we only want to compare the output. There's an excluded middle here.
> For one, the lambda calculus alone does not really describe a computation. Only a lambda expression combined with a state-machine -- i.e., an evaluation strategy -- defines a computation.
You do indeed need a description of how the computation is performed - an operational semantics - but state machines are not the only form of computation. For the lambda calculus reduction is evaluation - what you did in https://news.ycombinator.com/item?id=15786021 was computation, with no state machine in sight. The whole point of the Church-Turing thesis is that state machines and expression reduction are equivalent descriptions of computation.
> this style allows you to write your program however you like, and only then prove things about it, rather than write it with specific properties in mind (e.g., if you want to prove worst-case complexity, you must either write your program as a monad or use types that include a cost model).
This attitude has never made sense to me. Of course I'm writing my program with specific properties in mind - I'm not just writing some random program and then seeing what properties it has, I'm writing the program because I need a program with certain properties. If I've got a requirement for a particular worst-case complexity, I can't write any useful subcomponents without thinking about worst-case complexity; I want worst-case complexity to be visible for every line I write, as soon as I write it.
> A "term-reduction system", more commonly called an abstract rewriting system, is also a state machine.
No it isn't. It's a different formalism for describing computation, per Church-Turing. You can simulate one with the other, but neither subsumes the other; a rewriting system isn't a state machine any more than a state machine is a rewriting system.
> You get that anyway. Even in Java. That was precisely what Christopher Strachey showed when he first introduced the term "referential transparency" to programming languages[1] -- that imperative languages are referentially transparent. In Java, if you have an expression e, you can replace any sub expression, x, with another y, that has the same denotation, without changing the denotation of e. The difference between Java, Haskell and TLA is just what that denotation is. In Haskell, it is a "partial function"; in Java it's a predicate transformer [3] (i.e., a Hoare triplet); in TLA it's a set of sequences. This choice has both aesthetic and prgamatic consequences. I completely agree that the functional denotation and the behavior denotation are both normally more convenient than a Hoare triplet.
Any collection of symbols can be given a trivial "denotational semantics", but this "denotational semantics of Java" would not capture the things that make Java Java, because the relations between "expressions" (which would not correspond to Java expressions) bear no relation to the definition of Java-as-it's-usually-understood, the denotations of Java functions would not be functions. To be able to meaningfully talk about denotational semantics for a language, the semantics of a sequence of symbols in our denotation should match the way the sequence of symbols is understood by a reader, otherwise we just have two different languages that use the same symbols - and I don't think most people would read a line of Java and understand it to mean a Hoare triple. I'm not even convinced you've produced something compositional (GCL programs are just sequences of statements and can be composed by concatenation, so the Hoare triple semantics is valid for them, but Java programs are not structured that way), so it may not be a denotational semantics at all.
> you always "work on terms" when working syntactically
Exactly - what I'm saying is I want a toolset that makes it easy to work syntactically. I want referential transparency in terms of the common-sense meaning of the syntax, not in terms of some contrived meaning that exists only for analysis. I want a denotational semantics where things that look like function application denote function application, things that look like equality denote equality, and so on.
> It is 100% false that a semantic domain of partial functions makes your state space in any way smaller than if your semantics domain is sets of behaviors.
There are only 9 possible partial functions of type Boolean => Boolean, whereas there's a combinatorially huge number of possible behaviours. But most of the time I don't even have to reason about the specifics of a function, because just knowing that it is a function - that applying it to the same input always means its return value when applied to that input - provides me with enough information to greatly simplify the space of possibilities to think about. If I have some code like:
{
val a = f(2, 4, 5)
g(a, a)
}
g(f(2, 4, 5), f(2, 4, 5))
> Haskell's type system (without clever tricks such as singleton types) is so weak that the properties it "verifies" fall far, far below what is normally regarded as "formal verification".
Be that as it may, what I said stands: properties of program fragments are formally proven, in a verified way, in normal industrial code, every day using Haskell-like type systems. No other approach can say that; Eve may be aiming for mainstream but it's nowhere near as mainstream as Haskell. I'm a lot more confident in our ability extend that approach to cover the properties we care about, than in our ability to get the overhead of state-oriented approaches low enough to use for normal industrial code.
> This is just mathematically wrong, because if you think of the cardinality of functions you'd realize that it's the same as (normally bigger, actually) than that of sequences (e.g. the set of functions from the natural numbers to the natural numbers is exactly that of sequences of natural numbers).
Just thinking about sequences of state operations doesn't tell me enough to understand a program; I can't understand the composition of two sequences of state operations without understanding the full state. Whereas to understand the composition of two functions I only have to understand the return value of the first function, and that's generally taken from a much smaller space of possibilities than the space of possible program states. (Of course a state operation is equivalent to a function from program state to program state, and such functions would be just as hard to understand as state operations - but most functions are defined on much smaller spaces).
> Here are Xavier Leroy and Simon-Peyton Jones bemoan that the state of formal methods in FP is so far behind that of even "classical" imperative programming languages [4].
I don't do videos; I'll happily read written stuff but that talk didn't seem to be listed in the slides section of that site.
You keep saying that, but TLA is a formalism specifically designed to do just that. It defines a lattice of algorithms, where one is "smaller" than another if it is a refinement of it.
> If we now want to compare the runtime of X and Y, we can't reuse our analysis, because fragments that we previously considered equivalent are no longer equivalent, symmetries that we previously made use of are now broken.
No, that's not true, because equality and equivalence aren't the same. You can work with an equivalence relation knowing full well there are finer equivalences (think, e.g. of quotient types). In fact, in a partial order (like a lattice), for every element a, we can define an equivalence relation ~a, s.t. x ~a y iff x ≤ a and y ≤ a, i.e., all elements less than a are ~a-equivalent. You can work with programs like that, saying, e.g., that a is "any program that sorts", and so all sorting programs are ~a equivalent. Still, theorems that make use of this equivalence relation (or any other) do not assume that it's an equality relation.
I don't want to presume, but you maybe you're just used to a formalism where the only equivalence (on the denotation in that formalism) is equality (the extensional function equality). To make this more familiar, I can point out that typed functional languages also have weaker notions of equivalence, as they have one level of abstraction/refinement (assuming no subtypes) -- that between types and their inhabitants; the relation between type parameters and concrete types might be another level, as is typeclasses. You normally have theorems about functions based just on types, and that are true for all inhabitants (or theorems about a polymorphic signature that is true for all type instances). You don't need to rework your theorems for every type inhabitant (or every type instance). In a formalism like TLA, this abstraction/refinement relation is a lattice with infinite levels (a little similar to a formalism with subtypes). Instead of just having types (which express nondeterminism, i.e., the type Int -> Int nondeterministically represents some Int -> Int computation) and inhabitants, you have arbitrary levels of nondeterminism (or abstraction), where more refined programs can be instances of more abstract ones (i.e., ones with more nondeterminism).
> but state machines are not the only form of computation. For the lambda calculus reduction is evaluation - what you did in https://news.ycombinator.com/item?id=15786021 was computation, with no state machine in sight.
Evaluation is a state machine. The substitution I did -- that's a state machine. A state machine is not a Turing machine. It is anything that has states (e.g. expressions) and transitions between them (e.g. reductions).
> The whole point of the Church-Turing thesis is that state machines and expression reduction are equivalent descriptions of computation.
Not quite. That inference rules (reductions) form computation was known since Leibniz in the 17th century. Church's claim was that even the simple reductions of the simple lambda calculus can express any computation expressible by any formalism. Turing explained why that is -- because all formalisms and inference rules are special cases of state machines. Gödel then called Turing's explanation "a miracle", as for the first time we had a definition of what a formal system is and how it works.
> Of course I'm writing my program with specific properties in mind - I'm not just writing some random program and then seeing what properties it has, I'm writing the program because I need a program with certain properties.
It's not always that simple. Suppose I ask you to write a sorting program and you come up with mergesort. You then notice that aside from just sorting it has the property of being stable for incomparable elements. That's something that's nice to be able to prove without rewriting the program.
> You can simulate one with the other, but neither subsumes the other; a rewriting system isn't a state machine any more than a state machine is a rewriting system.
A rewriting system is very much a state machine (albeit often a nondeterministic one, due to evaluation order).
> Any collection of symbols can be given a trivial "denotational semantics", but this "denotational semantics of Java" would not capture the things that make Java Java, because the relations between "expressions" (which would not correspond to Java expressions) bear no relation to the definition of Java-as-it's-usually-understood, the denotations of Java functions would not be functions.
I don't know where you get that. Formal methods for Java (like Infer [1]) make use of this denotation all the time, and programmers who carefully think about their Java programs do it just as effectively as those who carefully think about their Haskell programs. Sometimes their work is harder, and sometimes it isn't, and in any event, there are many other considerations to take into account (e.g., analyzing programs from syntax is not the only nor the "best" way to analyze programs; we also analyze programs as they run using dynamic analysis tools, profilers and tracing).
Of course the denotation of Java methods isn't functions. The standard denotation for imperative languages is that of Hoare logic (or "Predicate transformer semantics" [2]). If I write a Java method that isn't pure, I don't think of it as a function. In fact, I rarely think of computations functions.
> I want referential transparency in terms of the common-sense meaning of the syntax, not in terms of some contrived meaning that exists only for analysis.
It's not contrived at all, and it's rather intuitive: every Java statement is a transformation of program state.
Now, I completely agree with you that functional semantics are more convenient (as they're simpler, more local etc.), but they stop being convenient once the program isn't sequential. The question is, is it worth it to use a language that enforces (by enforced purity) this function semantics on the entire program if it's only really helpful for some bits of it. There is no right answer to this question. Some would prefer that language and some wouldn't, and both would be perfectly justified.
> There are only 9 possible partial functions of type Boolean => Boolean, whereas there's a combinatorially huge number of possible behaviours.
How many possible partial functions are there for (Int -> Int) -> (Int -> Int)?
> and I've only had to think about a few lines
That's really, really good! But 1/ that still doesn't mean that purity needs to be enforced everywhere, and 2/ this helps but only with the easy part.
> properties of program fragments are formally proven, in a verified way, in normal industrial code, every day using Haskell-like type systems.
In that case, many, many more systems (many, many times over) are formally proven using Java-like type systems.
> I'm a lot more confident in our ability extend that approach to cover the properties we care about, than in our ability to get the overhead of state-oriented approaches low enough to use for normal industrial code.
That's an overhead that you're imagining. In fact, it's much easier to build formal tools for what you call "state-oriented" approaches than for pure functional languages because of the latter's dependence on higher-order functions.
> Just thinking about sequences of state operations doesn't tell me enough to understand a program; I can't understand the composition of two sequences of state operations without understanding the full state... Of course a state operation is equivalent to a function from program state to program state, and such functions would be just as hard to understand as state operations - but most functions are defined on much smaller spaces
Look, you're trying to extrapolate from bits of information. We're talking about a system that's based on temporal logic, by far the most useful logic for formal methods to date, and one that has so far directly yielded two Turing awards. You can try to imagine what that system would look like or you can read my posts/watch my talk. You're not actually dealing with the elements of sequences as you may imagine, just as you're not dealing with sets of pairs when you're analyzing functions. We're talking about an elegant algebra of program behaviors, that I don't wish to fully describe in a HN comment, partly because I've already described it elsewhere.
Anyway, once again, I'm not by any means trying to claim that Java is better than Haskell or that Eve is better than Haskell etc. I'm just trying to say that your conlusions (that Haskell is better than Java) are based neither on a good theoretical justification -- 1/ the fact that you can easily reason about sequential programs is very nice, but most programs today aren't sequential, and so we get to tradeoffs again, and 2/ you seem unfamiliar with the vast body of research on other kinds of program analysis; AFAIK, nobody claims that those other methods are any "better" or "worse" than the functional one; just different -- nor on any empirical data (which is far more important). I just don't like this discourse that X is better than Y without a careful definition of what "better" means and without some very compelling evidence.
[1]: http://fbinfer.com/docs/separation-logic-and-bi-abduction.ht...
[2]: https://en.wikipedia.org/wiki/Predicate_transformer_semantic...
Well, sure. But showing that two programs are ~-equivalent will be no help in attempting to show that they do (or don't) have the same runtime. The fact that I don't have to switch formalisms to talk about runtime doesn't actually help me, because I still have to redo all my analysis.
> A state machine is not a Turing machine. It is anything that has states (e.g. expressions) and transitions between them (e.g. reductions).
"State machine" is generally understood to mean a finite state machine i.e. a Turing machine.
> That inference rules (reductions) form computation was known since Leibniz in the 17th century.
Indeed; they are if anything the most natural definition of computation, contra your description of computation as a physical process. The "miracle" of Church-Turing is that the mechanistic finite state machine is equivalent to the more natural rewriting system, paving the way for mechanical computation.
> Turing explained why that is -- because all formalisms and inference rules are special cases of state machines.
He didn't show anything about a state machine in your generic sense of "anything that has states and transitions between them". He showed an equivalence between reduction and finite state machines. Neither is a special case of the other, they're just equivalent.
> It's not always that simple. Suppose I ask you to write a sorting program and you come up with mergesort. You then notice that aside from just sorting it has the property of being stable for incomparable elements. That's something that's nice to be able to prove without rewriting the program.
If stability was part of the requirements I would've wanted to pay attention to it all along; if it wasn't then it's unlikely to become one. Accidentally implementing a future requirement seems like a very rare coincidence.
> If I write a Java method that isn't pure, I don't think of it as a function. In fact, I rarely think of computations functions.
I suspect that's pretty unusual. I mean, it's pretty normal to call them "functions".
> It's not contrived at all, and it's rather intuitive: every Java statement is a transformation of program state.
The trouble is that "a transformation of program state" is not an easy thing to think about. It could do absolutely anything.
> How many possible partial functions are there for (Int -> Int) -> (Int -> Int)?
A lot, so a well-structured program wouldn't use a function with a signature like that. The space of possibilities for e.g. (a -> b) -> (a -> b) is much smaller.
> That's really, really good! But 1/ that still doesn't mean that purity needs to be enforced everywhere, and 2/ this helps but only with the easy part.
My experience has been that it can all, or almost all, be put in the easy part. I just haven't had these problems with nonsequentiality that you claim. Maybe there's a niche where they're important, but I don't see the use case the broader industry - webapps, business process automation, that kind of thing.
> In that case, many, many more systems (many, many times over) are formally proven using Java-like type systems.
Sure, not that I'd really distinguish between the two at the level we've been talking at. That the Java type system has been successfully used extensively in practice is a good, hopeful thing about it - though that people commonly cite Java's verbosity as a reason for leaving the language is a mark against that. Unfortunately I've found that in practical Java programs one almost always needs to go around the type system and/or can't practically represent important properties like "this function is only called during an open database transaction" or "this object graph contains only objects that we know how to represent as JSON", due to lacking monads, lacking records, perhaps due to lacking purity. To achieve the defect rates I believe the industry will need in the future, I believe we need a couple of small extensions over the Java type system: higher-kinded types, some form of record-like types (i.e. the ability to work generically with maps where the type of each value is known, but different for different keys), maybe linearity, maybe polykinds. Not some radical new model to learn, just ordinary functions with ordinary return values the way every industrial programmer is already used to thinking about the easy parts of their program with and a few clever techniques to allow us to extend the same approach to work on the hard parts as well.
> You can try to imagine what that system would look like or you can read my posts/watch my talk. You're not actually dealing with the elements of sequences as you may imagine, just as you're not dealing with sets of pairs when you're analyzing functions. We're talking about an elegant algebra of program behaviors, that I don't wish to fully describe in a HN comment, partly because I've already described it elsewhere.
I've tried to read your posts, repeatedly. I just struggle to find the "there" there; I have no intuitions about any of these objects that don't boil down to the same thing as your shadow-variables-and-assertions example; I can't see what they're supposed to do for me that plain old functions and values and types make hard - I can't even do the things that were previously easy.
> the fact that you can easily reason about sequential programs is very nice, but most programs today aren't sequential, and so we get to tradeoffs again
I'm just not convinced there's a balanced tradeoff here. To do functional reasoning you keep a natural, familiar semantics (functions as functions and so on) in plain-old mathematics that you already use when reasoning about the easy parts of your program, you factor out commonality as functions the same way you already do when programming. We're talking about making a few small generalisations of the type system, that's all. It's such a small step, but it's enough to let you prove so many of the things you actually care about in plain old industrial programming; I really can't see why a Java or Kotlin programer would prefer to jump to analysing their programs with a whole new formalism; that seems like a much bigger cost, and there's no visible space for it to have a correspondingly greater benefit.
I'm not sure what you mean by "runtime" -- perhaps something equivalent to Haskell operational semantics -- but in other formalisms the entire system is different. For example, in TLA there is no distinction between the "runtime" and the "function denotation" -- these concepts simply do not exist -- they are both arbitrary points in the same denotational lattice. You can even say that A and B are two different refinements (implementations) of Quicksort, B and C are refinements of Mergesort, and all four are refinements of Sort. What is true for Sort is true for all four. What is true for Quicksort is true for A and B. Those are just arbitrary levels of abstraction. There is no defined concept of "function" which is a specific level of abstraction.
> "State machine" is generally understood to mean a finite state machine i.e. a Turing machine.
A Turing machine is certainly not a finite state machine, and abstract rewriting systems are also state machines. In fact, if you'll google for papers on the operational semantics of lambda calculus (or related PLs), I'm sure the term state machine will come up.
> Indeed; they are if anything the most natural definition of computation, contra your description of computation as a physical process. The "miracle" of Church-Turing is that the mechanistic finite state machine is equivalent to the more natural rewriting system, paving the way for mechanical computation.
Where "more natural" meaning you like it better because that aesthetic appeals to you :) There is just no accepted standard here. In fact, vast subfields of CS never consider the formal-system description, and they are much, much larger than those subfields who prefer working in formal systems.
> He didn't show anything about a state machine in your generic sense of "anything that has states and transitions between them". He showed an equivalence between reduction and finite state machines. Neither is a special case of the other, they're just equivalent.
Not quite. Read his paper, it is very readable. He defines (for the first time!) a general notion of computation, and from it creates an arbitrary instance of it (which is not a finite state machine) which we now call "Turing machines" just for the sake of rigorous mathematical analysis. Turing was the first to define computation in general.
> If stability was part of the requirements I would've wanted to pay attention to it all along; if it wasn't then it's unlikely to become one.
My experience has been different.
> I mean, it's pretty normal to call them "functions".
First, they're not called functions in Java, but "methods", but let's say C. It's pretty normal to call Haskell functions "functions", even though they're not. The term "function" in programming has a long history, and it's because the idea resembles mathematical functions. I agree Haskell functions resemble mathematical functions much more than C functions, but neither of them are actual functions.
> My experience has been that it can all, or almost all, be put in the easy part. I just haven't had these problems with nonsequentiality that you claim. Maybe there's a niche where they're important, but I don't see the use case the broader industry - webapps, business process automation, that kind of thing.
Well, we've had different experiences, then, but I don't need to trust my experience. There's no evidence that writing applications in Haskell is significantly cheaper than writing them in Java or Kotlin.
> "this function is only called during an open database transaction" or "this object graph contains only objects that we know how to represent as JSON", due to lacking monads, lacking records, perhaps due to lacking purity.
This is actually easier in Java than in Haskell. That's what JML[1], arguably the most sophisticated contract system out there, is for (although, admittedly, very few people use it; then again, very few people use Haskell). I don't know why you keep bringing up monads when they are a feature of a formalism, not a general solution to a problem.
> To achieve the defect rates I believe the industry will need in the future, I believe we need a couple of small extensions over the Java type system: higher-kinded types, some form of record-like types (i.e. the ability to work generically with maps where the type of each value is known, but different for different keys), maybe linearity, maybe polykinds.
The difference is that I come from a formal methods direction. I don't look at solutions just in FP. I look at the entire formal methods field and see which solutions are promising for the problems. While I don't know if any would work, both research and a few decades of experience in safety-critical realtime systems show that the synchronous approach, now taken by Eve, is much more promising from a correctness perspective. If your only point of reference is FP, I don't know how you can claim that the (quite clunky, IMO) solutions FP comes up with are the best way forward. Read up on what the general formal methods community is reasearching so you'll have something to compare the FP approach to.
> It's such a small step, but it's enough to let you prove so many of the things you actually care about in plain old industrial programming; I really can't see why a Java or Kotlin programer would prefer to jump to analysing their programs with a whole new formalism; that seems like a much bigger cost, and there's no visible space for it to have a correspondingly greater benefit.
They don't need to jump anywhere. The current formal tools for Java are far more sophisticarted than those available for Haskell. That people don't use them is a different matter, but it's both a shorter jump and arguably a similar if not greater benfit to go from programming in Java to programming in Java and running a static analyzer than to go from programming in Java to programming in Haskell (even assuming Haskell was no worse than Java in any regard, and I find that this is not at all the case).
Church's definition of the lambda calculus actually slightly predates Turing's definition, and Goedel's definition was even earlier. There are bidirectional equivalences between all three; neither is an instance of the other.
> This is actually easier in Java than in Haskell. That's what JML[1], arguably the most sophisticated contract system out there, is for (although, admittedly, very few people use it; then again, very few people use Haskell).
> They don't need to jump anywhere. The current formal tools for Java are far more sophisticarted than those available for Haskell. That people don't use them is a different matter, but it's both a shorter jump and arguably a similar if not greater benfit to go from programming in Java to programming in Java and running a static analyzer than to go from programming in Java to programming in Haskell
I would think Haskell is substantially more popular than JML, though I could be wrong. I did make an effort to use a contract-based system with Java code and found it was ultimately harder than switching languages. Partly that's a question of tooling, but I think the biggest barrier was the semantic model.
> If your only point of reference is FP, I don't know how you can claim that the (quite clunky, IMO) solutions FP comes up with are the best way forward.
I'd make two points here: 1. The things FP does are largely just the application of widely agreed programming principles - separating concerns, making each function do one thing, explicitly distinguishing interface from implementation. I can imagine needing another formalism as well, but I can't imagine wanting to not have monads or records, and the minor type system enhancements needed to accommodate them seem like such a tiny cost compared to the benefits. Even if you only use the functional techniques for some parts of your analysis, and do other analysis using other techniques, a small language feature that makes the functional techniques much more effective is still worthwhile. 2. I feel like I gave a fair test in terms of the time and effort I put in - if anything I put much more effort into trying to use the non-FP approaches. FP solves the problems I have, and I didn't have to stop working and learn a new formalism; I was able to incrementally get there, starting by doing the same stuff I was already doing in Java, and remaining productive every step of the way. Whereas I sunk hours into thinking about preconditions and postconditions and never got anything out of it.
Read the papers, then. You'll find striking differences between Church's and Turing's papers. For one, Church doesn't define what computation is. Instead, he attempts to justify why the lambda calculus is universal, and even then he gets caught in circular reasoning, at which point he gives up and writes in a footnote something like, well, if I can't do this, I don't know how anyone can define computation. Turing's paper, however, was one of the biggest philosophical breakthroughs at least since the 17th century, and regarded by Gödel as a miracle. It is true that Church published his proof of the undecidability of logic ahead of Turing, but his paper does not contain an analysis of what computation is, whereas precisely that is considered the main achievement of Turing's paper.
> I would think Haskell is substantially more popular than JML, though I could be wrong.
I would think so, too, but it's still very fringe.
> I did make an effort to use a contract-based system with Java code and found it was ultimately harder than switching languages. Partly that's a question of tooling, but I think the biggest barrier was the semantic model.
I've had the opposoite experience. Even if Haskell dominated Java as a language (which I absolutely don't think it does), I wouldn't consider it worth switching because the bottom-line benefits are too small (if they exist at all), while the tooling and ecosystem (both libraries and hiring) is so lacking that the significant hit would dwarf any gains.
> The things FP does are largely just the application of widely agreed programming principles - separating concerns, making each function do one thing, explicitly distinguishing interface from implementation.
I disagree that FP has any advantage here over most programming languages.
> I can't imagine wanting to not have monads or records, and the minor type system enhancements needed to accommodate them seem like such a tiny cost compared to the benefits.
First, most languages have records (including Eve and TLA+). Second, monads are completely meaningless and useless once functions are not how you describe computation. They are very much a formalism-dependent construct. Lastly, while I like type systems, I think about the problem not the solution. The problem is cheap specification and verification of simple propeties. Types are not the only way of doing that, and when considering the future of programming, we cannot constrain ourselves to solutions found within a very narrow sub-discipline while ignoring the full body of research.
> I feel like I gave a fair test in terms of the time and effort I put in - if anything I put much more effort into trying to use the non-FP approaches. FP solves the problems I have, and I didn't have to stop working and learn a new formalism; I was able to incrementally get there, starting by doing the same stuff I was already doing in Java, and remaining productive every step of the way. Whereas I sunk hours into thinking about preconditions and postconditions and never got anything out of it.
I fully believe that. I've had the exact opposite experience, ever since starting to work with Scheme and SML almost twenty years ago. I don't think Java dominates Haskell and I don't think Haskell dominates Java. Each works better for different people and different circumstances, and there is currently no evidence that either is significantly ahead of the other in terms of the bottom-line.
I have no problem arguing for days over this feature and that, this design philosophy or the other. I just don't like claims that the evidence does not support.
I found these problems were worse when trying to use contracts; since they're not part of standard Java, the tooling and ecosystem doesn't work nicely with them. Automated refactoring in the IDE won't update the annotations properly. You go to use an existing library and find that the published annotations were for a previous version and no longer match the current API, or you can't find which version they go with - or worst of all, they still match the method signatures but are no longer true. And the hiring problem is the same. Ultimately the point I suspect we may have to disagree on is that I'm a lot more confident most Java programmers could learn Haskell than I am that most Java programmers could learn a contract-like approach, because I really think the latter is a much bigger conceptual leap.
> I disagree that FP has any advantage here over most programming languages.
I see programmers in other languages having to go around the language to get these things - e.g. the popularity of annotation-based AOP in Java codebases, and the use of monkeypatching to address similar problems in scripting languages - in a way that doesn't happen in (Haskell-like) FP languages.
> monads are completely meaningless and useless once functions are not how you describe computation. They are very much a formalism-dependent construct.
Be that as it may, I thought we agreed that we frequently do want to do the functions-and-values kind of reasoning about our programs, even if we only do it for the "easy parts".
> Lastly, while I like type systems, I think about the problem not the solution. The problem is cheap specification and verification of simple propeties. Types are not the only way of doing that, and when considering the future of programming, we cannot constrain ourselves to solutions found within a very narrow sub-discipline while ignoring the full body of research.
If there's an adequate solution in that narrow sub-discipline then we can. If the cheapest, most familiar approach works then there's no reason to look at more expensive approaches. Almost all programmers working in the industry have at least some basic familiarity with type systems. I'm not against exploring more radical approaches - that's part of what research is for - but when it comes to advocating something for industrial use, let's be sure we've exhausted the easy options first.
Right. There are always tradeoffs.
> And the hiring problem is the same.
I don't think so. A Java programmer can be trained in JML in a day.
> Be that as it may, I thought we agreed that we frequently do want to do the functions-and-values kind of reasoning about our programs, even if we only do it for the "easy parts".
Sure, but pure "functions" can be reasoned about as functions even in Java.
> If there's an adequate solution in that narrow sub-discipline then we can. If the cheapest, most familiar approach works then there's no reason to look at more expensive approaches.
It's neither the cheapest nor the most familiar. Virtually no formally verified programs encode correctness properties in types. Contracts are far more common.
> I'm not against exploring more radical approaches
It's not more radical. If you look at the programs of formal methods conferences, you'll find that the typed-FP approach is in the minority. I think that part of the problem is that some FP people have isolated themselves in a bubble that they sometimes forget how small it is.
This I don't believe, not in the general case. If it were that easy we'd see a lot more people doing it. (And I'm pretty sure I've put more than a day's worth in over the years).
> Sure, but pure "functions" can be reasoned about as functions even in Java.
It's much harder without monads. You lose the ability to cleanly divide the return value of a function that's composed from smaller functions into two visibly orthogonal aspects that you can provably think separately about, so you have to understand all aspects of what the intermediate values represent at once.
It is that easy. What is hard isn't knowing JML, but gaining experience with specification in general. This is a skill that is required regardless of formalism (and is actually why Idris and Java+JML, despite being very different, are still much more similar than they are different; same goes for TLA+ and Lean).
One of the reasons I would encourage those who are interested in correctness to read Schmidt's overview of abstraction/refinement relations [1] -- which forms the core of possibly the most important idea in all of program analysis: abstract interpretation -- is that it allows one to see type systems, contracts, refinement logics etc. as different expressions of this same core idea; specifically of a Galois connection between different abstraction levels, be they a program and its type, a program and its contract, or different abstraction levels in a formalism like TLA.
> It's much harder without monads.
But you have monads in Java. In fact, there are many more Java programmers using monads (e.g., Stream and CompletableFuture) than Haskell and Scala programmers using monads combined. What you can't do is abstract over all monads, which is of questionable value even in Haskell (and Java has other ways of abstracting over common patterns).
The goal now is to remove the need for monads in Java. Monads are equivalent to delimited continuations, but delimited continuations compose more easily (algebraic effect systems are modeled after them) and they fit much more nicely with imperative constructs like loops and exceptions. Delimited continuations are the monads of imperative programming, and they are coming to Java.
[1]: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.16.4...
A broad library of standard functions is certainly valuable; working in Java with Stream and CompletableFuture one naturally finds oneself wanting traverse, cataM and dozens of other such helpers. Maybe the ability to abstract over monads is only useful to library authors, but the libraries they produce are then immensely useful for regular programmers.
> Monads are equivalent to delimited continuations, but delimited continuations compose more easily
Perhaps, but at the cost of completely incomprehensible code. We've known for years or decades that continuation-based style can produce higher-performance code than conventional approaches, but they've seen limited adoption even in high-performance environment; many, perhaps most programmers (myself included) just don't and can't "get" them.
I find libraries that help developers save a few lines of code here and there not worth changing a programming paradigm. By far the biggest boost comes from reuse-in-the-large. I fully agree that languages with such higher-order constructs allow writing more reusable code than classical imperative languages. But "more", in this case, does not translate to big savings and does not justify a change of paradigm. We are deep in diminishing returns territory there, even if pure FP had no disadvantages.
But those higher-order constructs do not require a pure language, and could be added to Java/Kotlin once there are no bigger-impact improvements to be made, and if it's judged that their meager contribution justifies adding complexity to the language. Not every added utility automatically translates to "we should do it." Its cost must be weighed as well. Languages like Java/Kotlin choose to be more conservative in the cost/benefit of the features they embrace compared to languages like Scala.
> Perhaps, but at the cost of completely incomprehensible code.
Quite the opposite. Ordinary imperative code (i.e., blocking threads) is programming with continuations. Continuations are the core abstraction of imperative languages, just as partial functions are the core abstraction of pure-functional ones, and all the core constructs in those languages -- loops, exceptions -- are built to work with them. The complex code you're thinking of is analogous to very complex code that can be achieved with monads. While it could be done, there is no reason to ever do it.
I find being able to reduce code in the small yields exponential returns in the large. If one can reduce the size of plain code by say 10%, making functions and classes shorter and easier to comprehend, then that takes some of them below the threshold where they need to be split up, and unlocks further opportunities to see and factor out commonality, reducing code size and class counts further. That might take you below the threshold for needing to separate a layer in the larger component, and that in turn allows more reuse; that might take a component below the threshold of needing splitting up, and that might take the project below the threshold where it needs multiple developers or multiple teams involved.
You don't have to change paradigm. I can understand (though I don't agree with) wanting more operational features in a language. But I can't understand being so hostile to these conservative but useful features.
> But those higher-order constructs do not require a pure language, and could be added to Java/Kotlin once there are no bigger-impact improvements to be made, and if it's judged that their meager contribution justifies adding complexity to the language. Not every added utility automatically translates to "we should do it." Its cost must be weighed as well.
Costs should indeed be weighed, but HKT has one of the strongest cases in terms of power-to-weight: it's a very cautious extension of the type system that doesn't really make the language any more complex, since it just means permitting type parameters to be used in ways that concrete types are already allowed to be used. And virtually every application can benefit; I use traverse virtually every day. Features like language-level null or delegation have a much higher risk (they change more of the rules of the language, a reader has to be aware of them even if they aren't using them directly and when they're not necessarily visible in a function signature) and are less broadly applicable.
> Quite the opposite. Ordinary imperative code (i.e., blocking threads) is programming with continuations. Continuations are the core abstraction of imperative languages, just as partial functions are the core abstraction of pure-functional ones, and all the core constructs in those languages -- loops, exceptions -- are built to work with them.
Threads, loops and exceptions are notorious sources of bugs and incomprehensible code. To the extent that they're the core of imperative programming, imperative programming is a bad thing.
I am not hostile to them, just skeptical of their cost/benefit. I don't think every useful feature has a place in every language. Different languages should have different thresholds for the cost/benefit of features they want. It's perfectly legitimate for Scala to have a low threshold, and for Kotlin/Java to have a high one. In fact, a high threshold on cost/benefit is one of the cornerstones of the Java design philosophy, as laid down by James Gosling back in the 90s. He said that his design philosophy for Java specifically excludes features that are just a good idea, and only includes features that solve major problems (of course, what constitutes a major problem is neither universal in time nor in space; as coding fashions change, problems that were once minor can become major). You may prefer to use a language with a different design philosophy, but I think that philosophy is certainly reasonable. Again, without any kind of empirical data, I don't see how this can be settled by anything other than personal aesthetic preference.
> HKT has one of the strongest cases in terms of power-to-weight: it's a very cautious extension of the type system that doesn't really make the language any more complex, since it just means permitting type parameters to be used in ways that concrete types are already allowed to be used.
Maybe, and maybe Java and Kotlin should get HKT one day. But I don't think this feature would be the most important one to add right now, and I can certainly see strong arguments against encouraging higher-order abstractions in general. For one, I find that abstractions-in-the-small take precious mental resources away from far more important things. For another (although related), I think they encourage abstract code of the kind that was common in Java frameworks like Spring, which took Java a long time to discourage in favor of simpler, more concrete code, YAGNI etc.
> Threads, loops and exceptions are notorious sources of bugs and incomprehensible code.
OK, but I strongly disagree (BTW, by "threads" I'm not implying any kind of communication mechanism, like shared memory; Erlang is also based on threads. I just mean one or more sequential instruction stream that can block).
I see the fact that Spring was immensely popular in Java for a while as demonstrating just the opposite: that overgeneralisation and second-system effect happen to everyone, even in a language whose design philosophy was oriented towards avoiding it. I see Java's adoption of generics and lambdas as acknowledgement that omitting those features didn't help encourage simpler code, it just made complex code even worse. I think it's the same for HKT and similar abstraction tools.
No, that's just not true. If you have an order relation (a Boolean lattice, in fact), and B => C, then if A => B, then A => C. I.e., any proposition C that is true for your level-of-detail B, then it is also true for your finer level-of-detail A.
> because of course in the lambda calculus they're one and the same
This is a philosophical question, but I don't think it's accurate to say that. For one, the lambda calculus alone does not really describe a computation. Only a lambda expression combined with a state-machine -- i.e., an evaluation strategy -- defines a computation.
> Certainly I want to reason that way (most of the time), because it's a lot more convenient and simpler than reasoning about sequences of operations.
I don't know how you can say either of those things. It's true that I'm a beginner at Lean, but proving things in TLA+ is usually much easier. It's not so much a sequence vs a function, but that you naturally get this beautiful "lattice of abstraction". It allows you to prove that, say, a general description of the Quicksort, one that simply cannot be written in any programming language as it leaves unspecified how a pivot is chosen as well as other details, indeed sorts, and then you can show that a particular implementation is a refinement of that high-level description, and you automatically know it sorts correctly.
In addition, this style allows you to write your program however you like, and only then prove things about it, rather than write it with specific properties in mind (e.g., if you want to prove worst-case complexity, you must either write your program as a monad or use types that include a cost model). I've heard that some functional type theories, in particular, proof refinement logic, PRL, allows you to do the same, but it's not something that you can just do in Lean/Coq (unless you embed TLA in them).
Also, by far the most common proof technique of global program correctness (regardless of formalism) is the inductive invariant technique. Namely, say your program is P, and that your global correctness property (say, "the database is always consistent") is S, and you want to show that P => S, the inductive invariant technique finds an invariant I, such that I => S, that I is true in your initial state, and that if I is true for any state s of your program, then it is also true for any state s' reachable from s. This may not be how you prove properties of some simple functions, but it is by far the most common way to prove a global property for an entire program. Behavioral semantics makes this particularly convenient.
> monads are useful for working with computations that are perfectly adequately described by functions.
Right, but they're still part of the "functional algebra". You don't use them if your computations are represented by an entirely different algebra. They are not used in process calculi, and they are not used in TLA. They just don't serve any role whatsovever in describing computations in those mathematical theories.
> the broader notion of whether we analyse program fragments as sequences of operations on a pervasive state that changes over a pervasive time, or as expressions in a term reduction system.
Not exactly. A "term-reduction system", more commonly called an abstract rewriting system, is also a state machine. The difference, rather, is in denotation. Whether you're working in a system where the denotational semantics of a term is a so-called partial function, or one where the semantics of a term is different, say, a set of sequences, as in TLA.
> I'm agnostic about specific formalism, but I think being able to analyse programs as expressions where we consider expressions with the same reduction as equivalent is a vital capability that I would want any formalism I used to have.
You get that anyway. Even in Java. That was precisely what Christopher Strachey showed when he first introduced the term "referential transparency" to programming languages[1] -- that imperative languages are referentially transparent. In Java, if you have an expression e, you can replace any sub expression, x, with another y, that has the same denotation, without changing the denotation of e. The difference between Java, Haskell and TLA is just what that denotation is. In Haskell, it is a "partial function"; in Java it's a predicate transformer [3] (i.e., a Hoare triplet); in TLA it's a set of sequences. This choice has both aesthetic and prgamatic consequences. I completely agree that the functional denotation and the behavior denotation are both normally more convenient than a Hoare triplet.
> And I think there's a close-to-objective sense in which that technique/approach is valuable: the space of possibilities we have to consider when working with terms in a language can be so much smaller than the space we have to consider when working with operations on a state.
This is simply not true on multiple levels. One, you always "work on terms" when working syntactically. The question is what is the semantics of the term. It is 100% false that a semantic domain of partial functions makes your state space in any way smaller than if your semantics domain is sets of behaviors. It's just not true.
> And in practice, the only form of verified formal proof of properties of program fragments that sees use in "normal" industrial code (i.e. ordinary webapps and the like, not high-assurance environments) is Haskell-like typesystems
This is 100% false. Haskell's type system (without clever tricks such as singleton types) is so weak that the properties it "verifies" fall far, far below what is normally regarded as "formal verification". OTOH, the most common formal verification in industry is done on hardware and realtime software systems, which normally employs model checkers, and uses temporal logic, and semantics very similar to those of TLA or Eve. Eve brings the formalism that's so far been used for formally-verified development in the safety-critical world to the mainstream. In addition, some well-known companies using formal verification, like Altran UK, use Ada SPARK, which uses Hoare logic. Haskell-style programming is just nowhere near what people call formal verification, and those who use formal verification rarely use Haskell.
> I can't believe that state-based reasoning could ever displace expression-based reasoning, since (as seen in your own talk examples) even very short expressions can correspond to absolutely enormous spaces of possible states.
This is just mathematically wrong, because if you think of the cardinality of functions you'd realize that it's the same as (normally bigger, actually) than that of sequences (e.g. the set of functions from the natural numbers to the natural numbers is exactly that of sequences of natural numbers). In fact, this makes it harder to create automated formal reasoning tools (model checkers and static analysis tools employing abstract interpretation) for functional languages.
You're also wrong because already that style is far more common in formal verification. You don't have to take my word for it. Here are Xavier Leroy and Simon-Peyton Jones bemoan that the state of formal methods in FP is so far behind that of even "classical" imperative programming languages [4].
[1]: https://en.wikipedia.org/wiki/Abstract_rewriting_system
[2]: https://stackoverflow.com/a/9859966/750563
[3]: https://en.wikipedia.org/wiki/Predicate_transformer_semantic...
[4]: http://homepages.inf.ed.ac.uk/stg/Milner2012/Monday_Panel-ht...