1. 14

      Questions (and answers) like this really ought to start with a definition of what they mean by “Agile”.

      The top voted answer appears to be critiquing a very rigid Capital-A-Agile methodology, but none of it comes through to me as a valid critique of a more general lower-case-a-agile methodology: deploy regularly, tight feedback cycles with users, integrate feedback.

      1. 10

        I guess these discussions are always a bit futile, because “Agility” is by definition a positive property. It’s a tautology really.

        Most criticism of agile methods are more focussed on a specific implementation (scrum at company X), and the usual response is “this is not true agile”.

        1. 7

          “this is not true agile” I’ve been guilty of this in the past. Agile is good, therefore if what you’re describing to me isn’t good then it’s not true agile.

          But after years of Scrum at various shops, sometimes under the guidance of pricey “Scrum coaches” consultants I’m totally burnt out and disillusioned by it.

          As you say agile is by definition positive but beyond this, I think there are still a lot of good ideas and principles in the early agile movement just not in the Scrum process itself (which doesn’t predate Agile) and what it has come to represent.

          1. 6

            I would define Agile as “follows the principles of the Agile Manifesto”. This implies a few things:

            1. The Manifesto devalues things like comprehensive documentation. This can be criticized and discussed.

            2. Scrum is only one possible instance of Agile. Not necessarily the best, maybe not even a good one. I would suspect that people discussed that to death already when Scrum was fresh.

            3. You can do Scrum without Agile. Scrum is usually defined superficially. This means there is a lot of room for variation including stuff which undermines the Agile intentions. Second, it helps the consulting business, because how could you get Scrum right except by oral teachings of certified people?

            1. 1

              The Manifesto devalues things like comprehensive documentation. This can be criticized and discussed.

              This aspect is a bit peculiar. Do they devalue software-documentation? (which is how I understood this principle). Or maybe it can be thought of a devaluation of a requirements-library/document. I came to terms with this principle in the sense, that it meant as an advice to avoid wasteful, up-front documentation, because clearly you cannot build a good product without documentation.

              1. 1

                From the manifesto:

                That is, while there is value in the items on the right, we value the items on the left more.

                It’s not “documentation doesn’t matter”, it’s “deliver something that works or your documentation is pointless”.

              2. 1

                The key bit of superficiality that reduces Scrum’s value is that people ignore the fact that Scrum does not mandate a process:

                It is the opposite of a big collection of interwoven mandatory components. Scrum is not a methodology. What is Scrum?

                Scrum is not a process, technique, or definitive method. Rather, it is a framework within which you can employ various processes and techniques. Scrum Guide

                They take the initial process guide, defined in Scrum as a starting point to test, reflect, and improve upon, and treat it as a big collection of interwoven mandatory components. It makes middle management feel good as they get to hold meetings, see progress, and implement a buzzword, but avoids all of the valuable parts of Scrum.

              3. 3

                Bertrand Meyer has some criticisms (and compliments) of the core ideas, especially user stories vs requirements.

                1. 1

                  thank you for that link. Would prefer text over video, but if it is Meyer, I’ll try to make room for it.

                  1. 1

                    Yeah, I feel the same way. He apparently has a book on the same topic, but I haven’t read it.

                    1. 1

                      okay, I haven’t watched it fully, but skipped over a few parts ,but I made sure to look at the user storeis and requirements parts. I am a bit torn on his view, because I can relate to his feeligns as a software user, that many times his user-story was forgotten and he attributes this to not generalizing them into requirements. However, I wonder if the lack of a requirements document is really the reason. Also, I think he must have forgotten how unusable a lot of requirements-backed software has been.

                      I share his sentiments on design and architecture work. However, good teams with good management have always made it possible to fit such work into the agile workflow. I attribute to agile consultants, that throughput and “velocity” have been overemphasized to sell agile, when it should much more be about building good products.

                      He lost me when he commented on test-driven development.

                    2. 1

                      His book is called “Agile! The good, the hype, and the ugly”, it’s brief, insightful, and well worth a read.

                2. 5

                  I would argue that what you’re talking about there is more the consequences of adopting continuous integration and making deployments less painful, which one might call operational agility, but it has very little to do with the Agile methodology as such, at least from what I can see.

                  1. 6

                    Nope. Having tight feedback cycles with users is a core principle of Agile. Continuous integration on its own has nothing to do with user feedback, and doesn’t necessarily cause responsiveness to user feedback.

                    1. 1

                      The Agile Manifesto does not mention tight cycles, only “customer collaboration”.

                      1. 2

                        the Agile Principles (you have to click the link at the bottom of the manifesto) make multiple references.

                        1. 1

                          Can you explain? I don’t see the words “tight”, “feedback” or “cycles” here http://agilemanifesto.org/principles.html

                          1. 1

                            Presumably: The main difference between collaboration with customers (vs contract negotiations) is that rather than getting a single document attempting to describe what the customer wants up front (feedback cycle = one contract) you continually work with them to narrow down what they actually want (shorter/tighter than that).

                            1. 1

                              the first principle, satisfy the customer through early and continuous delivery of valuable software, implies it. the third, deliver working software frequently, implies it. the fourth, business people and developers must work together daily, is an out-and-out statement of it.

                        2. 1

                          In my experience CI&CD is more useful for bugs than features. If you are coming from waterfall I understand where the connection between CI/CD and agile comes in.

                          1. 2

                            Regardless of your experience and opinion of utility, those strategies are core to Agile and have obvious analogues in other industries that Agile draws inspiration from. They aren’t unique or novel products of Agile, but I think it’s fair to say that’s how they reached such widespread use today. It’s definitely incorrect to say they have little to do with Agile methodology.

                      2. 3

                        After having been making the error of using the word “agile” in the latter generic sense for some time, I came to realize that pretty much nobody does it. When you say “Agile” business people automatically think “Scrum” and it works (still) as a magical incantation. When you try to talk about the actual merits of agile approaches (plural) they tend to phase you out and think you’re trying to look smart without knowing anything.

                        1. -2

                          The top voted answer appears to be critiquing a very rigid Capital-C-Communism ideology, but none of it comes through to me as a valid critique of a more general lower-case-c-communism ideology: democratic, common ownership of the means of production, state and classlessness

                          1. 3

                            here

                            He is so “crazy” that one of his former colleagues has a totem that they use to mock him in his absence? Fascinating.

                            1. 4

                              I would just keep in mind that Michael is a member of this community when making comments like this.

                              1. 2

                                I think being skeptical is fine, and perhaps even warranted. However, the top level link /seems/ like a fairly reasonable read to me. Judge it on its content.

                                1. 5

                                  I think the problem is he speaks pretty authoritatively despite his expertise being based on just his experiences, or his perception of his experiences. It sounds good, but a lot of things sound good and are only occasionally true, not always true.

                                  I used to think he was just idiosyncratic til I had an experience that contradicted his claims, and then he just said “wait til you enter the real world.” I’m actually a few years older than him I believe. He’s incapable of imagining that things may be different. Even if he were right, it’s a very rigid view that doesn’t account for contrary evidence. I’m wary of trying to learn anything from people like that.

                                2. 2

                                  He showed himself to be pretty out there at Google, when he rage-quit with a particularly nutty letter to the entire company after not getting a promotion. Lots of bits of that letter were memes when I left Google (“I have T7-9 vision!”).

                                  1. 2

                                    He showed himself to be pretty out there at Google, when he rage-quit with a particularly nutty letter to the entire company after not getting a promotion.

                                    It wasn’t about not getting a promotion. I was marked down in “Perf” for speaking up about an impending product failure. (Naively, I thought that pointing out the problem would be enough to get it fixed. It was obvious to me what was about to go wrong– and I was later proven right– but I lacked insight into how to convince anyone.) I found out years later that I was put on a suspected unionist list. Needless to say, the whole experience was traumatic. There’s a lot that I haven’t talked about.

                                    The mailing list activity… I’m embarrassed by that. I did not handle the stress well.

                                    Lots of bits of that letter were memes when I left Google (“I have T7-9 vision!”).

                                    Isn’t it a sign of success, if people are talking about your mistakes several years later?

                                  2. 1

                                    Personally I think Michael O Church is a genius but I’m keenly aware that there’s a fine line between genius and madness. /u/churchomichael is not Michael O Church but seems to be another very intelligent writer but without the anger and national and international politics interest.

                                    1. 1

                                      doing some digging he seems….. crazy.

                                      I’ve had a lot of difficult experiences, some related to the political exposure that comes from being outspoken in a treacherous industry. I’ve needed treatment for some of the after-effects.

                                      Like, he got banned from Hacker News, and also Wikipedia.

                                      And Quora, too! Wikipedia I actually deserved; that was 2006 and I was being a jerk. The Quora ban was specifically requested by Y Combinator after they bought it.

                                      He just seems to spend an insane amount of time writing ranty comments/articles/etc online and not much else.

                                      It’s not that much of my time.

                                      See /u/churchomichael

                                      That’s not me. I’m as surprised as you are that someone would name his account in homage to me. There are also Reddit accounts (and even a subreddit!) that exist to mock me.

                                      Dude just seems to want to complain.

                                      No, I’d like to fix things, but the odds of that are very, very poor.

                                      He has 45 suspected sockpuppet accounts on Wikipedia

                                      Yeah, most of those accounts don’t exist. That’s a hit piece. I’m embarrassed by some of what I did on Wikipedia in 2003-6, but I never had 45 alternate accounts, though I did use so-called “role accounts” back when it was accepted.

                                    1. 4

                                      On services with large number of users typo in username can lead to account that also exists. In this case showing user if account with this username exists or not is meaningless.

                                      1. 2

                                        I agree. The error message is actually correct as written. The user entered their username incorrectly or their password incorrectly, or both. The application doesn’t know which and shouldn’t guess!

                                      1. 7

                                        Some Haskell features are just mistakes; others are designed for PL researchers to experiment, but their usefulness in industrial programming is yet to be proven.

                                        I’d like to see a list of which Haskell features aren’t considered good for production code, and why! I’ve decided TransformListComp is one, because it has zero uptake in the community. Years ago I saw ImplicitParams go horribly wrong, but haven’t tried it since.

                                        On the other side, I love OverloadedStrings and GADTSyntax. I asked on twitter, and the list of batteries included extensions included OverloadedStrings, ScopedTypeVariables, LambdaCase, InstanceSigs, and TypeApplications.

                                        Got any features you feel are good or bad for production Haskell?

                                        1. 2

                                          This is a good start on an answer: https://stackoverflow.com/a/10849782/108359

                                          1. 0

                                            Lazy evaluation makes it hard to reason about the space usage or even termination of a program. I prefer having eager evaluation with lazy data structures.

                                            1. 8

                                              The downside is that you can’t use functions for control flow. An obvious example is Church encoding, e.g.

                                              true x y = x
                                              false x y = y
                                              ifThenElse c x y = c x y
                                              

                                              If we call ifThenElse eagerly, both branches x and y will be calculated; if we used these to e.g. select between a base case and a recursive case, we’d cause an infinite loop.

                                              Most eager languages resort to a built-in lazy if construct (Haskell has one too, but it’s unnecessary), which forces us to reframe our problem in terms of some built-in boolean type rather than custom domain-specific types (for a similar issue, see boolean blindness).

                                              On the one hand, (Church) booleans are quite a weak argument for laziness since “real programs” will be using some richer, more meaningful, custom datatypes instead; yet on the other hand, most eager programs end up relying on booleans, since they’re the only thing that works with the built-in if!

                                              Whilst an eager language with things like case and pattern-matching can alleviate some of these problems, I still think that lazy function calls are important. In fact, I think this is a blub paradox, since even eagerly evaluated languages provide lazy && and || functions; but again, this is usually limited to hard-coded, built-in constructs.

                                              1. 4

                                                The lazy if example always stroke me as silly. It is actually less elegant than you might think: to call it, you need to create two thunks, even though you know in advance that (at least) one will be discarded. I know that optimizing compilers can get rid of the overhead, but that would be an implementation detail that isn’t immediately justified by the semantics of the language in question. In any case, you don’t need if as a built-in in a strict language. It is nothing but syntactic sugar for pattern matching on Bool. Similarly, arithmetic if is syntactic sugar for pattern matching on an Ord produced by a call to compare. Etc. etc. etc.

                                                By making a sharp distinction between values and computations, strict languages gain expressivity over lazy ones. If you want to recover the benefits of laziness in a predominantly strict language, you can always define an abstract type constructor of thunked computations - that can be implemented in 20-30 lines of ML. On the other hand, adding seq to a lazy language wreaks havoc in its semantics, weakening or destroying many free theorems, presumably the main reason for preferring a lazy language over a strict one.

                                                EDIT: Wording. Broken link.

                                                1. 3

                                                  In any case, you don’t need if as a built-in in a strict language. It is nothing but syntactic sugar for pattern matching on Bool. Similarly, arithmetic if is syntactic sugar for pattern matching on an Ord produced by a call to compare. Etc. etc. etc.

                                                  Yes, I hand-waved this away as “things like case and pattern-matching” :)

                                                  a sharp distinction between values and computations

                                                  From this perspective, my point could be phrased as laziness “unifying” values and computations. In the if example, we can implement it eagerly by making the thunks explicit, e.g. giving true and false type (Unit -> a) -> (Unit -> a) -> a. Or should that be (Unit -> a) -> (Unit -> a) -> Unit -> a? Maybe we need both…

                                                  One of my favourite things about programming is when I come across unifications of concepts I’d previously considered separate. Examples which come to mind are Python classes being first-class objects, Smalltalk control-flow statements (e.g. ifTrue:) being method calls, Lisp code being data (in a way that’s both useful (unlike strings) and looks the same unlike complicated AST encodings), and pointers being ints in C.

                                                  Whilst I accept that we may lose expressivity, and this can certainly be important for resource-constrained or -intensive tasks, for the sorts of inefficient plumbing I tend to write I very much like the symmetry that is gained from having fewer distinct concepts/constructs/etc. to take into account (especially when meta-programming!).

                                                  adding seq to a lazy language wreaks havoc in its semantics, weakening or destroying many free theorems

                                                  That’s certainly a problem, I agree :(

                                                  1. 4

                                                    Yes, I hand-waved this away as “things like case and pattern-matching” :)

                                                    Handwaving is failing to provide a proof. What you did was simply make a wrong statement:

                                                    Whilst an eager language with things like case and pattern-matching can alleviate some of these problems, I still think that lazy function calls are important.

                                                    Pattern matching isn’t there to “alleviate” any “problems” caused by the lack of laziness. Pattern matching is the eliminator for sum types, which, by the way, don’t actually exist in lazy languages.

                                                    since even eagerly evaluated languages provide lazy && and || functions; but again, this is usually limited to hard-coded, built-in constructs.

                                                    In a strict language, && and || are not functions, but rather syntactic sugar over nested uses of pattern matching on the boolean type.


                                                    From this perspective, my point could be phrased as laziness “unifying” values and computations.

                                                    You aren’t unifying anything. What you’re doing is ditching values altogether, and replacing them with trivial computations that return those values. In your limited world, values only exist “at the end of the computation”, but they are not first-class mathematical objects that you can, say, bind to variables. So you are deprived of any proof techniques that rely on variables standing for values, such as structural induction.

                                                    On the other hand, if you properly place value types and computation types in separate categories, you will find that these categories are related by an adjunction and admit different universal constructions. Explicitly acknowledging this structure allows you to define abstractions that don’t break in the face of nontermination or explicit thunk-forcing, unlike most of Haskell’s library ecosystem.

                                                    One of my favourite things about programming is when I come across unifications of concepts I’d previously considered separate.

                                                    If essential properties of the objects being “unified” are lost, it stops being “unification” and becomes “conflation”.

                                                    for the sorts of inefficient plumbing I tend to write I very much like the symmetry that is gained from having fewer distinct concepts/constructs/etc. to take into account (especially when meta-programming!).

                                                    If anything, you have destroyed the symmetry (duality) between values and computations.

                                                    EDIT: Added remark about conflation. Fixed typo.

                                                    1. 3

                                                      Pattern matching isn’t there to “alleviate” any “problems” caused by the lack of laziness. Pattern matching is the eliminator for sum types

                                                      Elimination is when we select one of the branches. That can be done before or after evaluating them. That’s the distinction I was making: in my made-up terminology an “eager case expression” would evaluate all branches to normal form, then select the appropriate one to return; a “lazy case expression” would select the appropriate branch before attempting to evaluate any of the branches. You’re right that if, && and || in eager languages are syntactic sugar over pattern matching (case), but my point was that even eager languages use the “lazy case expression” variety, not the “eager case expression”.

                                                      The way those languages achieve such laziness is by making pattern-matching a special language construct. We can’t write user functions which behave the same way (unless we distinguish between values and thunks); note that we can write macros to do this, as is common in Lisps.

                                                      With lazy function calls, such “lazy case expressions” can, in principle, be replaced by eliminator functions (like Church encodings and their variants); although I currently think that would be less nice (see Morte and Dhall, for example).

                                                      If essential properties of the objects being “unified” are lost, it stops being “unification” and becomes “conflation”.

                                                      Sure, but what counts as “essential” is subjective. C programmers might consider pointer arithmetic to be essential, which is lost by high-level representations like algebraic (co-)datatypes. Personally, I’m perfectly happy to e.g. conflate scope with lifetime (i.e. garbage collectors based on liveness).

                                                      I don’t have particularly strong opinions when it comes to either distinguishing or conflating the distinctions used by CBPV, “polarity”, co/data, etc. That’s why I currently fall back on my “symmetry” heuristic.

                                                      If anything, you have destroyed the symmetry (duality) between values and computations.

                                                      By “symmetry” I didn’t mean “duality between two different sorts of thing”, I meant “treating all of these things in a single, uniform way” (i.e. conflating). Fewer distinctions means fewer choices to be made, fewer cases to be handled and fewer combinatorial explosions to tackle. This makes life easier when e.g. parsing, code-generating, interpreting, etc.

                                                      Of course, conflating is a simplistic thing to do; yet such ease is nice to have, so I treat it as the “activation energy” (the ease/value offered) that each distinction must overcome in order for me to use them (at the loss of symmetry).

                                                      Examples of distinctions which I think are generally worth it (for me):

                                                      • Type-level/value-level (as found in dependently-typed languages)
                                                      • Compile-time/run-time
                                                      • Pure/effectful

                                                      Distinctions I don’t think are worth it (for me):

                                                      • Type-level/kind-level
                                                      • Separate constructs for types/values (e.g. type-level computation in Haskell, type families, etc.)
                                                      • Statements/expressions
                                                      • Linear/non-linear types
                                                      • Concrete/abstract syntax (i.e. not using s-expressions)
                                                      • Value/delayed-computation (“polarity”)
                                                      • Partial/total
                                                      • Native/managed

                                                      Of course, these are just my preferences, and they vary depending on what problem I’m tackling and what mood I’m in ;)

                                                      1. 3

                                                        Elimination is when we select one of the branches. That can be done before or after evaluating them. That’s the distinction I was making: in my made-up terminology an “eager case expression” would evaluate all branches to normal form

                                                        This doesn’t make sense. Expressions under binders are not reduced in a call-by-value language, and the left-hand side of a branchn is very much a binder for any variables used as constructor arguments. So what you call “eager case expression” does not exist at all.

                                                        The way those languages achieve such laziness is by making pattern-matching a special language construct.

                                                        A strict language with pattern matching doesn’t “achieve laziness”. It simply evaluates arms at the correct moment.

                                                        Sure, but what counts as “essential” is subjective. C programmers might consider pointer arithmetic to be essential, which is lost by high-level representations like algebraic (co-)datatypes.

                                                        I’m not sure pointer arithmetic is essential, but array manipulation certainly is essential, and memory-safe languages do a very poor job of dealing with it. I’d be willing to give up memory-safety in exchange for a predicate transformer semantics for array manipulation, so long as the semantics is explicitly formalized.

                                                        Personally, I’m perfectly happy to e.g. conflate scope with lifetime (i.e. garbage collectors based on liveness).

                                                        I’m not. Languages without substructural types suck at manipulating anything that doesn’t last forever (e.g., file handles).

                                                        (i.e. conflating). Fewer distinctions means fewer choices to be made, fewer cases to be handled and fewer combinatorial explosions to tackle. This makes life easier when e.g. parsing, code-generating, interpreting, etc.

                                                        And it makes life harder when debugging. Not to mention when you want to formally prove your programs correct. (I do.)

                                                        1. 2

                                                          Expressions under binders are not reduced in a call-by-value language

                                                          Yes, that’s what I’m referring to as ‘a form of laziness’. Expressions under binders could be (partially) reduced, if we wanted to. Supercompilers do this (at compile time), as do the morte and dhall languages, for example.

                                                          what you call “eager case expression” does not exist at all

                                                          The reason that basically no language does this is because it’s a pretty terrible idea, not that it couldn’t be done in principle. It’s a terrible idea because it evaluates things which will be discarded, it introduces preventable non-termination (e.g. with base/recursive cases), and seems to have no upsides.

                                                          My point is that the same can be said for strict function calls, apart from the “no upsides” part (upsides of strict calls include preventing space leaks, timely release of resources, etc.).

                                                          array manipulation certainly is essential… I’d be willing to give up memory-safety… Languages without substructural types suck… makes life harder when debugging… when you want to formally prove your programs correct

                                                          I think this is where our priorities differ. I’m happy enough with an inefficient, simple(istic) language, where I can formally reason about “getting the right answer (value)”, but I don’t care so much about how we arrive there (e.g. order of evaluation, space usage, garbage collection, etc.)

                                                          1. 4

                                                            Expressions under binders could be (partially) reduced, if we wanted to. (…) The reason that basically no language does this is because it’s a pretty terrible idea, not that it couldn’t be done in principle.

                                                            Sure, but not in a call-by-value language. The distinguishing feature (a killer feature!) of call-by-value languages is that variables stand for values, which is not true if expressions are reduced under binders.

                                                            Supercompilers do this (at compile time), as do the morte and dhall languages, for example.

                                                            Except for simple cases where the program’s asymptotic time and space costs are not altered, this is a terrible idea. (Yes, even when the program’s performance is improved!) I want to reason about the performance of my program in terms of the language I am using, not whatever machine or intermediate code a language implementation could translate it into. The former is my responsibility, the latter is beyond my control.

                                              2. 5

                                                Lazy evaluation makes it hard to reason about the … termination of a program

                                                A program terminates at least as quickly when evaluated non-strictly as it terminates when evaluated strictly, so that can’t be true.

                                                1. 3

                                                  For once I second @Yogthos. Lazy evaluation is certainly useful, but not as the default! If you care about algorithms, and IMO every programmer ought to, strict evaluation as the default makes analysis easier than lazy evaluation (“simply substitute and reduce” vs. “keep track of which thunks have been forced”) and gives tighter asymptotic bounds (worst-case vs. amortized) on running times.

                                                  1. 4

                                                    Strict evaluation should not be the default, you lose composition of algorithms.

                                                    1. 2

                                                      Eta-expand, then compose. Voilà.

                                                      1. 1

                                                        Eta-expand then compose what?

                                                        1. 3

                                                          For instance, rather than say foo . bar, where foo and bar are arbitrarily complicated expressions, you say \x -> foo (bar x).

                                                          As for composing complicated algorithms - it’s totally overrated. Instead of designing libraries around a mess of higher-order functions, oops, Kleisli arrows, oops, profunctors, oops, who knows, I’d rather reify every intermediate state of a complex operation using a custom abstract data type, and then only export procedures that perform individual atomic steps - good old-fashioned first-order procedures! Composing these atomic steps into the exact algorithm the user wants is best done by the user himself. Maximum flexibility and no abstraction overhead. But of course, you need decent support for abstract data types for this to work.

                                                          EDIT: Added long paragraph.

                                                          1. 4

                                                            I also have to do that for everything in foo and bar, then manually fuse -> code duplication.

                                                  2. 2

                                                    Perhaps the issue is less direct: laziness tempts us to use infinite (co)datastructures, which we must handle carefully (e.g. don’t take the length of an infinite list).

                                                    1. 1

                                                      Correction: I should have said “when evaluated lazily” not “non-strictly”. I think as written what I said was false.

                                                    2. 2

                                                      By the way, that’s not really what Shapr meant by “which Haskell features aren’t considered good for production code”!

                                                  1. -1

                                                    Pretty amazing that someone I consider a leading mind in fuzzing and security can manage to start a post on currency with the barter system fiction. It would be like starting a discussion of unicode with its origins in the need for emoji… eek. which is to say I should’ve taken the ride through that to the next paragraph. I still disagree with some of the angles concerning the origins of coinage but overall it’s relatively solid.

                                                    1. 11

                                                      And then the next paragraph starts:

                                                      It is a nice parable, but it probably isn’t very true. It seems far more plausible that early societies relied on the concept of debt

                                                      1. 8

                                                        I fail fast? 😳

                                                        1. 2

                                                          Ah, someone’s read David Graeber.

                                                      1. 1

                                                        This week I was reading about the theoretical underpinning of recursive definitions: fixed points. Whenever you define something recursively, you are technically taking a fixed point of a continuous function (yes, you read that correctly!). There is some really cool math behind this called domain theory.

                                                        Recursive definitions don’t need fixed points. c.f. Roza Peter Recursive functions. Recursion is a simple thing. It’s weird how people take pride in making the simple seem utterly complex. See https://plato.stanford.edu/entries/recursive-functions/ for a nice summary.

                                                        1. 6

                                                          Unless you want to implement recursive functions in a pure language. Because you need to have evaluated the function and bound the result to a name in order to bind the name when it occurs within the body, you have a bit of a chicken-egg problem. But you can use the Y combinator (which is really about finding fix points) and a modified version of the recursive function definition to achieve general recursion in a pure (read: lambda calculus) setting (of course, it is usually implemented with mutable cells, as far as I’m aware).

                                                          It’s not “making something complex out of something simple”, it is an important part of the history of computer science, the discovery that allows Lambda Calculus to achieve general computation and be Turing complete.

                                                          Getting into the complicated roots that gave rise to something simple != ruining something simple.

                                                          tl;dr: being dismissive and elitist isn’t a good look

                                                          1. 3

                                                            Peter’s work is in mathematics, not programming languages. It is set in the context of an arithmetic approach to computability which is equivalent in expressiveness to the lambda calculus, but much more clear and simple. I wonder how much of the neglect of the Skolem/Peter line of work is due to a preference for complexity, and how much is due to Peter’s gender, but whatever the cause: in mathematics, it is possible to choose to define recursion from basic principles without getting into the complexities that grafting recursion on to lambda calculus entails. The way recursion works in programming languages is, in my opinion, better represented in terms of recursive arithmetic than in the lambda calculus. If you think of a computable function something that can be defined by an algorithm, the apparent paradox of recursion in LC evaporates.

                                                            No criticism of the poster - that’s the orthodox point of view. But to me it’s a wrong turn.

                                                            1. 2

                                                              It would help in a rebuttal like this if you gave examples of people doing exactly what you’re describing. I imagine it’s been done if it’s much easier. Then, any readers more knowledgeable about math or formal methods might look into such things more. We might get another interesting post out of it.

                                                              1. 1

                                                                Recursion has been a known technique in mathematics for a very long time. It generally does not involve taking a fixed point on a continuous function and has nothing to do with “domain theory” except in very specialized circumstances. I think that the main result of type-theory/formal methods has been to create an obscure, specialist vocabulary.

                                                                1. 1

                                                                  Domain theory and fixed points on ωCPOs are only needed in the context of polymorphism. Simply-typed lambda calculus has set theoretic models, after all. I doubt very much that the “arithmetic approach to computability” treats polymorphism.

                                                                  1. 2

                                                                    That’s great. It is interesting that the approach taken to computability by Skolem, which is the primary basis of Godel’s proof, now merits skeptical quote marks!

                                                              2. 1

                                                                I wonder how much of the neglect of the Skolem/Peter line of work is due to a preference for complexity, and how much is due to Peter’s gender, but whatever the cause: in mathematics, it is possible to choose to define recursion from basic principles without getting into the complexities that grafting recursion on to lambda calculus entails.

                                                                Does the Skolem/Peter line account for polymorphism and higher-order functions? If not then there’s no need for the conspiricy theories. They are where the tricky bits of of programming language semantics start, after all. Programming language theorists didn’t make their subject complicated just for the hell of it.

                                                                1. 1

                                                                  Conspiracy theory? Give me a break. The original claim was: “ Whenever you define something recursively, you are technically taking a fixed point of a continuous function (yes, you read that correctly!).”

                                                                  If it had been: “Whenever you define something recursively in typed lambda calculus (or similar) , you are technically taking a fixed point “, I would not have commented.

                                                          1. 2

                                                            Depending on what sort of work we are counting, I am either Exceptional or Abhorrent. I bill about 20 hours a month of software consulting, which amounts to about 30 wall-clock hours a month. Said work pays very well, and earns me enough for about half of my living expenses and bills, which, objectively, is incredible. However, in order to earn the other half, I work about 35 additional hours per week, in non software industries. These jobs often require working until 10pm - 2am or are physically exhausting. Objectively, if not for the first source of income, the latter would be tragic.

                                                            (for the sake of being objective, I’ll admit that I choose to live in a place with a sky high cost of living, and that I have ornery ethical standards about the clients I will take.)

                                                            1. 5

                                                              Can’t you scale up to 40 hours a month of consulting?

                                                              1. 1

                                                                I can only dream. Finding clients with enough hours has proven tricky. About twice a year they will offer that much work, but it is the exception, not the rule.

                                                                1. 1

                                                                  Do you work in a really specific niche? It’s hard to imagine a line of work where it’s straightforward to find 20 hours a work but difficult to find 40!

                                                                  1. 1

                                                                    I work in a rather broad set of fields, but my personal goal for the last few years has been to work as much as possible for open source or non profit folks. perhaps unsurprisingly, they often have strictly limited budget per unit time.

                                                            1. 7

                                                              A E S T H E T I C

                                                              Any chance you could get lynx looking at lobsters? :3

                                                              1. 9

                                                                Sure thing!

                                                                https://u.teknik.io/bfG9p.jpg https://u.teknik.io/rAyqc.jpg

                                                                Is it everything you were hoping for?

                                                                1. 2

                                                                  Oh man, I was hoping for a screenshot of this thread!

                                                                2. 2

                                                                  Casually shilling for a possibly relevant project

                                                                1. 15

                                                                  I was disappointed that there were no demographic questions - that’s a vital area which the Rust survey creators put a lot of work into. I expect it was due to the survey creators not seeing it as important enough to justify the effort of doing it right, which I know is considerable. I understand that decision, but it’s frustrating, because it’s very important to some of us.

                                                                  1. 16

                                                                    I agree that demographics are important! I definitely want to include them in next year’s survey. This is the first survey I’ve ever published. I didn’t want to get the demographic questions wrong or otherwise mishandle them. That’s why I decided to focus on the technical questions. The survey was developed in the open (see this issue); next year’s will be too. I would be delighted to have you help out with the demographic questions.

                                                                    1. 13

                                                                      Just copy ours :).

                                                                      Jest aside, we’re cool with anyone taking these questions like all our other open source output.

                                                                      Also, there’s a huge problem currently: most languages don’t run these kinds of surveys and then many don’t share a common core. It’s hard to read a lot from them.

                                                                      In case of Rust, we’re in the lucky position to actually have run two of them, so we can at least put this year’s number in relationship to last year’s.

                                                                      But for the rest? Are we doing better then language X? Worse? Only gut feeling.

                                                                      I don’t see this as a competition, there’s rarely been a structured approach to mapping communities.

                                                                      In any case, if you’d like to exchange experiences, please feel free to contact community-team@rust-lang.org

                                                                      1. 8

                                                                        I’m happy to hear that! And I’m also happy to be contacted to comment on concrete proposals, when next year’s survey is at that stage; I don’t have the bandwidth to be involved more than that.

                                                                        I suspect the team that did the Rust survey will also be happy to advise about these topics. I know they’ve talked about it a bunch here on lobste.rs, and those old discussions are still in the archives somewhere.

                                                                      2. -2

                                                                        You mean the part about “underrepresented groups” or whatever on the Rust survey? Why do you think that is important?

                                                                        One of my favorite things about the Haskell community is that everyone is too busy doing actual technically impressive stuff to worry about e.g. how many gay people happen to be using it.

                                                                        To be blunt, I think that sort of thinking (obsessing over whether an organic community follows one’s arbitrarily constructed ideals for what it should look like) is a cancerous mind-suck that detracts from actually productive work.

                                                                        To be a little more blunt, I think the fact that Haskell has a reputation as being extremely technical has actually helped the community a great deal, at least just by virtue of the fact that it scares away people who are primarily involved in software as a means to push some political agenda.

                                                                        Late edit: feel free to respond instead of just downvoting, would be happy to be wrong here.

                                                                        1. 33

                                                                          This is downvoted already, I’ll bite anyways. First of all, I think your comment shows that you have no idea what we are doing there.

                                                                          Gathering demographics questions is much more then what you narrow it down to. It’s telling that the only thing you can come up with is “how many gay people happen to be using it”? It’s also: where do people live, would they want to travel to a conference, etc… It cuts out the guesswork. You know what? When you measure, you also sometimes find out that things are just okay. No need to do something. Great! Sometimes, you find something odd. Then you might want to investigate. It’s a community survey. We want to know about people, not about technology. But social groups are also a thing to check.

                                                                          The Rust community also does production user surveys, which are die-hard technical and very detailed, usually specific in certain areas like embedded and or gaming. We seek out users willing to do that and set up meetings to figure out the issues.

                                                                          To be blunt, I think that sort of thinking (obsessing over whether an organic community follows one’s arbitrarily constructed ideals for what it should look like) is a cancerous mind-suck that detracts from actually productive work.

                                                                          To be blunt too: It’s shit that you call my work “not productive”. Here’s a thing: I don’t want to contribute to rustc or Servo. Why? I code all day, I don’t want to code at night. I’m happy that other people want to. I still want to contribute to FOSS. In the last 5 years, I’ve set up 2 foundations, 11 conferences and managed around 250000 Euros to run all these things. I signed leases that could have bankrupted me. I managed to find ways to run 2-days conferences that cost 100EUR and still cover all expenses of speakers, attendees and those that cannot pay 100 Euros. I love that work. People are indeed very fair about this. Those that have more give, those that don’t, don’t. And I want everyone to benefit from that. My whole work revolves around the question “Who’s not here, and why?”. It’s my hack. Nothing of that is fundamentally special, other people could have done it.

                                                                          And you know what? We measure. We don’t go out “hey, please do X because I think it works”. No, we go “hey, we did X and metric Y improved”.

                                                                          It’s also amazing how many people just need a “have you considered programming might be something for you?” and then just head of and learn it. But the question needs to be asked a couple of times.

                                                                          It’s shitty to go on an concern troll around people doing precisely that to better do “productive work”.

                                                                          There’s no way to get me to work on other things without paying me. And you know what I like about the Rust community? They don’t concern troll me. They go: cool, if that’s what you want to do, please do it for us. It’s not like I bind a lot of resources. Community work works best if you don’t have many cycles. We align on a goal and then we do a lot of footwork.

                                                                          Sure, there are cases where issues arise and social work becomes focus, but that’s fine. Interestingly, the work of community workers is often to talk about issues before they come a trashfire, go to reddit and subsequently to 4chan.

                                                                          There’s also the “fixed cake” fallacy at work here: The belief that if we expand our community beyond a certain group, another group has to take the impact. That isn’t the case. The cake is not fixed. The market for programming languages is growing in absolute terms, also our communities are growing in absolute terms. These are effect to be appreciated and taken into consideration.

                                                                          Different folk need to be addressed in different fashion and thats fine. These surveys give us a bearing in where we want to invest our time or where things just work.

                                                                          If you absolutely want to talk in programming terms, we’re profiling our work. I find it amazing that there is so much pushback when we actually check on our successes.

                                                                          It’s shitty of people to devalue that work. A work, which has to be said, is more often done by women and people of color in many communities. Many of which are masters of it.

                                                                          There’s two options here: I do this work within a community or I don’t. It’s as simple as that. No “more productive” trolling.

                                                                          I structured work on these issues is still “cancerous mind-suck” for you, then go ahead. But say it to my face when you meet me.

                                                                          To be a little more blunt, I think the fact that Haskell has a reputation as being extremely technical has actually helped the community a great deal, at least just by virtue of the fact that it scares away people who are primarily involved in software as a means to push some political agenda.

                                                                          I just leave this here:

                                                                          So I just met Simon Peyton Jones (creator of Haskell) and chatted with him for a bit. Asked him his thoughts on Rust and he said he thinks it seems exciting and he was jealous of the great community we have. Just thought I would let you guys know :)

                                                                          (From: https://www.reddit.com/r/rust/comments/5yo24a/meta_rust_jealousy/)

                                                                          This was, by the way, the best compliment I ever saw, I respect Simon very much.

                                                                          We have an awesome many people primarily interested in software working in the Rust community. But they don’t throw the community workers under the bus like you do. That’s why I run a 6-monthly Rust conference and not a 6-monthly Haskell conference.

                                                                          I love Haskell, but there’s reasons I’m not active there. Still, for anyone that wants to learn techniques and procedures, by all means get in touch.

                                                                          Communities don’t happen at random. They work through network effects and feedback and these can be moderated and improved.

                                                                          Finally, to be very blunt: you just cost me 45 minutes of community work, which I’d have preferred to fill with something productive.

                                                                          But I also think it’s worth putting it out for others to read.

                                                                          EDIT: I’d also like to state that I know quite some people in the Haskell community caring very deeply about this. haskell-cafe is still one of my inspirations for a cool space to make. But that space is intentional, not organic.

                                                                          1. 10

                                                                            Thank you very much for writing this. It will serve as a great resource the next time I spot a similar comment in the wild.

                                                                            1. 4

                                                                              Found this thread late, but wanted to say thanks @skade for the consistently insightful commentary on community here, and for you work in the Rust community. I don’t work with Rust much, but on the occasions when I’m working on community-building, the Rust community is one of the first places I go to for examples of how to do it well.

                                                                              1. 1

                                                                                Thanks for responding.

                                                                                It’s telling that the only thing you can come up with is “how many gay people happen to be using it”?

                                                                                That’s the only demo data you put on https://blog.rust-lang.org/2017/09/05/Rust-2017-Survey-Results.html

                                                                                Please, tell me how you thought that was “telling”.

                                                                                But social groups are also a thing to check.

                                                                                Check and… what?

                                                                                The Rust community also does production user surveys,

                                                                                Do you see me objecting to those?

                                                                                To be blunt too: It’s shit that you call my work “not productive”.

                                                                                Sorry you feel that way. I think a lot of things aren’t productive, including some things I do, so you shouldn’t take it personally.

                                                                                In the last 5 years, I’ve set up 2 foundations…

                                                                                Cool, but you don’t need to justify your relevance because I called one of your interests into question.

                                                                                It’s shitty to go on an concern troll around people doing precisely that to better do “productive work”.

                                                                                Actually, I wouldn’t say anything if I just thought you were just wasting your own time; further than that, I think obsessing over demos is actively counterproductive. The utility to the community is negative, not zero.

                                                                                There’s also the “fixed cake” fallacy at work here: The belief that if we expand our community beyond a certain group, another group has to take the impact.

                                                                                It’s not so much “taking the cake” as “ruining the cake”. If you “expand your community” to include demo-obsessed identity politicians, the community is going to become actively worse.

                                                                                A work, which has to be said, is more often done by women and people of color in many communities.

                                                                                Why did you feel this comment was relevant to the conversation? I have several hypotheses, but I’d prefer not to assume your motivations.

                                                                                I structured work on these issues is still “cancerous mind-suck” for you, then go ahead. But say it to my face when you meet me.

                                                                                Sure. I don’t have an aversion to arguing about the social costs of different activities in person any more than I do online.

                                                                                That’s why I run a 6-monthly Rust conference and not a 6-monthly Haskell conference.

                                                                                Right, that’s what I said earlier; something about Haskell pushes away people with demographic planning aspirations, which I like a lot.

                                                                                Communities don’t happen at random… these can be moderated and improved.

                                                                                This is just fundamentally untrue; most of the best communities are more or less spontaneous. Many communities I love (such as lobsters) are good precisely because they’re minimally moderated.

                                                                                haskell-cafe is still one of my inspirations for a cool space to make. But that space is intentional, not organic.

                                                                                The list is, afaik, unmoderated, and the Haskell IRC (one of the best chats on freenode) is also totally unmoderated. Your example is evidence against your claims.

                                                                                1. 6

                                                                                  Communities don’t happen at random. They work through network effects and feedback and these can be moderated and improved.

                                                                                  This is just fundamentally untrue; most of the best communities are more or less spontaneous. Many communities I love (such as lobsters) are good precisely because they’re minimally moderated.

                                                                                  This is false for Lobsters, both historically and currently.

                                                                                  Speaking historically, you cut out the key phrase “network effects” from the quote. The Lobsters of early 2014 was a very different, nearly empty place. The current state of Barnacles is quite similar: low activity by any metric you care to measure (traffic, stories posted, comments, votes, etc.) and a negligible sense of community. Online communities start as failures and have to overcome the chicken-and-egg problem that it’s a waste of an individual’s time to participate until quite a lot of other people are already participating.

                                                                                  And on an ongoing basis, Lobsters requires daily attention to moderation and maintenance. Most of it is design, small edits, comments, and private messages. The rare, exciting things like deleted comments and banned users are the tip of an iceberg. It’s all the small, constant attention that keeps the positive feedback loops working to power a successful community instead of killing it. This is also true of Haskell-cafe.

                                                                                  The theme I take from your comments seems to be that the work you are unaware of doesn’t exist and, if it does, it must be worthless. I don’t understand that dismissive cynicism well enough to respond meaningfully to it, so all I can do is point out these surface-level inaccuracies.

                                                                                  1. 2

                                                                                    Lobsters requires daily attention to moderation and maintenance.

                                                                                    I seem to recall jcs saying that he never deleted anything if he could avoid it, and indeed that seemed to be the case. It seems that you are now taking a somewhat more active stance, but historically lobsters has had very little/none of what I would call active moderation.

                                                                                    Most of it is design, small edits, comments, and private messages… This is also true of Haskell-cafe.

                                                                                    SPJ sending out an email about being nice isn’t community moderation or management. Neither is general site maintenance. I’m not sure how you would conclude that I disagreed with any of these things unless we’re using very different definitions for a number of words.

                                                                                    The theme I take from your comments seems to be that the work you are unaware of doesn’t exist

                                                                                    I’m aware of all the examples you gave; they just aren’t the kind of obsessive, inorganic micromanagement I was objecting to.

                                                                                  2. 4

                                                                                    That’s the only demo data you put on https://blog.rust-lang.org/2017/09/05/Rust-2017-Survey-Results.html

                                                                                    I don’t get it. That page contains a bar chart with all sorts of demographic categories on it, just above “Diversity and inclusiveness continue to be vital goals for the Rust project at all levels.”

                                                                                    1. -2

                                                                                      Me:

                                                                                      e.g. how many gay people happen to be using it.

                                                                                      Guy who responded to me:

                                                                                      where do people live, would they want to travel to a conference, etc…

                                                                                      What kind of demo data do you see them sharing on that page? I’m not really sure what you’re confused about; you seem to be agreeing with me.

                                                                                      1. 7

                                                                                        The blog post is an editorialised overview, the 2016 one covers that. https://blog.rust-lang.org/2016/06/30/State-of-Rust-Survey-2016.html#survey-demographics

                                                                                        There have not been notable changes, so it wasn’t mentioned again.

                                                                                    2. 4

                                                                                      As the person who started the Haskell IRC channel and as an active moderator of said channel, moderation happens often. There’s a team of motivated users on the #haskell-ops IRC channel and we have to step in more than I’d prefer.

                                                                                      Good communities require much work and regular feedback.

                                                                              1. 1

                                                                                As ever, an example would help.

                                                                                1. 19

                                                                                  This is a fantastic and insightful analysis. You could debate it, of course, but the fact that Lisp emerged when the alternatives were so low-level is amazing; the comparison to calculus is a good one.

                                                                                  1. 3

                                                                                    Following the Maxwell equations analogy: if Lisp is analogous to vector calculus, today we have programming language analogues of tensor calculus, differential geometry, de Rham cohomology, etc.

                                                                                    1. 3

                                                                                      Which languages are they? Almost all currently-used languages I can think of come from the Algol stable, rather than Lisp; to use the analogy they are built from counting pebbles rather than vector calculus. Clojure and Elixir seem like the only counterexamples I can recall.

                                                                                      1. 6

                                                                                        Tensor calculus makes finer distinctions that vector calculus (at least as taught to engineers) totally glosses over: contravariant vs. covariant indices, tensors vs. pseudotensors vs. tensor densities, etc. These distinctions are useful, because they prevent you from wasting time saying things that are geometrically and physically nonsense. Does this remind you of a certain language feature that causes endless online debates, and neither Clojure nor Elixir has?

                                                                                        If Lisp is analogous to a tool that was good enough to formulate classical electrodynamics, then we today have analogues of tools that are good enough to formulate general relativity, quantum mechanics, etc.

                                                                                        1. 2

                                                                                          Does this remind you of a certain language feature that causes endless online debates, and neither Clojure nor Elixir has?

                                                                                          Wait, I thought Clojure does have contracts

                                                                                          1. 3

                                                                                            Runtime-enforced contracts at best distinguish wanted from unwanted meanings. They don’t distinguish the presence from the absence of a meaning (i.e., nonsense). For if there were no meaning, there would be no program to run.

                                                                                            1. 2

                                                                                              The way I think of it is that runtime-enforced contracts allow you to fail quickly in response to bad data. Check a POST body against a JSON schema and return 400 if it doesn’t match, and the like. Compile-time “contracts” (i.e. types) allow you to be certain that the data you are handling in a given function or module is valid.

                                                                                              Runtime contracts could be seen as protecting against defects in the type system. “Integer” may be the most limiting type expressible in a given language, but a contract can say “this value is between 0 and 9.”

                                                                                              1. 1

                                                                                                Compile-time “contracts” (i.e. types)

                                                                                                “Compile-time contracts” needn’t be types. It could be something you proved on your own the traditional way, i.e., using paper and pen. Why limit yourself to the subset of mathematics that one specific tool (a type checker) can handle?

                                                                                                Runtime contracts could be seen as protecting against defects in the type system. “Integer” may be the most limiting type expressible (…)

                                                                                                This is a virtue, not a defect. At some point you start hitting diminishing returns when you try to prove everything with types. Other mathematical tools are more flexible and scale better to more complex scenarios.

                                                                                                1. 4

                                                                                                  To be frank, I don’t trust paper and pen proofs. You can prove something ten ways from Sunday, and then get a NULL pointer where you don’t expect it and blow up. I think of the Knuth quote, “Beware of bugs in the above code; I have only proved it correct, not tried it.” That’s not to say that verification and proof outside of the code is valueless (certainly not), but if I’m relying on it I would also encode my assumptions in runtime contracts if they exceed the power of the type system to encode.

                                                                                                  1. -4

                                                                                                    To be frank, I don’t trust paper and pen proofs.

                                                                                                    This is only natural if you don’t know mathematics. The fix is obvious: learn mathematics.

                                                                                                    1. 9

                                                                                                      I’ve got a PhD in mathematics and therefore the number of mistakes I’ve made in so-called “proofs” is staggering.

                                                                                                      1. 6

                                                                                                        There’s a reason we left pen and paper proofs for mechanically-checked proofs with minimal TCB’s. People were screwing up too much. You should thoroughly read this paper by Guttman:

                                                                                                        http://www.cypherpunks.to/~peter/04_verif_techniques.pdf

                                                                                                        Key except illustrating the problem:

                                                                                                        “The problems inherent in relying purely on a correctness proof of code may be illustrated by the following example. In 1969, Peter Naur published a paper containing a very simple 25-line, text-formatting routine which he informally proved correct. When the paper was reviewed in Computing Reviews, the reviewer pointed out a trivial fault in the code which, had the code been run rather than proven correct would have been quickly detected. Subsequently, three more faults were detected, some of which again would have been quickly noticed if the code had been run on test data.

                                                                                                        The author of the second paper presented a corrected version of the code and formally proved it correct (Naur’s paper only contained an informal proof). After it had been formally proven correct, three further faults were found which, again, would have been noticed if the code had been run on test data.

                                                                                                        This episode underscores three important points made earlier. The first is that even something as apparently simple as a 25-line piece of code took some effort (which eventually stretched over a period of five years) to fully anaylse. The second point is that, as pointed out by DeMillo et al, the process only worked because it was subject to scrutiny by peers. Had this analysis by outsiders not occurred, it’s quite likely that the code would’ve been left in its original form, with an average of just under one fault for every three lines of code, until someone actually tried to use it. Finally and most importantly, the importance of actually testing the code is shown by the fact that four of the seven defects could have been found immediately simply by running the code on test data.”

                                                                                                        Mathematics alone won’t help if one is verifying algorithms and/or code. There’s many ways to screw up. The correct solution might have to take a heavy amount of proofs that are then thoroughly checked by human minds and/or tools. Most people working alone on pencil and paper might be making serious mistakes that will end up in the codebase.

                                                                                                        See also my submission Don’t Trust the Math:

                                                                                                        https://pastebin.com/zz7YZZUk

                                                                                                        1. 2

                                                                                                          These are different problems. Paper and pencil proofs are to convince people and to understand the principles. Mechanical proofs are for details - but they can be wrong on bigger issues. The big limitation right now is we don’t have good ways of thinking about complex state systems mathematically.

                                                                                                        2. 6

                                                                                                          I majored in mathematics and don’t think it obviates the need for careful testing.

                                                                                                          1. 5

                                                                                                            “Mathematics” does not govern software. Software and hardware do. There are edge cases that writing a mathematical proof (on paper!) does not cover. Many of them. That’s the meaning of the Knuth quote I included above. Unless you think he doesn’t know math, either.

                                                                                                            1. 2

                                                                                                              I’d argue that people govern software - people, in all their irrational, legally mandated requirements that have to be satisfied before they’ll sign the functional acceptance agreement!

                                                                                                            2. 5

                                                                                                              Condescension is not knowledge. Real mathematicians know that proofs can be wrong. Real engineers/scientists know that correct proofs may be for mathematical models that miss some aspect of the physics. Being able to use some terms from category theory doesn’t make you qualified to be in either one of those categories.

                                                                                                2. 6

                                                                                                  Lambda functions are fairly widely implemented in most mainstream languages by now (C#, C++ IIRC, Rust, PHP)

                                                                                                  While they are still mostly Algol-like, I believe that a lot of the things LISP invented/discovered have slowly bled into other languages we use today.

                                                                                                  1. 4

                                                                                                    I believe that a lot of the things LISP invented/discovered have slowly bled into other languages we use today.

                                                                                                    What did you had in mind? As far as I can tell most of the languages we use today lack those iconic lisp traits:

                                                                                                    • homoiconicity
                                                                                                    • hygienic macros
                                                                                                    • interactive development - here I’m referring to the situation where there is runtime error and lisp system stops, lets you fix the code, recompile only the changed parts and continue instead of forcing you to fix and restart whole interaction
                                                                                                    1. 1

                                                                                                      Maybe ultra-high-level programming, memory safety, garbage collection, and DSL’s could be on the list of what went mainstream. If looking at LISP machines, keeping your whole stack in high-level languages as much as possible. There’s containers and VM’s for that now. They were also among earliest IDE’s with interactive development and debugging. Just a few ideas that popped into my head rather than solid since the lineage of programming languages is wide enough for me to forget or just not know something in a quick post. :)

                                                                                                  2. 1

                                                                                                    Odd then that not only has the vast majority of scientific computing bypassed Lisp, but the higher level mathematical tools are mostly built on Algol descended languages.

                                                                                                3. 1

                                                                                                  The other one that came out a few years after McCarthy was META II:

                                                                                                  https://en.wikipedia.org/wiki/META_II

                                                                                                  He liked that language for similar reasons in terms of DSL building or just expressing transformations. Kay ended up merging LISP variants and META successors in his later work in STEPS project.

                                                                                                  http://www.vpri.org/pdf/tr2007008_steps.pdf

                                                                                                1. 3

                                                                                                  While I like the ingenuity, I question whether a case could be made that the practice is unfair in some way under EEOC law. It might be harder because the onus is on the candidate but it seems kind of grey to me…

                                                                                                  My current employer, and other employers before, have tried to run a consistent process, such that all candidates, for a given job, are given roughly the same experience, to avoid a situation where someone who didn’t get hired can’t claim their tasks were harder than others and they were being discriminated against.

                                                                                                  Anyone here happen to be in HR and/or know better than me, the laws around hiring practices?

                                                                                                  1. 1

                                                                                                    … have tried to run a consistent process

                                                                                                    This is addressed in the section called “What About Consistency?”

                                                                                                    1. 2

                                                                                                      Yes, but my inquiry goes beyond that, I think? They certainly acknowledge the pssoibility of having issues. My question is “what issues do they actually have that may not be obvious?” Like, is there case law resulting in a successful argument for a discrimination case given interviews like this? Does it go beyond the typical diversity argument that the author pokes at?

                                                                                                      1. 1

                                                                                                        No it’s not? Did you actually read the article?

                                                                                                        There’s a growing body of evidence that structured and consistent interviews are the best predictor of future job performance. Plus, they help limit cultural and unconscious personal biases held by organizations and individuals. A collaboratively designed, per-candidate interview is about 180º away from this approach as possible, and honestly our evaluation process is still entirely unstructured and vulnerable to these biases. It hasn’t stopped us from making offers to women, people of color, LGBTQ individuals, and more but I can’t claim there’s any systemic protection against this disfunction. Nor can I even guess how — or if — this scales beyond 10, 100, 1000 people. We’re not there yet, although some day we might be (have I mentioned we’re hiring?).

                                                                                                        highlight is mine.

                                                                                                        1. 2

                                                                                                          Just because someone has made offers to women, POC, LGBTQ etc doesn’t mean that their process is not vulnerable to bias. It just means the employees they happened to start with possibly aren’t overt bigots.

                                                                                                    1. 3

                                                                                                      Observations

                                                                                                      • I can’t do that algorithm quickly in my head.
                                                                                                      • I’d probably get a mobile app to do it for me,
                                                                                                      • at which point I may as well
                                                                                                        • choose a master password and hash it with the domain name, or
                                                                                                        • just use a password manager on my mobile device.
                                                                                                      1. 12

                                                                                                        Neither of these approaches are perfect: With the uniform representation approach we lose control over how our data is laid out in memory, and with the template instantiation approach we lose modularity and polymorphic recursion.

                                                                                                        Which is why I have been saying for a while - these ought to be two different forms of polymorphism, so that you can explicitly choose the form you need when you write your program. More precisely:

                                                                                                        ML-style polymorphism:

                                                                                                        • ∀, not Π
                                                                                                        • Always rank-1
                                                                                                        • Always inferred
                                                                                                        • Always monomorphized

                                                                                                        Fω-style polymorphism:

                                                                                                        • Π, not ∀
                                                                                                        • Rank-N or even impredicative if you want
                                                                                                        • Explicit type function application
                                                                                                        • Never monomorphized

                                                                                                        I’d even advertise them as “static” and “dynamic” polymorphism.

                                                                                                        1. 2

                                                                                                          Could you write up a blog post or something about this? It sounds really interesting and deserves to be spread more widely!

                                                                                                          1. 2

                                                                                                            I suspect I haven’t expressed myself sufficiently clearly, but anyway, here it goes: https://meaningfulcomputing.wordpress.com/2017/10/23/two-kinds-of-parametric-polymorphism/

                                                                                                            1. 1

                                                                                                              Thanks!

                                                                                                        1. 2

                                                                                                          Perhaps this becomes slightly more obvious (or perhaps not) when you notice that

                                                                                                          class Class a where
                                                                                                              foo :: <type depending on a>
                                                                                                              bar :: <another type depending on a>
                                                                                                              ...
                                                                                                          

                                                                                                          is just another way of saying

                                                                                                          data ClassDict a = { foo :: <type depending on a>
                                                                                                                             , bar :: <another type depending on a>, ... }
                                                                                                          
                                                                                                          class Class a where
                                                                                                              classDict :: ClassDict a
                                                                                                          

                                                                                                          In other words its easy to map between the collection of class members and its dictionary type.and the typeclass instance is just a privileged choice of value of dictionary type. In fact I kind of wish class definitions were given like

                                                                                                          class Class a -> ClassDict a
                                                                                                          

                                                                                                          or something equally silly.

                                                                                                          1. 1

                                                                                                            You can already write the latter thing. Typeclasses are, most practically, a mechanism for doing this automatically/globally/efficiently.

                                                                                                          1. 41

                                                                                                            Not for proving theories about […]

                                                                                                            Come now. Types establish facts and enforce useful equalities that help in writing and maintaining software. It makes the code more amenable to human comprehension and along the way it gives you mechanical assistance, which is huge. They’re also essentially “free” proofs as the only proof required is the code-that-does-the-thing-you-want-to-do. The only time this isn’t the case is if you’re using a DTPL and need to establish something not eminently obvious from a straight-forward implementation. With type inference you also don’t have to state your expectations. You can write the code that you think should work and see what type you get. In Haskell you can then flip that around, declare some types, set their implementations to undefined, and then play with the types to see if you’re headed where you want to get. Particularly useful for library integrations. Like a “bidirectional conversation” with the compiler about what’s going on.

                                                                                                            I, for one, embrace having become a cyborg.

                                                                                                            I don’t really want to get sucked into this debate, but I’ll note that I don’t often see Haskellers seeking this debate out like they used to. Myself included. It seems to mostly be users of untyped languages feeling insecure/defensive about it. You can do what you want, but don’t get upset when it instigates rebuttals. I think some of the communication difficulties here are related to how I didn’t really appreciate types until I grokked a language with nice types. Then I saw how there was no “trade-off”, all stages of a project or idea could become faster and easier, from ideation to EOL maintenance.

                                                                                                            I used to use Clojure and Datomic in production and let me say that the proof is not in the pudding for what Rich is saying. Datomic was a spectacularly poorly managed product. Getting irritated with unnecessarily difficult-to-debug runtime errors in a few hundred lines of Clojure is what drove me to finally learn Haskell, so I guess I should thank Rich for that.

                                                                                                            There’s a great thread started by Chris Done here.

                                                                                                            Other good replies

                                                                                                            1. 16

                                                                                                              It makes the code more amenable to human comprehension

                                                                                                              No, not for everyone. I find thinking in types way more constraining than thinking in values at runtime. Apparently, there are many people like me.

                                                                                                              and along the way it gives you mechanical assistance, which is huge.

                                                                                                              No, it’s not huge. There’s no conclusive study showing that type checking improves quality. It usually boils down, again, to personal preference of particular people doing the coding.

                                                                                                              I’m not against type checking in general (heck, Rust is one of my favorite languages, as is Python). But the outright arrogance of quite a few people considering type checking to be a clearly superior paradigm, here on Lobste.rs and elsewhere, starts getting on my nerves, sorry.

                                                                                                              It seems to mostly be users of untyped languages feeling insecure/defensive about it.

                                                                                                              That sounds like confirmation bias and doesn’t advance the discussion. Look at how every pro-dynamic typing article is upvoted (this one and one of Bob Martin’s recently) and gets shredded in the comments, with gusto.

                                                                                                              1. 8

                                                                                                                No, not for everyone. I find thinking in types way more constraining than thinking in values at runtime. Apparently, there are many people like me.

                                                                                                                Can you describe what you mean by that? Are you saying the runtime values do not correspond to any static type? When I write in a dynamic language, I still think about things in terms of what type they correspond to. Do you not do this?

                                                                                                                1. 3

                                                                                                                  Right… Since I keep failing to write a good blog post about it, let me use this opportunity to try and articulate this here.

                                                                                                                  Yes, runtime values do have types, but that alone is both too much and too little:

                                                                                                                  • too much in a sense that I usually don’t care about the majority of the allowed operations on this type at a particular place in my code
                                                                                                                  • too little in a sense that a type does not convey semantics (okay, it’s a string, but what it represents?)

                                                                                                                  Consider an example in (hopefully) self-descriptive Python:

                                                                                                                  def read_safe(filename):
                                                                                                                      if os.path.exists(filename):
                                                                                                                          return open(filename).read()
                                                                                                                      return 'default_value'
                                                                                                                  

                                                                                                                  I don’t care here if I can, say, upcase the filename, or if it’s representable as a valid utf-8, or of any other string properties. The only thing that this code actually cares about is that this value can be checked against if a certain file exists and can be opened by this name.

                                                                                                                  Conversely, the name that I chose for this value — “filename” — already tells a programmer much more than the knowledge that it might be a string. We all know what a “filename” is. (Hickey talks about this too in that video.)

                                                                                                                  And in fact, depending on the version of Python this value can be of many different types: an array of bytes, an array of 16- or 32 bit unicode codepoints, and in later Pythons — an instance of pathlib.Path. And this particular function doesn’t care in the slightest, it works without changes. This is why I don’t like the excitement in the Python community about type annotations: as soon as this value with is annotated with any concrete type it’s coupled with irrelevant details and becomes a maintenance burden.

                                                                                                                  In a typed language we could invent an interface/trait/protocol for such a value. But then we will have to invent and maintain very granular definitions of such contracts for every possible use case, whereas in a dynamic language the value contract is defined by the way the value is actually used.

                                                                                                                  1. 4

                                                                                                                    too little in a sense that a type does not convey semantics (okay, it’s a string, but what it represents?)

                                                                                                                    It’s pretty common in languages with good type systems that using strings for things that are more semantically rich falls away. I generally have some abstract type that can be converted to and from a string but in the business layer it remains this abstract type. So a social security number would not be a String but SSN type where its underlying representation is hidden.

                                                                                                                    How would you communicate to users of the function what filename can be, though? Somewhere, someone has to state what the things open can validly take, right? This informalism seems convenient for you, you’re just writing a function that passes its input to another function and, hey, if they give you something that open doesn’t take, that’s not your problem, amirite? But what if you need to do any bit of manipulation of filename before opening it? For example, the _safe part means that it won’t read from /etc/ so you need to check if it starts with that. Isn’t the flexibility a hindrance now? This code suddenly balloons because it has to handle all these possible representations of a filename.

                                                                                                                    Conversely, the name that I chose for this value — “filename” — already tells a programmer much more than the knowledge that it might be a string.

                                                                                                                    But what if we made an abstract type called Path and the only way to construct a Path was in such a way that obeyed the operating system’s definition of what a path is?

                                                                                                                    Maybe I’m getting side tracked though, I was trying to understand how you think about things in terms of runtime values, but it still feels to me like you think in terms of types, you’re just letting something else deal with it. But maybe I just don’t get it.

                                                                                                                    1. 1

                                                                                                                      How would you communicate to users of the function what filename can be, though?

                                                                                                                      A docstring! I actually often call Python a docstring-typed language :-) The good part of this is that it’s not formal, so you can convey meaning in whatever way you feel best. This is, of course, the worst part as well because you can mislead or completely ignore the fact that your users need to know what the hell f or items mean in your argument list. So, to be clear, I’m not saying there’s an iron-clad solution to bad APIs, I’m saying that adequate means are available.

                                                                                                                      Also, given the introspective nature of dynamic languages it’s usually fairly easy to drop down a level and just read the source code and see how those parameters are used. For example in the ipython shell it just requires adding a second ? to an object (func? would show the docstring, func?? — the source).

                                                                                                                      if they give you something that open doesn’t take, that’s not your problem, amirite?

                                                                                                                      Yes. I’m not sure how problematic you see it, though. It surely happens from time to time, but a single traceback is usually enough to see at which level of the stack something expected a different value.

                                                                                                                      But what if we made an abstract type called Path and the only way to construct a Path was in such a way that obeyed the operating system’s definition of what a path is?

                                                                                                                      That would’ve been awesome! But we didn’t. You can’t anticipate all the usage patterns and invent ideal data types for everything from the get go.

                                                                                                                      That’s a little beside the point though (unless I misunderstand something). Assumption change, and code has to be refactored.

                                                                                                                      I was trying to understand how you think about things in terms of runtime values, but it still feels to me like you think in terms of types, you’re just letting something else deal with it.

                                                                                                                      The difference is that instead of specifying a concrete type as part of the function contract I’m specifying this contract in a different way that allows a user choose whatever type they happen to have around. And yes, they’re responsible for seeing if it actually works.

                                                                                                                      The main idea of this dichotomy is not that “values don’t have types”. Of course they do. It’s just that a notion of type may not be the best (and certainly not the only) way to establish an API contract. It disallows using other un-anticipated types, and it doesn’t convey the particulars of using a value in this particular function (even if I say “this is a Path”, it fails to say that it should be openable).

                                                                                                                      Let’s push this a little further… Values have many properties by which they can be grouped with other values. Size, memory layout, origin, security context, mutability, lifetime — you name it. A “type” is usually a combination of a few of those, but ultimately it doesn’t tell you everything about the value. Only the value itself can tell you everything about itself. “Thinking in values” as opposed to “thinking in types” is the proposition to accept this fact. And yes, the flexibility of being more expressive does have downsides. Like not being able to rely on fixed memory layout to compile into an efficient machine code.

                                                                                                                      1. 2

                                                                                                                        It disallows using other un-anticipated types, and it doesn’t convey the particulars of using a value in this particular function (even if I say “this is a Path”, it fails to say that it should be openable).

                                                                                                                        I’m not really grokking this “un-anticipated types” part of your argument, though. At some point, someone has to implement how to handle string, Path and all the encodings. In the case of your example, that is whoever implemented open. So there are no un-anticipated types, we can’t pass an int in there and expect open to magically figure out what to do with it.

                                                                                                                        And so, if someone needed to figure out what the type was at some point, then that means that, at the very least, we could infer the type of filename based on its usage in open. So I’m not really understanding what is being saved or won in the example you’re using.

                                                                                                                        1. 1

                                                                                                                          In this example, what’s being saved is the need to update type annotations on arguments of read_safe that sits in the middle. While the user upstream and open downstream care about it, read_safe doesn’t have to. In a typed language, it does.

                                                                                                                          It’s not the only advantage though… Consider a different example:

                                                                                                                          def process_json(f):
                                                                                                                              data = json.load(f)
                                                                                                                              return process(data)
                                                                                                                          

                                                                                                                          Here, the only contract on f is that it should have the .read() method returning some json. It can be of any type having many more methods. And even json.load doesn’t have to care about everything else those concrete types can do, it only cares about the subset.

                                                                                                                          This is exactly what interfaces/traits/protocols are about with added flexibility of not having to define a new one for every particular use case.

                                                                                                                          So, there’s really nothing more to it than saying “don’t tell what type it is, tell me what it should do”.

                                                                                                                          1. 2

                                                                                                                            In this example, what’s being saved is the need to update type annotations on arguments of read_safe that sits in the middle.

                                                                                                                            But either the type inference engine can figure that out on its own, or in the case of read_safe, I could just say that filename has the same type as the input to open, that way if open changes, read_safe gets it for free.

                                                                                                                            Here, the only contract on f is that it should have the .read() method returning some json

                                                                                                                            Don’t you mean .read() method returning a string?

                                                                                                                            So, there’s really nothing more to it than saying “don’t tell what type it is, tell me what it should do”.

                                                                                                                            This is exactly what structural typing will do, which is what Ocaml’s object system is based on. It can infer the type of input based on what methods you call or you can specify the type based on what things it can do.

                                                                                                                            1. 1

                                                                                                                              Yeah, language that require type annotations can be a pain. Whole-program inference is a must-have feature, IMHO.

                                                                                                                  2. 17

                                                                                                                    No, not for everyone. I find thinking in types way more constraining than thinking in values at runtime. Apparently, there are many people like me.

                                                                                                                    That’s familiarity, not a difference in how your brain works.

                                                                                                                    No, it’s not huge. There’s no conclusive study showing that type checking improves quality. It usually boils down, again, to personal preference of particular people doing the coding.

                                                                                                                    We don’t have sound experimental protocols for this. Reading tea leaves on GitHub is not science.

                                                                                                                    I’m not against type checking in general (heck, Rust is one of my favorite languages, as is Python). But the outright arrogance of quite a few people considering type checking to be a clearly superior paradigm, here on Lobste.rs and elsewhere, starts getting on my nerves, sorry.

                                                                                                                    I don’t care what you believe or use. If nobody lies about the tools or practices then I won’t have to rebut anything.

                                                                                                                    That sounds like confirmation bias and doesn’t advance the discussion. Look at how every pro-dynamic typing article is upvoted (this one and one of Bob Martin’s recently) and gets shredded in the comments, with gusto.

                                                                                                                    Bob Martin’s post was even more ignorant than this talk, it deserved to get shredded if only for making preferential users of dynamic typing look dumb.

                                                                                                                    Reiterating what I said in my first post, I don’t reaaaallyyyyy want to debate this because people tend to get upset and I don’t think arguing with programmers is a good use of my time or this space. You’re going to believe what you believe until you get shocked out of it. That’s just how this thing tends to go, nobody’s actually open-minded in these threads. So why not spare ourselves the grief and get back to work?

                                                                                                                    1. 5

                                                                                                                      It’s got nothing to do with familiarity. Types force you to express yourself in a way that can be verified statically by the type checker. A set of provable statements is necessarily a subset of all valid statements. Static typing restricts how you can express yourself, and that’s the biggest drawback of this approach.

                                                                                                                      At the end of the day, a human has to be able to read the code and understand its intent. Anything that distracts from that is a net negative in my experience. For example, you could write a 300 line sort in Idris https://github.com/davidfstr/idris-insertion-sort/blob/master/InsertionSort.idr that verifies all kinds of things statically. Understanding that it’s semantically correct is much harder than it would be for a 5 line version without types.

                                                                                                                      1. 12

                                                                                                                        A set of provable statements is necessarily a subset of all valid statements.

                                                                                                                        You don’t typically run into incompleteness when you’re only using lightweight types like with run-of-the-mill Haskell. If your program is ill-typed in Haskell, the overwhelmingly likely scenario is that your program is just wrong or unsafe, not that it’s correct but can’t be typed.

                                                                                                                        1. 3

                                                                                                                          That depends what you’re doing and what you consider “Hakell”. It’s not too hard to run into a need for RankNTypes in some cases (though you can usually write the code in a different way to avoid that need).

                                                                                                                          1. 0

                                                                                                                            Sure, but at that point you’ve already accepted that there is value in avoiding formalism. At that point it’s just a matter of degrees of comfort. My view is that code should be written for human readability first and foremost, because only a human reader can decide whether it’s semantically correct or not.

                                                                                                                            1. 10

                                                                                                                              There’s a minimum amount of formalism, but there isn’t a maximum amount of formalism. It’s necessarily a matter of degree. The argument is that most people pick way too low.

                                                                                                                              I find Haskell code more readable than the vast majority of languages, at a given level of program complexity. You seem to be assuming that Haskell is hard to read, which I don’t think is a reasonable assumption at all.

                                                                                                                              1. 1

                                                                                                                                I find a lot of people also conflate typing with type signatures. What makes Haskell great is you can get many of the type system benefits without ever writing a type signature at all!

                                                                                                                              2. 8

                                                                                                                                Sure, but at that point you’ve already accepted that there is value in avoiding formalism.

                                                                                                                                There is value in not being tied to a specific formalism. But there is little value in avoiding all formalisms altogether, unless you count the possibility of being wrong as “value”.

                                                                                                                                only a human reader can decide whether it’s semantically correct or not.

                                                                                                                                Only if the human reader can reliably prove things about programs.

                                                                                                                                1. 2

                                                                                                                                  This is something that static typing proponents have to demonstrate empirically. So far there’s no compelling evidence to suggest that projects are delivered faster with statically typed languages, have less defects, or improved ease of maintenance. Considering how long both type disciplines have been around, that’s quite the elephant in the room. I’ve heard the sentiment that it’s just too hard to test for this, but that just rings hollow to me. If something is clearly more effective that would be possible to demonstrate.

                                                                                                                                  It’s a false dichotomy to claim that you either use static typing or nothing at all. The reality is the formalism of using the type system is only one approach, and other approaches appear to be equally as effective in practice. You have testing, static analsysis tools like Erlang dialyzer http://erlang.org/doc/man/dialyzer.html runtime specification tools like Clojure Spec https://clojure.org/about/spec

                                                                                                                                    1. 2

                                                                                                                                      This is something that static typing proponents have to demonstrate empirically.

                                                                                                                                      No—You have to be more careful about how you’ve selected the “burden of proof”.

                                                                                                                                      You’ve placed it on requiring proof that static types provide X benefit.

                                                                                                                                      One can just as well turn this around and require poof that eschewing static types provide X benefit.

                                                                                                                                      We cannot a-priori place such demands in either direction.

                                                                                                                                      Finally, Requiring statistically significant studies pretty much guarantees no provable claims can be made for any side; since that amounts to a social science laden with shaky assumptions and ambiguous modeling. ‘reading the tea leaves on github is not science’

                                                                                                                                      (~crossposted from hn thread)

                                                                                                                                      1. 2

                                                                                                                                        Requiring statistically significant studies pretty much guarantees no provable claims can be made for any side; since that amounts to a social science laden with shaky assumptions and ambiguous modeling.

                                                                                                                                        It’s not a guarantee. We have the techniques and skill required to do a rigorous study, it’s just that such a study is really expensive and nobody wants to invest the money. “It’s hard” is not a reason to give up on something.

                                                                                                                                        1. 3

                                                                                                                                          Very well; I eagerly await the studies then.

                                                                                                                                          In the meantime, then, be skeptical about claims that attempt to discredit practices such as static typing due to an undue burden of proof requirement.

                                                                                                                                          1. 2

                                                                                                                                            Sure. But also be skeptical about claims that types reduce bugs. Everybody’s arguing from anecdata and everybody’s both biased and fallible.

                                                                                                                                        2. 1

                                                                                                                                          You’ve placed it on requiring proof that static types provide X benefit.

                                                                                                                                          That’s actually a correct burden of proof. We usually put it on the person claiming something brings benefits or should be a standard practice. So, if static typing has benefits, it’s up to us who believe that to demonstrate that using logical arguments and/or evidence in the field. There’s people in the discussion doing that. So, we don’t have to worry about burden of proof since we’re doing our part. ;)

                                                                                                                                          1. 1

                                                                                                                                            Claiming the same point more strongly doesn’t provide new information or absolve you from the contradiction I’ve identified

                                                                                                                                            1. 3

                                                                                                                                              Yogthos correctly noted that the burden of proof is on anyone challenging the status quo. The status quo is that there’s no consensus in this forum or in programming community at large whether static typing improves software over dynamic with their style of quality assurance. Yogthos wanted anyone pushing static types as the new, status quo that we should all adopt for the claimed benefits to provide evidence of those benefits. This is the standard method of discussion. When you countered that, I reminded you of that and that’s all my comment was about.

                                                                                                                                              Now you’re talking about a contradiction I have to absolve. Whatever it is will be a separate point to discuss. Burden of proof remains on anyone advocating adoption of a method with claimed benefits. They prove it. Then people should check it. Otherwise, we’d have to accept an Internet’s worth of false claims wasting time proving each one wrong. That would be a waste of time. Hence, the established direction for burden of proof.

                                                                                                                                        3. 2

                                                                                                                                          This is something that static typing proponents have to demonstrate empirically. So far there’s no compelling evidence to suggest that projects are delivered faster with statically typed languages, have less defects, or improved ease of maintenance.

                                                                                                                                          As I said elsewhere in the discussion, I’m not advocating static type systems in this discussion. Formalisms other than types do exist! However, if you want your programs to be free of defects, you have to prove them correct. Types sometimes make a very small contribution towards that goal. Tests don’t help one iota.

                                                                                                                                          1. 0

                                                                                                                                            I disagree with that. If you want your programs to be correct, you have to ensure they work as specified for the use cases you have. You can try to do that using static types, or you can use test,s or a runtime contract. All these approaches are effective in practice.

                                                                                                                                            1. 2

                                                                                                                                              If you want your programs to be correct, you have to ensure they work as specified for the use cases you have.

                                                                                                                                              No disagreement here. However, the claim that a program works as specified requires proof.

                                                                                                                                              You can try to do that using static types, or you can use tests or a runtime contract.

                                                                                                                                              Most type systems only allow you to prove very trivial things about your programs. Tests are only a feasible strategy if the space of legitimate inputs is small enough to be exhaustively searched. “Runtime contracts” are a misnomer, but assuming you meant “runtime contract checks”, well, those don’t prove your program correct.

                                                                                                                                              1. 1

                                                                                                                                                Proof is a formal term and typically implies correctness for all possible cases. A program has to only demonstrate correctness for possible inputs.

                                                                                                                                                Ultimately, your program has to have some sort of specification. My experience is that these specifications will not be formal in practice. You have to code your program to whatever requirements you have as best understood.

                                                                                                                                                A runtime contract like Clojure Spec https://clojure.org/about/spec will allow you to encode a specification and do generative testing against it. This is a sufficient level of proof that the software works as expected for vast majority of situations.

                                                                                                                                                1. 3

                                                                                                                                                  Proof is a formal term and typically implies correctness for all possible cases. A program has to only demonstrate correctness for possible inputs.

                                                                                                                                                  What distinction are you making between “all possible cases” and “all possible inputs”?

                                                                                                                                                  Ultimately, your program has to have some sort of specification. My experience is that these specifications will not be formal in practice. You have to code your program to whatever requirements you have as best understood.

                                                                                                                                                  Of course, you can’t expect a business analyst or what-have-you to hand you a formal specification. You have to generate it yourself from the information you have been given.

                                                                                                                                                  A runtime contract like Clojure Spec https://clojure.org/about/spec will allow you to encode a specification

                                                                                                                                                  This would actually be a formal specification, assuming you have a formal semantics for Clojure! The proof that your program meets the specification is still missing, though.

                                                                                                                                                  and do generative testing against it.

                                                                                                                                                  Generative testing is a little bit smarter than unit testing, but it’s no replacement for a proof.

                                                                                                                                                  1. 2

                                                                                                                                                    Generative testing is a little bit smarter than unit testing, but it’s no replacement for a proof.

                                                                                                                                                    It’s worth noting that the first property-based testing library was QuickCheck for Haskell, so proof is no replacement for generative testing, either :P

                                                                                                                                                    1. 1

                                                                                                                                                      It’s worth noting that the first property-based testing library was QuickCheck for Haskell, so proof is no replacement for generative testing, either.

                                                                                                                                                      Let’s set aside for a while the matter of whether your conclusion is true or false. I fail to see how exactly your premise entails your conclusion. Are you implicitly assuming that Haskell’s type system can verify every property you could possibly care about, and even then it still wasn’t enough?

                                                                                                                                                      1. 2

                                                                                                                                                        I’m saying that enough Haskell people felt that their particular type system wasn’t enough such that they created (an incredibly innovative!) testing library. Defense in depth, yo.

                                                                                                                                                        1. 1

                                                                                                                                                          Almost every other comment I said in this thread explicitly says (paraphrased) “types do little for you” and “you have to prove yourself that your programs are correct”.

                                                                                                                                                          1. 3

                                                                                                                                                            I think there’s a miscommunication happening here. I love formal methods to the point I spent months writing a manual on TLA+. I just don’t think it’s enough. It’s not enough to prove your program is correct: you have to obsessively test it too.

                                                                                                                                                            1. 4

                                                                                                                                                              I think your original statement felt a bit out of place since I don’t know any Haskeller that thinks their type system is powerful enough to generate a proof of the correctness of the program.

                                                                                                                                                    2. 1

                                                                                                                                                      Let’s say I have inputs a and b, and a result c. If I know my input range is from 0-100, I can test that a^n + b^n = c^n for all possible inputs. However, it’s much more difficult to prove this to be the case for any input in general.

                                                                                                                                                      This would actually be a formal specification, assuming you have a formal semantics for Clojure! The proof that your program meets the specification is still missing, though.

                                                                                                                                                      I would argue that it’s not required. If I have a specification, I can do generative testing to exercise the code, and I can validate that the data coming into the system is within the accepted range.

                                                                                                                                                      My argument is that the effort required to provide an exhaustive proof is not justified in vast majority of situations. The business requirement is typically to produce software that works well enough that the users are happy. A proof is not a business requirement.

                                                                                                                                            2. 2

                                                                                                                                              This is something that static typing proponents have to demonstrate empirically.

                                                                                                                                              What is? I don’t see that @pyon made any contentious claims in that comment.

                                                                                                                                              1. 0

                                                                                                                                                The claim that static typing is the most effective formalism. This is a false dichotomy:

                                                                                                                                                There is value in not being tied to a specific formalism. But there is little value in avoiding all formalisms altogether, unless you count the possibility of being wrong as “value”.

                                                                                                                                                1. 1

                                                                                                                                                  What I actually claimed is that types help very little. How exactly does that agree with “types are the most effective formalism”?

                                                                                                                                                  1. 1

                                                                                                                                                    Appears I misread your comment. That said, I do think there is value in possibility of being wrong, if that means you can express yourself in a less constrained fashion. Ultimately, your formal specification can be wrong as well, so it’s really a question of where you’re going to be looking for errors.

                                                                                                                                                    1. 2

                                                                                                                                                      Appears I misread your comment.

                                                                                                                                                      I didn’t even bring types into the discussion until you did.

                                                                                                                                                      That said, I do think there is value in possibility of being wrong, if that means you can express yourself in a less constrained fashion.

                                                                                                                                                      The only freedom that you get is the freedom to say nonsense. That’s not terribly useful.

                                                                                                                                                      Ultimately, your formal specification can be wrong as well

                                                                                                                                                      So you test it, more or less the same way scientists test scientific theories:

                                                                                                                                                      • Make predictions (i.e., logical inferences from the specification) about what the user meant in distinct cases.
                                                                                                                                                      • Ask the user if these predictions agree with what they expected.
                                                                                                                                                      1. 1

                                                                                                                                                        The only freedom that you get is the freedom to say nonsense. That’s not terribly useful.

                                                                                                                                                        That’s absurd. You can state many things without being able to prove them. As long as you can demonstrate that the statement works within the context you’re using it, you get value out of it.

                                                                                                                                                        So you test it, more or less the same way scientists test scientific theories:

                                                                                                                                                        Which is exactly what you’d do with tests or runtime specifications.

                                                                                                                                                        Ultimately, we’re discussing cost benefit here. My claim is that you can deliver working software faster without using formal proofs. That’s what the business cares about at the end of the day. A company that delivers a working product that people use will outcompete the company working on a perfect product.

                                                                                                                                                        1. 1

                                                                                                                                                          As long as you can demonstrate that the statement holds (FTFY) within the context you’re using it, you get value out of it.

                                                                                                                                                          You’re just adding one more premise (the “context” you talk about) to the implication you have to prove.

                                                                                                                                                          1. 1

                                                                                                                                                            While we don’t have a proof, we certainly have a lot of evidence accumulated over the years. If formal proofs were indeed a requirement for developing usable software, then we’d all be using them by now. It’s really that simple.

                                                                                                                                                            Businesses using languages like Haskell and OCaml would outcompete those using Python, Ruby, or JavaScript. This is not what we see happening in practice though. Despite these languages having been around for many decades, they remain niche.

                                                                                                                                                            Now, it’s perfectly possible that once somebody is trained up sufficiently they could be just as productive. However, that seems to be a challenge as well.

                                                                                                                                                            At the end of the day we need languages that can be learned relatively easily by an average developer to become productive with. The more formal the language the less accessible it becomes. So economics aren’t in favor of formal methods I’m afraid.

                                                                                                                                                            1. 2

                                                                                                                                                              If formal proofs were indeed a requirement for developing usable software, then we’d all be using them by now.

                                                                                                                                                              Sure, one can trivially argue they are not a requirement but we lack any reasonable amount of scientific study on if they help. I think they probably do (more understanding of / reasoning about code seems likely to help quality) but what I think is hardly science ;)

                                                                                                                                                              1. 1

                                                                                                                                                                Businesses using languages like Haskell and OCaml would outcompete those using Python, Ruby, or JavaScript.

                                                                                                                                                                I don’t see how you arrive to that conclusion. Neither Haskell nor OCaml is in short supply of features that make formal verification harder than necessary.

                                                                                                                                                                At the end of the day we need languages that can be learned relatively easily by an average developer to become productive with.

                                                                                                                                                                Maybe the notion of “average developer” is the problem in the first place?

                                                                                                                                                                1. 1

                                                                                                                                                                  You still haven’t explained what sort of formal verification you advocate, or given an example of a language using it. Haskell and OCaml are the most popular formal languages I’m aware of. Are you talking about languages like Coq here?

                                                                                                                                                                  From a business perspective, you need a tool that can be learned in a reasonable amount of time by a person you’re going to be able to hire from the pool of people available. That’s where your average developer comes from. Technology that can be used by a wider pool of people effectively will always dominate.

                                                                                                                                                                  1. 1

                                                                                                                                                                    Are you talking about languages like Coq here?

                                                                                                                                                                    No. Plain paper and pen proofs.

                                                                                                                                        4. 11

                                                                                                                                          For example, you could write a 300 line sort in Idris https://github.com/davidfstr/idris-insertion-sort/blob/master/InsertionSort.idr that verifies all kinds of things statically. Understanding that it’s semantically correct is much harder than it would be for a 5 line version without types.

                                                                                                                                          https://research.googleblog.com/2006/06/extra-extra-read-all-about-it-nearly.html

                                                                                                                                          1. 3

                                                                                                                                            Sure, and these are exactly the types of bugs you will see in the real world in dynamically typed languages. I’ll let you decide if that bug was a show stopper or not for production use. Also from the link:

                                                                                                                                            And now we know the binary search is bug-free, right? Well, we strongly suspect so, but we don’t know. It is not sufficient merely to prove a program correct; you have to test it too.

                                                                                                                                            1. 2

                                                                                                                                              But would the Idris proof actually have caught the bug? It’s an overflow error, while Haskells have infinite-precision numbers. Seems like sidestepping the problem to me.

                                                                                                                                              1. 7

                                                                                                                                                The actual error is conflating (physical or virtual) machine integers with the integers. It is totally fine to use machine integers for performance reasons, but it is not okay to pretend that results that were proven for the integers must also hold for machine integers.

                                                                                                                                            2. 7

                                                                                                                                              The Idris example is interesting but doesn’t say too much. There is lots of complicated ways things can be solved with or without types. I don’t know if the link you pasted is considered a good solution or not.

                                                                                                                                              That being said, one thing that the Idris solution will give you but a dynamically typed solution won’t without extensive tests is if I modify the code in such a way that it violates the invariants, the compiler will complain. This is a major benefit of a good type system, IME.

                                                                                                                                              1. 3

                                                                                                                                                However, you have to know that the invariants themselves are correct. A type specification is effectively a program that the type checker uses to analyze your original program. If a specification is as complex as the Idris example, it becomes difficult to tell whether it’s correct in any meaningful sense. So, now you just pushed the problem back, you just have a metaprogram that you have to reason about.

                                                                                                                                                1. 8

                                                                                                                                                  The thing you are missing:

                                                                                                                                                  In typed languages you often have to be wrong twice to introduce a bug: You have to get both the code and the types wrong. Getting only one of them wrong will be flagged and rejected by the compiler.

                                                                                                                                                  In untyped languages you usually have to be right twice to avoid a bug: Yo have to get both the code and the tests right. Getting only one of them wrong is no reliable guarantee that your bug will be found before deployment.

                                                                                                                                                  1. 2

                                                                                                                                                    In typed languages you often have to be wrong twice to introduce a bug

                                                                                                                                                    Yes, and moreover, both wrong in a compatible way!

                                                                                                                                                    1. 1

                                                                                                                                                      I’m not missing that at all. My point is that the formalism often requires you to express yourself in a specific way that can be verify. So, while you know something is self-consistent, you don’t know that it’s correct in a semantic sense.

                                                                                                                                                      Dynamic languages let you write much more direct code that’s easier for a human to read. Meanwhile, you can also provide specifications in a dynamic language. Take a look at Racket Contracts or Clojure Spec as examples https://clojure.org/about/spec In fact, I’d argue this provides a more rich specification than types as it focuses on semantic correctness.

                                                                                                                                                      1. 8

                                                                                                                                                        Dynamic languages let you write much more direct code that’s easier for a human to read.

                                                                                                                                                        No more than any other paradigm, though, right? I don’t find Ocaml code any less readable than Python code. In most cases, the types aren’t even explicitly written in Ocaml so there is line noise or anything getting in the way.

                                                                                                                                                        I’ve actually been writing code in Python a bunch lately after spending a lot of time in Ocaml and I’ve noticed that I end up having to look at documentation fairly frequently, whereas in Ocaml I would generally just look at the type of a value instead. But the documentation is really hit or miss, so I’ve even found myself looking at the code for dependencies several times, I’ve only done that a few times in Ocaml.

                                                                                                                                                        YMMV, but your blanket claim that dynamic languages let one write code easier to read than statically typed languages doesn’t match my experience.

                                                                                                                                                        On top of that, ease of reading isn’t the metric I personally go by. It’s ease of refactoring. I’ve found that dynamic languages take a lot of effort to make refactoring safe, but in a language like Ocaml I have the compiler watching over my shoulder.

                                                                                                                                                        1. 1

                                                                                                                                                          We clearly have very different experience here. I do find that Clojure code ends up being more direct than any static language I’ve used. I also find that it allows me to trivially express patterns that are challenging to encode using type systems. For example, something like Ring middleware https://github.com/ring-clojure/ring/wiki/Middleware-Patterns is difficult to do in a static context.

                                                                                                                                                          I do find readability is incredibly important when refactoring. I need to know what the code is doing and why to refactor it effectively.

                                                                                                                                                          1. 3

                                                                                                                                                            You can accomplish that pattern in a statically typed language. Ocaml has a few implementations of that, one is hmap: http://erratique.ch/software/hmap

                                                                                                                                                            The only thing that isn’t exactly what I think you want is your key encodes the type of the value so you have to know the type you want to get out of a particular key.

                                                                                                                                                            I do find readability is incredibly important when refactoring. I need to know what the code is doing and why to refactor it effectively.

                                                                                                                                                            But how does that square with your response to @pyon in another subthread:

                                                                                                                                                            With a dynamic language it’s sufficient to show that the program behaves as expected for the specific use cases that you have

                                                                                                                                                            How do you express how the program should behave for the cases you have? Is it tests? What happens if your break the code for a valid case but that you didn’t write a test for? The problem I find when refactoring code in a dynamically typed language generally revolves around how hard it is to know what the code should do and if I change the code in a certain way (for example, make something that was an integer now a string), have I broken something users of the codebase depend on. That sort of refactoring is trivial in a statically typed language, just make the change and let the compiler tell you every other place that needs to change. IME, those changes are very difficult in a dynamically typed language.

                                                                                                                                                        2. 4

                                                                                                                                                          I’m not missing that at all. My point is that the formalism often requires you to express yourself in a specific way that can be verify.

                                                                                                                                                          That’s a bit like arguing that seat belts are bad, because they make it hard to drive while standing upright in your seat. Doh!

                                                                                                                                                          The point is that there are hundred of thousands of people still walking on this planet that wouldn’t be around without seat belts.

                                                                                                                                                          Dynamic languages let you write much more direct code that’s easier for a human to read.

                                                                                                                                                          Let’s just disagree on that.

                                                                                                                                                          Take a look at Racket Contracts or Clojure Spec as examples https://clojure.org/about/spec.

                                                                                                                                                          The whole problem with these things is that they are optional. You can decide to use them in your own code, but if libraries are not using them you are in an uphill battle.

                                                                                                                                                          We have seen this problem times and times again with newer languages trying to graft on nullability information on existing libraries and spectacularly failing, despite the much smaller scope of the issue.

                                                                                                                                                          The main benefit of types is that they force everyone to follow their rules.

                                                                                                                                                          I can look at a random library’s type signatures and immediately know which things cannot happen.

                                                                                                                                                          1. 3

                                                                                                                                                            If you use Design-by-Contract, you can do both. The Design-by-Contract preconditions, invariants, and postconditions are similar to static types where you’re bolting them on rather than being integrated in the language. Some languages, esp Eiffel and Ada/SPARK, integrate them. I doubt Python etc support it so you’d be using some language feature, maybe just the OOP stuff, to do it. The precondition checks especially would guarantee certain things about your program before you even run it with people using your library knowing more about it just looking at them. Invariant or postcondition checks can be combined with property-based or purely-random testing to catch a lot of errors in a way that highlights exactly what failed.

                                                                                                                                                            Now, people can get these properties wrong. However, the literature of academic and industrial deployments strongly argue that they’ll catch vastly more implementation errors in development and maintenance phases than review or testing alone.

                                                                                                                                                        3. 7

                                                                                                                                                          However, you have to know that the invariants themselves are correct.

                                                                                                                                                          And in a dynamic language we don’t even know what any of the invariants are, so I don’t see this response as damning of types. In Ocaml, the sort function for lists has the type: cmp:('a -> 'a -> int) -> 'a list -> 'a list which is pretty lightweight, it’s not nearly as formal as the Idris one but it still tells me important things, like that the sort implementation cannot know anything about the contained type.

                                                                                                                                                          Essentially it feels like you’re saying there exists no invariants worth checking at compile time. Is this an accurate summary of your stance?

                                                                                                                                                          1. 5

                                                                                                                                                            However, you have to know that the invariants themselves are correct.

                                                                                                                                                            So long as an understandable logic, the experience of several decades in formal specification show people find errors in requirements, design, or implementation using them. Every case study has errors caught this way with most in industry who were just using their heads and tests before reporting a drop in defects after introducing formal specs. The specs themselves are about the what more than the how which focuses the mind for review or tooling for checks. The how is usually more complex with Idris especially being a heavyweight way to do things not representative of effort/reward ratio of typical usage of either static typing or formal specs.

                                                                                                                                                            Now, some of these specs can get pretty big. This varies from being limitations of the spec language to intrinsic complexity of the problem. The former is something they might also screw up on. The compiler might catch some but not all of those screwups. The latter represent the complex details the programmer must get right that are implicit in non-typed or non-specified programs. As in, such complexity is always there but just invisible to compilers, checkers, and maybe the programmer depending on skill. Then, making it explicit, it can be checked by any of those. The more you want to explicitly check, the more types/specs come with the given module. Again, there’s a spectrum of effort put in vs rewards gotten out that one can use depending on importance of module and their resource constraints.

                                                                                                                                                            1. 1

                                                                                                                                                              Agree completely.

                                                                                                                                                        4. 5

                                                                                                                                                          In real life, programmers do not deliberately write unreadable code in either static or dynamic type systems, because that would be pointless. It is also possible to write dynamically-typed code that is unreadably dynamic if you aren’t immersed in the local idioms (I can point to a lot of mainstream Ruby examples!). So I’m not sure what point you’re trying to make. [edited due to premature post!]

                                                                                                                                                          1. 0

                                                                                                                                                            I completely agree that you can make a mess in any language. However, my point was that static typing necessarily restricts the number ways you can write code to those that are statically provable. A dynamic language allows you to write a statement that is not accompanied by an exhaustive proof, and proving something is often much more difficult than stating it.

                                                                                                                                                            For example, Fermat’s Last Theorem states that no three positive integers a, b, and c satisfy the equation a^n + b^n = c^n for any integer value of n greater than 2. That’s a really simple statement to make, and to understand. Proving that to be correct is a lot more difficult. Even when such a proof has been found, only a handful of people in the world can judge whether its correct or not.

                                                                                                                                                            1. 14

                                                                                                                                                              A dynamic language allows you to write a statement that is not accompanied by an exhaustive proof,

                                                                                                                                                              Yes, but that is overly categorical.

                                                                                                                                                              Most typed languages also do not require exhaustive proofs, in the form of the Idris example you posted. You seem to want to create a false dichotomy, between no types on one had, and a total formally verified technique on the other (which are cumbersome).

                                                                                                                                                              Most proponents of static typing here aren’t advocating for full dependent-typed/verified languages (most of which are still experimental!) capable of solving Fermat’s Last Theorem in the compiler.

                                                                                                                                                              1. 1

                                                                                                                                                                Idris example is an extreme case, but pretty much any statically typed languages make it difficult to work with heterogeneous data. Types are also make it difficult to pass data across boundaries. This is the same problem you have with OO class hierarchies.

                                                                                                                                                                1. 4

                                                                                                                                                                  Is heterogeneous data something you find yourself commonly working with? Even in a language like Python it’s generally considered good practice that all entries in your containers have the same type unless there is some way to know before hand what they will be. But GADTs make that work in a statically typed language just fine.

                                                                                                                                                                  1. 2

                                                                                                                                                                    Yes absolutely. Most real world data tends to be heterogeneous in my experience. This is a perfect example https://github.com/ring-clojure/ring/wiki/Middleware-Patterns You can have middleware functions that update the request and response maps by adding keys relevant to that piece of middleware, or updating existing keys. This would be pretty much impossible to do using a static language, especially if you want to be able to write middleware libraries that aren’t aware of one another.

                                                                                                                                                                    1. 3

                                                                                                                                                                      Linking to my response about HMap here: https://lobste.rs/s/n6eix9/rich_hickey_delivers_rationale_for#c_keqhja

                                                                                                                                                                      tl;dr - it isn’t pretty much impossible.

                                                                                                                                                                      Most real world data tends to be heterogeneous in my experience.

                                                                                                                                                                      I guess you mean heterogeneous and not known a-priori? For heterogeneous data we have things like records which let you store different kinds of data in the same thing, but you know what it is before hand.

                                                                                                                                                              2. 3

                                                                                                                                                                If you have to bring up Fermat’s Last Theorem that suggests your argument is on shaky ground.

                                                                                                                                                                1. 1

                                                                                                                                                                  Please do elaborate.

                                                                                                                                                                  1. 3

                                                                                                                                                                    It’s a very hefty sledgehammer of an argument and it suggests that some subtledties may be escaping you.

                                                                                                                                                            2. 4

                                                                                                                                                              Static typing restricts how you can express yourself, and that’s the biggest drawback of this approach.

                                                                                                                                                              Do you have an example of a program that cannot be statically typed and still represents a program you would want to write?

                                                                                                                                                              1. 5

                                                                                                                                                                Clojure transducers https://clojure.org/reference/transducers are difficult to type for a general case since the result depends on the runtime type of the argument. These are a core mechanic in Clojure. Ring middleware https://github.com/ring-clojure/ring/wiki/Middleware-Patterns is another example of something that’s not really possible in a typed language.

                                                                                                                                                                1. 2

                                                                                                                                                                  Thanks! I don’t know enough about either to comment more.

                                                                                                                                                                  1. 1

                                                                                                                                                                    Ring middleware is another example of something that’s not really possible in a typed language.

                                                                                                                                                                    Unless I’m very much mistaken “ring middle way” is easily expressible in a typed language with polymorphic row types.

                                                                                                                                                                    1. 1

                                                                                                                                                                      Ring middleware functions can modify the map in any way. They can add keys, remove keys. or change types of existing keys. The functions are defined in separate libraries that aren’t aware of one another directly. I can add a dependency and chain the middleware libraries any way I see fit. How would you express this using row types?

                                                                                                                                                                      1. 1

                                                                                                                                                                        They can add keys, remove keys. or change types of existing keys. … How would you express this using row types?

                                                                                                                                                                        That’s exactly the functionality that polymorphic row types give you.

                                                                                                                                                                        Concretely, in some imaginary type system

                                                                                                                                                                        -- Consumes any row type
                                                                                                                                                                        addAKey :: { r } -> { newKey :: Foo, r }
                                                                                                                                                                        
                                                                                                                                                                        -- Consumes any row type with `oldKey` field
                                                                                                                                                                        removeAKey :: { oldKey :: Foo, r } -> r
                                                                                                                                                                        
                                                                                                                                                                        -- Consumes any row type with `key` field
                                                                                                                                                                        changeTypeOfAKey :: { key :: Foo, r } -> { key :: Bar, r }
                                                                                                                                                                        
                                                                                                                                                                        1. 1

                                                                                                                                                                          This is something you’d have to do on case by case basis though?

                                                                                                                                                                          1. 1

                                                                                                                                                                            I don’t understand what you mean.

                                                                                                                                                                            1. 1

                                                                                                                                                                              Linking to HMap comment, I think it does what the @Yogthos is referring to:

                                                                                                                                                                              https://lobste.rs/s/n6eix9/rich_hickey_delivers_rationale_for#c_keqhja

                                                                                                                                                                2. 2

                                                                                                                                                                  A set of provable statements is necessarily a subset of all valid statements.

                                                                                                                                                                  That runs counter to Gödel’s completeness theorem: a statement in a first-order theory is provable iff it’s true in all models. In programming language terms: a statement about a program is provable iff it holds in all conforming implementations of the language the program is written in.

                                                                                                                                                                  Now, you might only care about one language implementation (presumably the one you’re using), but some of us care about portability and freedom from irrelevant implementation details…

                                                                                                                                                                  1. 0

                                                                                                                                                                    This is actually a direct result of Godel’s incompleteness theorem. It’s also known as the halting problem in CS. For example, Scala compiler has a bug where it stack overflows trying to resolve types https://github.com/scala/bug/issues/9142

                                                                                                                                                                    You’re restricted to a set of statements that can be verified in a reasonable amount of time.

                                                                                                                                                                    1. 3

                                                                                                                                                                      Gödel’s first incompleteness theorem asserts every effectively axiomatized formal system sufficiently powerful to prove basic arithmetic facts contains statements that are neither provable nor disprovable. It says nothing about the “validity” of such statements, because GFIT is a theorem in proof theory, not model theory. In particular, by Gödel’s completness theorem, the Gödel statement, just like any other statement that is neither provable nor disprovable in a theory, is true in some models and false in others. Whether that is “valid” enough for you is up to you - I prefer to work with statements (programs) that are true (run correctly) in all models (conforming implementations) of a theory (programming language).

                                                                                                                                                                      Also note that I’m not advocating types (in this discussion). But you have to prove your programs correct, whether you use types or something else altogether. “Using types is an inefficient way to prove most things I have to prove” is a legitimate objection - one that I agree with, even! “I want to get away with not proving what I have to prove” is not.

                                                                                                                                                                      1. 1

                                                                                                                                                                        No, you don’t have to prove your programs correct. That’s the key difference. With a dynamic language it’s sufficient to show that the program behaves as expected for the specific use cases that you have. With a static language you have to write it in a way that the type checker is able to prove to be exhaustively correct.

                                                                                                                                                                        1. 4

                                                                                                                                                                          With a dynamic language it’s sufficient to show that the program behaves as expected for the specific use cases that you have.

                                                                                                                                                                          So you can exhaustively test the entire space of legitimate inputs? You must have a few dozens orders of magnitude more computing power available to you than I do.

                                                                                                                                                                          With a static language you have to write it in a way that the type checker is able to prove to be exhaustively correct.

                                                                                                                                                                          That’s not true. As a matter of fact, I don’t do that when I use statically typed languages. Types provide basic sanity checks (e.g., modules don’t peek into each other’s internal details), but the bulk of the program’s proof of correctness is written by me, using paper and pen.

                                                                                                                                                                          1. 0

                                                                                                                                                                            Of course I wouldn’t. I’d validate data at the edges using Spec https://clojure.org/guides/spec Types are not the only way to provide basic sanity checks.

                                                                                                                                                                            1. 5

                                                                                                                                                                              Judging from your replies, you seem to think I’m delusional about types, even though I have been very explicit about the limited extent to which types help me. I expected it to be patently clear from my previous statements that I’m not telling you to use types. You can, of course, use whatever you wish. What I’ve actually said is:

                                                                                                                                                                              • You have to prove your programs correct.
                                                                                                                                                                              • To prove your programs correct, you need to use some formal system.
                                                                                                                                                                              • Gödel’s incompleteness theorems isn’t an excuse for not proving your programs correct.
                                                                                                                                                                              • Types sometimes relieve you from a very tiny part of the effort of proving your program correct.
                                                                                                                                                                              • There exist formal systems other than types.

                                                                                                                                                                              Furthermore, I originally only intended to make the first two points.

                                                                                                                                                                              1. 0

                                                                                                                                                                                I disagree with the idea that you have to prove your programs correct in a general case. That can be desirable in some situations, but it’s simply not a business requirement.

                                                                                                                                                                                The result of Godel’s incompleteness theorems is that the type checker restricts the way you’re able to express yourself to a subset of expressions that can be proved in a reasonable amount of time by the type checker. My argument is that it can result in code that’s harder for a human to understand than code that can’t be machine verified.

                                                                                                                                                                                I think we agree on the value of types, but not on the value of formal proofs.

                                                                                                                                                                                1. 2

                                                                                                                                                                                  The result of Godel’s incompleteness theorems is that the type checker restricts the way you’re able to express yourself to a subset of expressions that can be proved in a reasonable amount of time by the type checker.

                                                                                                                                                                                  You keep bringing in type checkers. Didn’t you get the memo when I said “Formalisms other than types do exist!”?

                                                                                                                                                                                  My argument is that it can result in code that’s harder for a human to understand than code that can’t be machine verified.

                                                                                                                                                                                  My experience is exactly the opposite. Types don’t write much of your proof of correctness for you, but they make the parts you have to write yourself much easier to write.

                                                                                                                                                                                  1. 0

                                                                                                                                                                                    It certainly does sound like our experiences are very divergent here. You keep talking about other formalisms, but the point I make regarding the type checker apply to those just the same. Perhaps, you can elaborate on how you believe these other formalisms avoid the problem.

                                                                                                                                                                                    1. 5

                                                                                                                                                                                      Humans and computers have different strenghts:

                                                                                                                                                                                      • Computers are faster and more reliable than humans at performing long calculations, especially case analyses.

                                                                                                                                                                                      • Humans are better than computers at defining usable abstractions and jumping between them, which requires insight.

                                                                                                                                                                                      Formal systems come in varying degrees of human- and computer-friendliness. At the two extremes, we have:

                                                                                                                                                                                      • Cellular automata usually have simple and efficiently implementable definitions (computer-friendly). However, their evolution over time is very difficult to analyze and predict (human-hostile).

                                                                                                                                                                                      • Higher-order programming languages (i.e., whose variables can be instantiated with abstractions) allow complex hierarchical structures to be directly expressed in them (human-friendly), but the fundamental operation in their semantics, namely variable substitution, is difficult to implement both correctly and efficiently (computer-hostile).

                                                                                                                                                                                      Notably, the first-order predicate calculus lies at a sweet spot in the middle. It is simple enough to be used by humans directly, not just to define things, but also to perform actual computations (although this requires training). At the same time it is a powerful enough metalanguage for higher-order object languages (e.g., set theory).

                                                                                                                                                                                      In my view (others might not agree), the key to making verification more tractable is to intelligently split the verification effort into parts that are relatively easy for a human to perform (defining hierarchical structures and abstraction boundaries, finding loop invariants and variants) and parts that are relatively easy for a computer to perform (performing mechanical consistency checks, exhaustive searches and case analyses). Different parts might have to be performed using different formal systems, designed to exploit the strengths of whoever has to use it directly.

                                                                                                                                                                          2. 3

                                                                                                                                                                            With a static language you have to write it in a way that the type checker is able to prove to be exhaustively correct.

                                                                                                                                                                            Here’s a well-typed program

                                                                                                                                                                            add3 x y z = x + y + z
                                                                                                                                                                            

                                                                                                                                                                            In what way have I (or the type checker) “proven it to be exhaustively correct”?

                                                                                                                                                                            1. 1

                                                                                                                                                                              It’s not well typed if x, y, and z are int32s.

                                                                                                                                                                              1. 2

                                                                                                                                                                                It is well typed. The operation just happens to be addition in Z/kZ for k = 2^32, instead of the usual integer addition.

                                                                                                                                                                                1. 1

                                                                                                                                                                                  So it’s well-typed but potentially has a lot of behavioral bugs, because you can’t guarantee that x + y >= x.

                                                                                                                                                                                  1. 3

                                                                                                                                                                                    Z/kZ isn’t an ordered ring, hence you shouldn’t define an operation <= that works on int32 arguments.

                                                                                                                                                                              2. 0

                                                                                                                                                                                You’ve created some very basic constraints here such as x, y, and z having to support the + operation. This example is not very interesting for obvious reasons. :)

                                                                                                                                                                                1. 4

                                                                                                                                                                                  The rest of strongly typed programming is very much of this flavour and indeed rules out (merely?) “not very interesting” bugs.

                                                                                                                                                                3. 2

                                                                                                                                                                  Have some thoughts on this, but first of all:

                                                                                                                                                                  I don’t really want to get sucked into this debate … users of untyped languages feeling insecure/defensive about it.

                                                                                                                                                                  That’s very rude of you.

                                                                                                                                                                  Okay, on to the meat of this. I think everybody has the same misconception about dynamic typing, including a lot of people who use dynamic typing: dynamic typing and static typing are not exclusive. All static typing means is that types exist at compile time. All dynamic typing means is that types exist at runtime. Languages can be both statically typed and dynamically typed (C#). Languages can be neither (bash). Each one has benefits and drawbacks, and it happens that each one’s drawbacks cancel out the other’s benefits, which is why a lot of languages are only one or the other. But since most dynamic languages aren’t also static (because drawbacks), people conflate it with untyped and end up arguing “static vs untyped”. It doesn’t help that a lot of languages don’t really explore the power dynamic typing gives you, precisely because they choose it to avoid the overhead of static typing.

                                                                                                                                                                  Here are some dynamic language features that would be a lot to implement in non-dynamic languages:

                                                                                                                                                                  • J’s array manipulations have very different type signatures depending on the dimensions of your arguments and the specified rank of the verb. That allows it to do extremely fast manipulations in extremely concise syntax: see here for examples.
                                                                                                                                                                  • The two most popular data analysis languages, Python and R, both allow for interactive, partially executable REPLs. That makes them good for exploring data before committing to a transformation or full script.
                                                                                                                                                                  • Python also uses prototype inheritance, letting you adjust all instances of an object at runtime (for example, to add logging or caching).
                                                                                                                                                                  • Ruby has runtime metaprogramming, which is key for how the ActiveRecord ORM works.
                                                                                                                                                                  • I get the impression SQL would be a lot trickier to statically type but that’s just a hunch.

                                                                                                                                                                  Now, I’m not saying these are good or bad. In some contexts, these are good features to have. In other contexts, they’re less useful than static typechecking. But there is a tradeoff that happens and there’s never a free lunch.

                                                                                                                                                                  1. 3

                                                                                                                                                                    dynamic typing and static typing are not exclusive

                                                                                                                                                                    Right, and that’s true in Haskell too. The former should be preferentially minimized.

                                                                                                                                                                    All dynamic typing means is that types exist at runtime.

                                                                                                                                                                    Those aren’t types, they are tags, sometimes called class tags. Types have no representation.

                                                                                                                                                                    I get the impression SQL would be a lot trickier to statically type but that’s just a hunch.

                                                                                                                                                                    I maintain a type-safe SQL DSL library for Haskell and it has single-handedly improved my work more than learning or using Clojure ever did.

                                                                                                                                                                    Python also uses prototype inheritance, letting you adjust all instances of an object at runtime (for example, to add logging or caching).

                                                                                                                                                                    I have never ever needed this and anytime I’ve run into someone that did it’s because the tooling was failing them in other places. There are far more robust and maintainable ways to solve the same problems.

                                                                                                                                                                    I was primarily and preferentially a user of untyped programming languages until I finally got to grips with Haskell. I still use it despite being quite comfortable in and having used Python and Clojure in production because the advantages have been profound. I get you don’t share in that belief, IME, it’s usually unfamiliarity or discomfort. I didn’t like feeling stupid at first either. I tried and failed to learn Haskell many times, that’s partly why I started writing a book years ago. I gave a talk about having failed to learn Haskell over the course of several years too. I assure you it was worth it in the end.

                                                                                                                                                                    I see you getting stuck into your idiosyncratic definition of what a type system is with soc so let me cite Robert Harper. I think the point is elaborated in PFPL as well but I don’t remember it being very accessible.

                                                                                                                                                                    1. 3

                                                                                                                                                                      It seems to mostly be users of untyped languages feeling insecure/defensive about it.

                                                                                                                                                                      I get you don’t share in that belief … I didn’t like feeling stupid at first either.

                                                                                                                                                                      I see you getting stuck into your idiosyncratic definition of what a type system is

                                                                                                                                                                      Are you able to have a discussion with someone without making fun of them?

                                                                                                                                                                      If I said I was comfortable programming in languages with good static type systems, would you accept that it’s possible for someone to have different preferences without being objectively wrong, or are you going to say that my experience doesn’t count?

                                                                                                                                                                      1. 2

                                                                                                                                                                        You can do better than preference, but this isn’t the time or place for that conversation. Hit me up another time.

                                                                                                                                                                    2. 3

                                                                                                                                                                      Technically (I know, I know) every language has a static type system.

                                                                                                                                                                      In shell this system has only one type (string) and there is no need for a typechecker because and value can always be used anywhere a string can be used (since they are all strings). You have some arguments about shell functions (they’re not strings… but also aren’t values).

                                                                                                                                                                      Bash has a bit more in it. Every value in bash has the type of anonymous union across string, list, etc. There’s still only one type in the static type system, so again, no typechecker.

                                                                                                                                                                      In Ruby, there is still only one type, but now it has a name (RbValue) and it is a tagged union. (Again, reasonable people can have arguments about if it counts as a union since new tags can be introduced at runtime. Tagged union is the most obvious thing to call it, but you might want to call it Dynamic or some such, but this does not fundamentally change the description of the static type system).

                                                                                                                                                                      1. 2

                                                                                                                                                                        All dynamic typing means is that types exist at runtime.

                                                                                                                                                                        I’m not sure how this can be true:

                                                                                                                                                                        A type system is a tractable syntactic method for proving the absence of certain program behavior by classifying phrases according to the kinds of values they compute.

                                                                                                                                                                        With other words, types are used to reject programs according to the rules specified by the type system at compile-time.

                                                                                                                                                                        There might be artifacts of types encoded into the compiled program to facilitate the execution of that program, but these runtime tags are are values, not types.

                                                                                                                                                                        1. 1

                                                                                                                                                                          You’re defining a “type system” as “a static type system”. That’s like me defining a “programming language” as “compiled”, and then saying that Python is clearly not a programming language.

                                                                                                                                                                          1. 2

                                                                                                                                                                            There is no “dynamic” type system. A type system is a “static” type system is a type system.

                                                                                                                                                                            1. 2

                                                                                                                                                                              If you’re unwilling to even acknowledge that your preferred definition is not universal, I don’t see how we can have any meaningful discussion.

                                                                                                                                                                              1. 2

                                                                                                                                                                                The definition is a literal quote from Pierce.

                                                                                                                                                                                Which definition would you propose instead, which doesn’t dilute the term “type system” to the point where any random bit pattern in memory can be construed as a type?

                                                                                                                                                                                1. 2

                                                                                                                                                                                  One guy makes a claim about something that’s widely contested. It’s popular in a subset of academia. Now, it’s undeniable truth to be reinforced for all time. Am I following that argument about Pierce correctly?

                                                                                                                                                                                  I’ve seen definitions like his or those we’re getting in this thread. I’ve also seen in formal methods community that some build things on a computational basis where some tech computes something that supports the logical system (eg type system). They use a mix of logic and computation to get things done with user defining the types as they go for their specific programs, proofs, and so on. That’s a lot more like developing with languages using dynamic, strong typing far as foundational concepts. Then, some say dynamic is a subset of static but they work so differently in how they’re used. Seem like independent lines of thought much like ALGOL68 vs LISP 1.5.

                                                                                                                                                                                  I doubt the matter is settled because Pierce or any subset of CompSci says so. That experienced programmers are still arguing about it hints at this.

                                                                                                                                                                                  1. 2

                                                                                                                                                                                    I doubt the matter is settled because Pierce or any subset of CompSci says so. That experienced programmers are still arguing about it hints at this.

                                                                                                                                                                                    That’s a bit like arguing that the shape of the earth is not settled, because there are camps advocating for a spherical model and camps arguing for a flat earth model.

                                                                                                                                                                                    To cut it short, one is science, the other one is nonsense.

                                                                                                                                                                    1. 4

                                                                                                                                                                      It’s kind of weird to me to see computer people keep naming more things after mathematicians who already have a lot of things named after them. It’s a funny cultural phenomenon: for computer people, the mathematicians are more like distant relatives than close friends, so cluttering the namespace further doesn’t seem like a problem to them. It’s kind of funny how everything gets called Bayes this, Gauss that, where those mathematicians have the most tenuous relationship to the things computer people are naming.

                                                                                                                                                                      I had to think of what a Poincaré embedding could be… maybe a higher-dimensional manifold into R^2 or R^3? Higher-dimensional topology is something Poincaré really is known for. But no, it’s just the disk model of the hyperbolic plane. Most of the time, I don’t even grace that with Poincaré’s name, kind of like how mathematicians just call finite fields, “finite fields”, very rarely Galois fields.

                                                                                                                                                                      My nitpick isn’t just purely pedantic: this unfamiliarity with mathematics has caused some real problems, such as an AI winter. It’s blindingly obvious that a perceptron was just defining a plane to separate inputs and that lots of of data sets couldn’t be separated by a plane, but because of hype and because Minsky pointed out what really should have been obvious to everyone, connectionism, neural networks, deep learning, or whatever the next rebranding will be, all fell into a deep AI winter. I know I sound like an ass, but it’s both cute and worrying to see computer people struggling with and rediscovering my familiar friends. It almost reminds of me Tai’s model but a little less severe.

                                                                                                                                                                      1. 2

                                                                                                                                                                        But clearly Poincaré embedding is a reference to https://en.wikipedia.org/wiki/Poincar%C3%A9_disk_model. It’s not like machine learning researchers chose the name arbitrarily. The embedding is named after the metric you choose to use for it. These names are informative. When someone say Euclidian, I know nothing fancy is happening. When someone says Gaussian, I know somewhere is a normal distribution in the formulation. When someone say Bayesian, I know I can expect a space to inject priors. The naming isn’t arbitrary.

                                                                                                                                                                        You suggest using the terms mathematicians use, but it’s not clear it makes the work any more accessible. For non-Mathematicians it just means they are more likely to end up on some unrelated paper that doesn’t help them understand the idea. I get where you are coming from, I remember when kernels were a big thing, watching people struggle with what is essentially inner products and properties of inner products. It never helped to tell them they need to understand inner products. I just had to give them LADR and that was enough.

                                                                                                                                                                        I think there is some confusion between the deep learning hype and the people practicing it. The practitioners are mostly aware of the mathematics. It’s everyone downwind that gives the impression of ignorance.

                                                                                                                                                                        1. 3

                                                                                                                                                                          When someone says Gaussian, I know somewhere is a normal distribution in the formulation.

                                                                                                                                                                          For example, Gaussian integers and Gaussian curvatures, right?

                                                                                                                                                                          1. 1

                                                                                                                                                                            I think I could make a connection for Gaussian curvature, but fair point.

                                                                                                                                                                            1. 2

                                                                                                                                                                              I know both probability theory and differential geometry, and I don’t see the connection (pun not originally intended, but thoroughly enjoyed).

                                                                                                                                                                              1. 1

                                                                                                                                                                                Sorry for the delay in responding. One connection I might draw is if you sample points from a multivariate Gaussian, that cloud of points resembles a sphere with Gaussian curvature. It’s a bit of a reach.

                                                                                                                                                                          2. 3

                                                                                                                                                                            I agree the researchers seem to usually know the mathematics, but they speak with such a funny foreign accent. Learning rate instead of step size, learning instead of optimising, backpropagation instead of chain rule, PCA instead of SVD… everything gets a weird, new name that seems to inspire certain superstitions about the nature of the calculations (neural! learning! intelligent!). And they keep coming up with new names for the same thing; inferential statistics becomes machine learning and descriptive statistics becomes unsupervised learning. Later they both become data science, which is, like we say in my country, the same donkey scuffled about.

                                                                                                                                                                            There are other consequences of this cultural divide. For example, the first thing any mathematician in an optimisation course learns is steepest descent and why it sucks, although it’s easy to implement. The rest of the course is spent seeing better alternatives, and discussing how particulars of it like such as its line search can be improved (for example, the classic text Nocedal & Wright proceeds in this manner). People who learn optimisation without the optimisation vocabulary never proceed beyond gradient descent and are writing the moral equivalent of bubble sort because it’s more familiar than quicksort and has less scary mathematics

                                                                                                                                                                            1. 1

                                                                                                                                                                              Is PCA really the same thing as SVD? I suspect I may finally be able to understand PCA!

                                                                                                                                                                              1. 2

                                                                                                                                                                                It’s essentially the SVD. The singular vectors are the directions of highest variation and the singular values are the size of this variation. You do need to recentre your data before you take the SVD, but it’s, like we say in the business, isomorphic.

                                                                                                                                                                                And if you know it’s SVD, then you also know that there are better algorithms to compute it than eigendecomposition.

                                                                                                                                                                                1. 1

                                                                                                                                                                                  SVD is a tool you can use to perform a PCA.

                                                                                                                                                                          1. 11

                                                                                                                                                                            I continue to be unable to understand why I’ve never witnessed any of this. I’m a man who has worked in software for years and before that I was educated in STEM for years. In all this time I’ve seen one single example of the kind of misogyny described here: a senior colleague replied to me and not the intern who asked him a question when the three of us were eating lunch together. That was an odd experience made all the odder by the fact that it was the unique time I’ve witnessed such behaviour.

                                                                                                                                                                            Am I blind? Lucky? It’s not as though I haven’t been trying to find corroborating evidence of this kind of behaviour.

                                                                                                                                                                            1. 37

                                                                                                                                                                              This is why I wrote this. While I’ve been in tech since I graduated in 2001 and have worked with many women I hadn’t seen these behaviors first hand. I write “seen” rather than “experienced” because I’m sure I was oblivious to many instances. Having a female business partner has illumninated to me how pervasive these behaviors are.

                                                                                                                                                                              I don’t see sexism every day but I certainly do every month. Take that as a lower bound and multiply by years in the industry and it’s a lot to bear.

                                                                                                                                                                              1. 26

                                                                                                                                                                                Am I blind? Lucky? It’s not as though I haven’t been trying to find corroborating evidence of this kind of behaviour.

                                                                                                                                                                                I wouldn’t say blind, more like our context-experiences, as men, make a lot of this invisible to us. It’s worth asking coworkers for their experiences with this, if they’re comfortable with it; they’ll have a lot of examples to share.

                                                                                                                                                                                1. 20

                                                                                                                                                                                  I, like the author of the OP, have had a lot of opportunity to watch second-hand misogyny on the part of my wife. My guess is that if you aren’t seeing it, it’s because you’re not close enough to someone to hear how they experience things.

                                                                                                                                                                                  Listening to my wife, the number of open, clearly sexist things that happen over her 8 year career so far has been fairly low. There’ve been a few instances of “Little Girl” comments – the name stems from the first she experienced, when one of the R&D Engineers suggested that the project would’ve been better in the hands of a “real” Manufacturing Engineer, and not some “Little Girl”.

                                                                                                                                                                                  The result of him saying that, by the way, was a slap on the wrist by HR and, later, a promotion to a managerial position where he would only be dealing with men (because the R&D team there was 100% men).

                                                                                                                                                                                  More often, though, are the instances of much smaller, much less overt things. Some are similar to your sole experience, but many are so subtle that I didn’t understand the issue till she explained to me. One common gripe she has is the “Alright guys… and Sarah.”-trope. It’s insidious because it seems inclusive, but in reality it’s singling her out as being different. I asked her what it made her feel like as I’m writing this, she says:

                                                                                                                                                                                  Those sorts of things aren’t hurtful, but they do make me feel exposed. I don’t mind being one of the ‘guys’, I’d much rather you just do that, then make me seem like I need to be coddled/require special attention. Some women I know don’t like being one of the guys, some like being singled out, but none I’ve met mind when you use ‘folks’ or ‘Ladies and Gentlemen’ or some other really common, inclusive phrasing.

                                                                                                                                                                                  (emph mine)

                                                                                                                                                                                  I think these sorts of things can feel really ‘normal’ to someone, even someone looking for sexism and misogyny in the workplace or elsewhere.

                                                                                                                                                                                  Another common kind of misogyny she’s experienced comes in the form of reviews. My wife is a Manufacturing engineer. She’d tell you that being an MFE means that she figures out: “How to take the thing that R&D took 10 months to build 1 of, and make it so we can build 10, 100, 1000, however many a day.” This is a field that requires no small amount of crossfunctional ability. She’s equal parts an ME, EE, Programmer, Quality Control Specialist, Documentation Writer, and half a dozen other things. This means working with lots of people and exerting a lot of will to make things happen simply by convincing people it should. Now, I’m in a similar sort of role, though on the software side. I imagine, given the venue, that you are in some similar situation. I’m sure you’ve known folks who have argued strongly for their position – I imagine you’ve argued strongly for your positions. I know I have. I also know that I’ve never been told to “Be nicer” in my 1:1’s with my boss, or that I was “overly aggressive in supporting my view of the product.” Nor have I ever been called “Petulant,” to my face, by my boss – or anyone else for that matter. My wife is not petulant, she’s passionate. It’s something companies claim to look for in engineers – passion to do good work is important. The difference I’ve seen is not in the actions my wife takes, but in the way those actions are received. This is something broadly hidden from view to outside observers; no one sits in those meetings except her and her boss. When I go hard in the paint to try to argue for a particular design, I don’t leave anything on the table, I make a case as strongly as possible. I can say for a fact that there are times I have been petty and low-minded when I didn’t get what I wanted. I’ve never been called petulant in a review. I’ve never been told I was too aggressive. Even if you don’t believe me when I say my wife isn’t those things, you should at least believe that I’m telling the truth when I claim to be petulant and have never been called on it. Even if you can’t see the misogyny, hopefully that illuminates the privilege that is equal to the problem.

                                                                                                                                                                                  Point being, it’s certainly possible that you work and live in a particularly good environment, where the people are aware and try to curtail this sort of thing, but more likely it’s that the misogyny that’s happening isn’t on the surface. I encourage you to engage with women engineers in an honest and open way; ask them about their experience. Ask them if you’ve been party to that experience. If you care about not doing shitty things to people, it’s worth an ask. Some women will give you the brush off about it – they don’t want to talk about it, that’s okay. But in my experience, when I’ve asked women about their experiences, they’ve been more than willing to tell me; especially when I open with, “Hey, my wife had something shitty happen to her, does this shit happen to you? Can you tell me about it? Do I do this? I’d like to not; but I don’t know if I am.”

                                                                                                                                                                                    1. 3

                                                                                                                                                                                      This is a really interesting article. Thanks for sharing it. Personally I usually just use “People” or “Folks” (as in, “Hey People” or “Hey Folks”); my wife I think was getting at the main point of there being a problem of being singled out, but this article makes a good case for even that ‘more inclusive’ phrasing of “Ladies and Gentlemen” still being about gender. It occurs to me now it also leaves out various folks who find them selves identifying as neither ladies nor gentlemen. Very interesting, TIL.

                                                                                                                                                                                      1. 5

                                                                                                                                                                                        This is the problem that “y’all” was invented to solve.

                                                                                                                                                                                        1. 4

                                                                                                                                                                                          “Y’all” sounds real bad with my New England accent. Seriously, it oughta be a warcrime when I say it.

                                                                                                                                                                                          1. 1

                                                                                                                                                                                            Now you got me curious. I’d probably smirk or smile a bit but no more than over the unusual things down here. I say adapt it and spread it. To heck with the haters! :)

                                                                                                                                                                                            1. 2

                                                                                                                                                                                              It ends up somewhere in the vicinity of rhyming with ‘Mal’ (as in “They stabbed me, Mal, with a sword, how weird is that?”). I can put on an accent and say it okay, but if I’m speaking naturally, it doesn’t really work. Suffice to say my accent ended up in a weird place when it solidified; and while I can force other accents, my default is… pretty weird.

                                                                                                                                                                                              I usually try to speak in a pretty flat accent, but it’s an affectation. My natural accent lives somewhere between a Worcester/Brockton/Rhode Island accent; and leans pretty hard on hard ‘a’ sounds (I pronounce “Java” with an ‘a’ like “at” or “apple”, not one like “hard” or “all”); thus the weirdness with “y’all”.

                                                                                                                                                                                              I sometimes do use “y’all” in text, but it’s usually not something I need to do (if I’m addressing a group, I’ve probably started a chat/am sending an email, and “You all” is more appropriate there).

                                                                                                                                                                                          2. 1

                                                                                                                                                                                            I keep using it being from the South. It’s more efficient. :) It also has the side effect of baiting out those that bully over grammar or just look to argue with those who are perceived as less educated. That’s sometimes useful.

                                                                                                                                                                                            1. 2

                                                                                                                                                                                              I’m not from the South, but given that English lacks a distinct 2nd person plural, and here’s this handy one, why not use it? Plus, it sounds awesome.

                                                                                                                                                                                              1. 1

                                                                                                                                                                                                Well, that’s an interesting take on it. Makes sense.

                                                                                                                                                                                    2. -3

                                                                                                                                                                                      I continue to be unable to understand why I’ve never witnessed any of this.

                                                                                                                                                                                      It’s because misogyny doesn’t actually happen as much as you’d think, based on all the hysteria about it.

                                                                                                                                                                                      The problem is blown way out of proportion, to give the peasants something to pointlessly bicker over while they’re shafted by their governments. It’s the same thing with racism.

                                                                                                                                                                                    1. 12

                                                                                                                                                                                      Chen’s blog post is interesting in both what it references, McIlroy critiquing Knuth, and in what it misses in that exchange.

                                                                                                                                                                                      In short, in 1986 Jon Bentley asked Donald Knuth to demonstrate literate programming by implementing a word-count program which would then be critiqued by Doug McIlroy. Knuth delivered a beautiful example of literate programming in Pascal. 10 pages worth. McIlroy, in addition to his critique, delivered a six-segment shell script that accomplished the same thing without intermediate values…a purely functional implementation as Chen describes it.

                                                                                                                                                                                      McIlroy, among other comments, ends his critique with:

                                                                                                                                                                                      Knuth has shown us here how to program intelligibly, but not wisely. I buy the discipline. I do not buy the result. He has fashioned a sort of industrial-strength Fabergé egg—intricate, wonderfully worked, refined beyond all ordinary desires, a museum piece from the start.

                                                                                                                                                                                      That’s the background.

                                                                                                                                                                                      Chen takes up the topic because he’s intrigued by McIlroy’s solution because it’s purely functional, wondering how he’d do the same today. He writes his solution in Haskell in two variations: “standard” and literate. As a Haskell implementation, it’s effective. Chen then discuss the advantages of both and falls on the side of “standard” rather than literate. Had he left it at that, it would be an interesting bit of Haskell.

                                                                                                                                                                                      A curious exchange in the comment section brings the discussion back to McIlroy’s critique of Knuth. Dorin B takes Chen to task for misunderstanding McIlroy’s point:

                                                                                                                                                                                      You missed the point in McIlroy’s sollution: to use reusable components.

                                                                                                                                                                                      Chen then replies:

                                                                                                                                                                                      No, I think I illustrated exactly the point that McIlroy was making, and I believe that if you emailed him, he would completely agree with me today. … Note how every single line in my Haskell program is in fact a reusable component.

                                                                                                                                                                                      Chen completely misses Dorin’s that for McIlroy’s reusable components isn’t about functions or sub-routines but composable tools. Dorin’s right.

                                                                                                                                                                                      In the interview Chen posted with McIlroy the question that segues into a discussion of his critique of Knuth’s solution begins with a discussion of how pipes effectively invented the concept of the tool. McIlroy says:

                                                                                                                                                                                      McIlroy: Yes. The philosophy that everybody started putting forth: “This is the Unix philosophy. Write programs that do one thing and do it well. Write programs to work together. Write programs that handle text streams because that is a universal interface.” All of those ideas, which add up to the tool approach, might have been there in some unformed way prior to pipes. But, they really came in afterwards.

                                                                                                                                                                                      MSM: Was this sort of your agenda? Specifically, what does it have to do with mass produced software?

                                                                                                                                                                                      McIlroy: Not much. It’s a completely different level than I had in mind. It would nice if I could say it was. (Laughter) It’s a realization. The answer is no. I had mind that one was going to build relatively small components, good sub-routine libraries, but more tailorable than those that we knew from the past, that could be combined into programs. What has… the tool thing has turned out to be actually successful. People just think that way now. That’s providing programs that work together. And, you can say, if you if stand back, it’s the same idea. But, it’s at a very different level, a higher level than I had in mind. Here, these programs worked together and they could work together at a distance. One of you can write a file, and tomorrow the other one can read the file. That wasn’t what I had in mind with components. I had in mind that … you know, the car would not be very much use if its wheels were in another county. They were going to be an integral part of the car. Tools take the car and split it apart, and let the wheels do their thing and then let the engine do its thing and they don’t have to do them together. But, they can do them together if you wish.

                                                                                                                                                                                      MSM: Yeah. I take your point. If I understand it correctly, and think about it, a macro based on a pipeline is an interesting thing to have in your toolbox. But, if you were going write a program to do it, you wouldn’t just take the macro, you’d have to go and actually write a different program. It wouldn’t be put together out of components, in that sense.

                                                                                                                                                                                      McIlroy: So, when I wrote this critique a year or two ago of Knuth’s web demonstration. Jon Bentley got Knuth to demonstrate his web programming system, which is a beautiful idea. …

                                                                                                                                                                                      Now, in 1968, I would have thought he was doing just right. He was taking this sub-routine and that sub-routine, and putting them together in one program. Now, I don’t think that is just right. I think that the right way to do that job is as we do it in Unix, in several programs, in several stages, keeping their identity separate, except in cases where efficiency is of extreme importance. You never put the parts into more intimate contact. It’s silly. Because, once you’ve got them there, it’s hard to get them apart. You want to change from English to Norwegian, you have to go way to the heart of Knuth’s program. You really ought to be able to just change the pre-processors that recognize this is a different alphabet.

                                                                                                                                                                                      For Chen to then argue that his Haskell implementation illustrates exactly McIlroy’s point shows Chen either didn’t read what McIlroy had to say about it, or doesn’t understand it. That’s not to say McIlroy is against functions, sub-routines or software toolboxes. But that’s not the point McIlroy was making.

                                                                                                                                                                                      Of course Chen isn’t alone in misunderstanding Unix and what Thompson, Ritchie, Kernighan, McIlroy and many others achieved with it. In a nutshell this is what distinguishes many BSD users from Linux users.[1] BSD isn’t merely about POSIX, nor is it about avoiding Windows and other proprietary software (important as those goals may be). BSD is mostly about the Unix philosophy.[2]

                                                                                                                                                                                      On the whole, Chen’s discussion of literate vs “standard” program is interesting. As a Haskell programmer, I find his solution informative. As commentator on McIlroy or the Unix philosophy, I’ll look elsewhere.

                                                                                                                                                                                      [1] That’s not to say many Linux users aren’t interested in the Unix philosophy or that all BSD users are Unixphiles. Setting aside criticisms about security, implementation and what have you, the issue many Linux users have with /systemd/ is isn’t Unix-like.

                                                                                                                                                                                      [2] Yes, the various BSDs differ a bit on how that looks and how rigorously to pursue it.

                                                                                                                                                                                      Edit: Fix formatting.

                                                                                                                                                                                      1. 2

                                                                                                                                                                                        I think that the right way to do that job is as we do it in Unix, in several programs, in several stages, keeping their identity separate, except in cases where efficiency is of extreme importance.

                                                                                                                                                                                        We often must ditch this lots-of-separate-programs approach whenever efficiency is of more than negligible importance.

                                                                                                                                                                                        1. 0

                                                                                                                                                                                          I admit I know nothing of the wider context; all I know is what you’ve posted here. But from what you’ve written it sounds like Chen is presenting the 21st century McIlroyian view which may not be the same as the original in concrete terms but is the same spirit rebased on today’s technology.

                                                                                                                                                                                          1. 3

                                                                                                                                                                                            I think Chen is trying to cast McIlroy that way, but for it to be the 21st-century version of McIlroy’s argument, reusable software components would have to come after tools. But that’s not how it went. Indeed, McIlroy says as much in his critique of Knuth:

                                                                                                                                                                                            Now, in 1968, I would have thought he was doing just right. He was taking this sub-routine and that sub-routine, and putting them together in one program. Now, I don’t think that is just right. I think that the right way to do that job is as we do it in Unix, in several programs, in several stages, keeping their identity separate, except in cases where efficiency is of extreme importance.

                                                                                                                                                                                            Chen is saying more than is warranted based on the support he provides (the linked interview). It’s one thing to write something like: “In the same spirit as McIlroy’s reusable tool approach…” It’s another to write:

                                                                                                                                                                                            No, I think I illustrated exactly the point that McIlroy was making, and I believe that if you emailed him, he would completely agree with me today.

                                                                                                                                                                                            Again, that’s not to say McIlroy would disagree with a reusable-component approach to software development.

                                                                                                                                                                                            The point is McIlroy was making a very specific critique of Knuth’s program based on value of tool over software reuse and composition and Chen completely missed it. And then asserts McIlroy would agree with him that writing software with reusable software components is point McIlroy was making.

                                                                                                                                                                                            Chen misunderstands McIlroy, and worse, imputes his misunderstanding to McIlroy.