1. 3

    Nitpick:

    <p>"Oil"</p><p>&quot;Oil&quot;</p>. The former might be valid HTML, but the latter is better. (The former is also not valid XML.)

    The former is a perfectly valid[1] XML, there’s nothing wrong with " outside tags.

    [1]: More correctly, it’s well-formed. “Valid” only has meaning against a specified DTD schema, which is absent here. But if we assume it’s HTML, then it’s also a valid HTML fragment.

    1. 3

      Yes, you’re right, I made a correction:

      http://www.oilshell.org/blog/2018/02/14.html#toc_2

    1. 9

      Why are engineers so bad at paying other engineers for their work?

      Well, in this particular case, it’s because the result of the work sucks. Trying using SumoLogic to look at our own logs had been a very unpleasant experience for us. And after spending some time with the product I realize that it’s intentional: the product seemingly exists only for the purpose of selling consulting services with it. I.e., it doesn’t just solve the problem of aggregating a big amount of logs from several hosts, it also couples it with an unworkable browser-based UI, a custom query language, inability to post-process data. And a simple thing like tail -f is considered a “premium” feature, which they call LiveTail™, and which is so limited that it’s incompatible with most of their own filters. And then you get blog posts from SumoLogic condescendingly telling you that “you can only do so much with command line tools” and if you want to be a grown-up, you should start by attending a workshop that would teach you how to use their system.

      [/rant]

      Now, I understand that the general gist of the post is not about it, and I probably agree with the one that is there. But it did mention SumoLogic, so it got me started :-)

      1. -2

        It is, after all, a truth universally acknowledged, that a program with good use of data types, will be free from many common bugs.

        I’m afraid it is only so for the value of “universally” meaning “other fans of type safety”. And that’s a rather constrained subset.

        1. 2

          A language being free from a many common bugs does indeed change the set of common bugs for that language. But that doesn’t mean that it is indeed free from many common bugs of the languages without those safety features. You absolutely do gain a certain amount of safety the stronger your type system is and that does provide a fair amount of value that shouldn’t be dismissed just because there are still possible bugs. Type systems in many cases manage to push the remaining bugs into the “spec”. Which has the benefit of allowing you to fix the bug by fixing the spec and then having a compiler tell that you have indeed actually fixed said bug.

          For developers who can leverage this power it’s really useful and increases productivity. For those who can’t yet leverage this power it just feels like the language is slowing you down.

          1. 0

            I’m not trying to discuss the issue itself, I’m pointing out that that “truth” is not universally accepted, not even close.

            Talking about the issue, one of the assumption by type safety advocates I have qualms with is the word “many” here:

            A language being free from a many common bugs does indeed change the set of common bugs

            Another is this implied assumption that any gain in safety is good, without considering the disadvantages:

            You absolutely do gain a certain amount of safety the stronger your type system is and that does provide a fair amount of value that shouldn’t be dismissed just because there are still possible bugs.

            This is trivialization of the opposing view. Strong type safety system may be dismissed not because “there are still possible bugs” but because on balance they remove too few for too much effort. Simple as that.

            1. 1

              you’re shifting the goalposts a little. Sure, maybe the balance of safety versus effort is not worth it for you. But that doesn’t mean that there isn’t a much smaller set of bugs with type safety than without, all else being equal.

        1. 3

          I am pretty convinced that it’s the wrong question to ask. You don’t “prove” anything to your prospective employer, because it’s not a University exams, and a job is not a favor. You come to an interview with the skills you have, and it’s their job to find out if they can use them. If they don’t it’s either because they simply don’t or they failed to recognize those. In both cases it’s not a candidate’s failure, you just go and look for another company.

          (Unless of course you really don’t have any useful skills, but from your question it doesn’t seem to be the case :-) )

          1. 1

            I think the virtue of this advice is that it enhances the confidence of those who believe it. You don’t internalize the rejection so you are more confident in the face of future adversity.

            I know that I internalize that rejection as a total judgment of my abilities. It’s easy to forget that interviewing is a game of imperfect information for both sides.

            1. 1

              You make a good point and I will certainly keep it in mind, but as a principle I don’t particularly like burden-shifting. The stoic in me wants to figure out how I can make something better.

              1. 2

                You’re in a bad position for that, however. Because no interviewer/recruiter is going to give an honest answer why they don’t want to hire you (even when they could). So you can’t really make an informed decision and learn from it.

            1. 21

              To be honest, most of my goodwill towards Tim Berners-Lee (which there was a lot of, by the way) went away when he started shilling for web DRM. Requiring w3c compliant browsers to ship closed source BLOBs in order to correctly display w3c compliant web pages is against the very core of the open web; not to mention how the w3c wouldn’t even protect security researchers who want to see if there are security issues with said BLOBs. I know Berners-Lee probably isn’t responsible for every one of those decisions, but he publicly (and probably internally in the w3c) argued for DRM.

              For further reading, here’s a great (albeit long) article from the EFF: https://www.eff.org/deeplinks/2017/10/drms-dead-canary-how-we-just-lost-web-what-we-learned-it-and-what-we-need-do-next

              1. 7

                Computers, the Internet, and the web represent some of the greatest innovations in the history of mankind and the fruition of what could have only been a fantasy for billions of our ancestors for thousands of years. To see it so quickly, in the course of a few decades, and thoroughly corrupted by the interests of corporate profits is profoundly sad. I am severely disappointed to have dedicated my life to the pursuit of mastering these technologies which increasingly exist primarily to exploit users. DRM is a thread in a tragic tapestry.

                1. 3

                  At this point my usual plea is, judge what’s spoken, not by whom it’s spoken. TBL’s authority is one thing, and the merit of what he has to say about that “Solid” thing is quite another. The idea feels very sane to me, although I don’t see a clear path of shoving it past the influence of all the silo-oriented companies like Facebook and Google.

                  1. 2

                    “At this point my usual plea is, judge what’s spoken, not by whom it’s spoken.”

                    This sentiment was drummed into me as a child and ordinarily I would strive to do this to a point, but the topic of putting locks on the open web by way of DRM is to me related to the apparently opposed mission of “solid”.

                    Arguing for decoupling data from applications provided by corporate giants in the interests of user control seems absurd when he just played a major part in removing transparency and control from a user’s web experience.

                    I’m not quite sure what to make of this.

                    1. 2

                      Did you consider the possibility that DRM could also work in reverse? The Digital Rights Management of individuals. I think that is the underlying motivation for allowing DRM: to protect assets and information. Users can not freely copy media to which they have no right of ownership, and conversely, companies can not freely copy user data to which they should have no right of ownership.

                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. 17

                                      If only json had allowed trailing commas in lists and maps.

                                      1. 9

                                        And /* comments! */

                                        1. 3

                                          And 0x... hex notation…

                                          1. 3

                                            Please no. If you want structured configs, use yaml. JSON is not supposed to contain junk, it’s a wire format.

                                            1. 4

                                              But YAML is an incredibly complex and truth be told, rather surprising format. Every time I get it, I convert it to JSON and go on with my life. The tooling and support for JSON is a lot better, I think YAMLs place is on the sidelines of history.

                                              1. 4

                                                it’s a wire format

                                                If it’s a wire format not designed to be easily read by humans, why use a textual representation instead of binary?

                                                If it’s a wire format designed to be easily read by humans, why not add convenience for said humans?

                                                1. 1

                                                  Things don’t have to be black and white, and they don’t even have to be specifically designed to be something. I can’t know what Douglas Crockford was thinking when he proposed JSON, but the fact is that since then it did become popular as a data interchange format. It means it was good enough and better than the alternatives at the time. And is still has its niche despite a wide choice of alternatives along the spectrum.

                                                  What I’m saying is that adding comments is not essential a sure-fire way to make it better. It’s a trade-off, with a glaring disadvantage of being backwards incompatible. Which warrants my “please no”.

                                              2. 1

                                                http://hjson.org/ is handy for human-edited config files.

                                                1. 1
                                                2. 5

                                                  The solutions exist!

                                                  https://github.com/json5/json5

                                                  I don’t know why it’s not more popular, especially among go people.

                                                  There is also http://json-schema.org/

                                                  1. 3

                                                    I had to do a bunch of message validation in a node.js app a while ago. Although as Tim Bray says the spec’s pretty impenetrable and the various libraries inconsistent, once I’d got my head round JSON Schema and settled on ajv as a validator, it really helped out. Super easy to dynamically generate per message-type handler functions from the schema.

                                                    1. 2

                                                      One rather serious problem with json5 is its lack of unicode.

                                                    2. 3

                                                      I think this only show that JSON has chosen tradeoff that make it more geared to be edited by software, but has the advantage of being human editable/readable for debugging. JSON as config is not appropriate. There is so many more appropriate format (toml, yaml or even ini come to mind), why would you pick the one that doesn’t allows comments and nice sugar such as trailing commas or multiline string. I like how kubernetes does use YAML as its configuration files, but seems to work internally with JSON.

                                                      1. 8

                                                        IMO YAML is not human-friendly, being whitespace-sensitive. TOML isn’t great for nesting entries.

                                                        Sad that JSON made an effort to be human-friendly but missed that last 5% that everyone wants. Now we have a dozen JSON supersets which add varying levels of complexity on top.

                                                        1. 11

                                                          “anything whitespace sensitive is not human friendly” is a pretty dubious claim

                                                          1. 5

                                                            Solution: XML.

                                                            Not even being ironic here. It has everything you’d want.

                                                            1. 5

                                                              And a metric ton of stuff you do not want! (Not to mention…what humans find XML friendly?)

                                                              This endless cycle of reinvention of S-expressions with slightly different syntax depresses me. (And yeah, I did it too.)

                                                              1. -5

                                                                Triggered.

                                                                1. 13

                                                                  Keep this shit off lobsters.

                                                        1. 17

                                                          I love the smell of outrage in the morning. Or afternoon. Whichever.

                                                          I like Firefox. I’m not terribly concerned about this. A sure way to get them to stop is to donate monthly.

                                                          1. 15

                                                            How much? How much would it cost to stop this, over and above Mozilla’s existing income? Why doesn’t Mozilla, as a user first organization, tell its users “we need this much money or we’re going to add the looking glass extension”?

                                                            1. 6

                                                              Oh, yes, a 1000 times this! I’d happily pay for Firefox more than I pay for every single web service I use.

                                                              1. 5

                                                                It would cost an infinite amount, because that’s the amount companies need to aim to earn in a capitalist economy.

                                                                1. 5

                                                                  It’s a non-profit.

                                                                  1. 3

                                                                    Even non-profits have expenses to cover. Over infinite time these approach infinity as well.

                                                                    The point still stands that them having a transparent budget would make it easier for us the users to “pay off” these kinds of threats.

                                                                    1. 3

                                                                      The mozilla corporation (a branch of the mozilla non-profit Foundation) is for-profit.

                                                                      1. 3

                                                                        Only legally. It’s “keep the lights on”.

                                                                        The problem is that software development and the services the corp provides is not considered non-profit under most jurisdictions.

                                                                        This setup (a foundation and a corporation) is straight from the playbook for non-profits that have substantial non-eligible parts.

                                                                2. 4

                                                                  A sure way to get them to stop is to donate monthly.

                                                                  They made $360,000,000 last year: https://www.ghacks.net/2017/12/02/mozillas-revenue-increased-significantly-in-2016/

                                                                  Why would you want to throw more money at the corporation who’s pissing on you while telling you that it’s raining?

                                                                  1. 8

                                                                    When you are donating to Mozilla, you are donating to the Foundation, which is not involved much in Firefox, but in a lot of other tech and policy advocacy things. This includes net neutrality lobbying, discussing the copyright reform in Europe and support many many tech teaching projects all over the globe.

                                                                    You’d be hurting all those projects instead of Firefox development over your anger with the product.

                                                                    Making your anger known in a different fashion will have more impact.

                                                                    (FWIW: I don’t want to keep you from stopping to donate if you don’t feel like Mozilla Foundation is not following their mission anymore)

                                                                    1. 4

                                                                      Regrettably, the net neutrality thing didn’t pan out, I’m not sure about the copyright work, and the educational stuff is probably better left to local efforts (if my own experience is to be believed).

                                                                      I’d rather they focus on Firefox, Thunderbird, and documentation and free up people and resources to go do other things.

                                                                      1. 6

                                                                        Regrettably, the net neutrality thing didn’t pan out, I’m not sure about the copyright work, and the educational stuff is probably better left to local efforts (if my own experience is to be believed).

                                                                        Policy is no “put enough money here, it’ll work” game. The debate about net neutrality has been going back and forth in the recent years and Mozilla has always been involved. Losing Mozilla as a campaigner there would not be helpful in any way.

                                                                        The educational stuff is probably better left to local efforts (if my own experience is to be believed).

                                                                        This is obviously very personal, but in my experience, Mozilla has reach to a lot of people and other groups that other tech groups can only dream of. I would highly recommend looking at who’s around at MozFest. Also, the Foundation does a lot of these things through co-operations like with the Ford Foundation, which are usually quite productive and the output brings a lot of worthwhile reading.

                                                                        I’d rather they focus on Firefox, Thunderbird, and documentation and free up people and resources to go do other things.

                                                                        Thunderbird obviously left out, Mozilla Corporation has most employees on precisely these products. It is their focus.

                                                                        The Corp is just not the Foundation and merging them also makes no sense, IMHO.

                                                                  2. 2

                                                                    Or use a fork if all else fails. Sad day if it comes to that, after all the good work otherwise gone into Firefox.

                                                                  1. 3

                                                                    Let me try and have a go at it :-)

                                                                    The sad truth of it is, no we can’t. Because we can’t compare what we do with what would have happened if we did something differently. Because there would be other factors at play.

                                                                    • We’re having fewer outages than our competitors or other teams doing kind of the same thing? May be it’s our architecture, but may be we just hired better people or what we do is different from they do in some key aspect.
                                                                    • We used to have more outages, changed the architecture, and now there are fewer of those? Well, may be we just got more experience over this time and our old architecture would’ve served just as well.
                                                                    • We switched from that (clunky static|incoherent dynamic) language to this (expressive dynamic|reliable static) language and are happy about it? Chances are, people on this particular team just prefer this mental model over that one.

                                                                    About that last point… This is what it all comes down to, for me: if this particular team doing this particular project feels happy about architectural choices being made, then they’re good choices. We can’t measure it objectively (and it may even be impossible). And yes, it means that another team might do better, but this is irrelevant because there’s no “other team” anyone could just put on this project at no cost. The quality of architecture is the function of a team anyway.

                                                                    1. 1

                                                                      Thanks! Capturing that subjective side seems important. The architecture is going to have as much to do with team quality-of-life as with objective capability measures, and the relation is reflexive; a happier team will not want to subvert or “work around” the architecture, and a supportive architecture will make the team happier.

                                                                    1. 16

                                                                      I think it might be interesting to look at the blast radius for incidents, though, I have no idea what kind of software you work on…

                                                                      But imagine you have a single rails app that does everything for your customers and it goes down, due to a database failure, or something… what happens to your availability? It goes to 0 for the time the outage lasts. The blast radius of the database outage blows up your entire kingdom.

                                                                      You’re smarter than that, of course, so you move to a service oriented architecture. Then, a database goes down, and the whole kingdom blows up again.

                                                                      You correct that by creating more databases that exist per service, and your database for the “private messages” feature goes offline… you’ve affected part of your customer base, but only a small part of the entire kingdom is suffering— the blast radius was reduced, and your customers are happy because you’ve made decisions that keep partial availability under most problems that come up, so total outages are very rate.

                                                                      Also, similarly, the number of self-inflicted incidents caused by bad changesets/deploys. Your software engineering practices should explicitly target reducing this as a goal, and your architecture is very important in containment here.

                                                                      1. 1

                                                                        I like the “blast radius” analogy, thanks :). “Are we encountering fewer problems and having less difficulty as a result of those we do encounter” is a great thing to measure, along with “are we trying to find new problems in areas we couldn’t have thought about/would have run away from before”.

                                                                        1. 1

                                                                          The question is, less difficulty compared to what? To “us” doing almost exactly the same thing but with controlled bits different in a parallel universe? Because that’s the only way to compare apples to apples.

                                                                          1. 2

                                                                            Progress is measured by comparing parallel universe today to parallel universe yesterday.

                                                                            It’s important to remember that not all forward motion is progress, it’s possible for a code bases to grow simultaneously less stable, harder to work on, and less feature-rich over time.

                                                                            1. 1

                                                                              I agree. “Do we have this problem less often than we did before” could be a goal, but it takes a bit of asking why to find out whether that’s because we designed it out of the solution, or because we employ a bunch of avoid-that-problem people.

                                                                      1. 9

                                                                        I would also add: be ready to be questioned back with “What is it that you’re trying to do” when presenting an expert with a possible solution. Chances are you’re trying to solve a problem in a very roundabout way, and there is a more idiomatic, better way to solve your problem. So don’t be shy in describing your end goal.

                                                                        1. 9

                                                                          Don’t forget to describe your constraints along with your goal. Otherwise you might get very unhelpful answers.

                                                                        1. 2

                                                                          Seems like this is targeted specifically at the use case of running inside a browser.

                                                                          I’m just transitioning from npm to yarn for my own projects. Current versions of either seem pretty good to me, and much improved over old versions of npm in terms of speed.

                                                                          Faster is always better, but I don’t feel seriously inconvenienced by existing tooling anymore (at least on my own projects, which are not that large.) Are there still major performance concerns for typical projects with existing tools?

                                                                          1. 1

                                                                            I’m just transitioning from npm to yarn for my own projects.

                                                                            I wonder when do you JavaScript people actually program for users :-)

                                                                            1. 1

                                                                              What users? ;-)

                                                                              I probably should have specified “for new projects”, but in any case, your point stands!

                                                                          1. 2

                                                                            support for Python 2.7 is removed

                                                                            That’s a shame. I do definitely appreciate Django’s relatively long LTS support timeframes and the work that has to go into that but it’s unfortunate I’ll have to make a decision between the py2 line and Django in 2020.

                                                                            1. 2

                                                                              I’m sorry but the only shame is that it took so long. Supporting obsolete versions is expensive, and the decision to move off Python 2 has been made, what, 10 years ago? I don’t know why people insisting on supporting Python 2 expect the entire community to pay the price. Still.

                                                                              1. 2

                                                                                I don’t know why people insisting on supporting Python 2

                                                                                At least in my case it’s because I don’t view Python 3 as a net gain with respect to Py2. People are still starting projects in Py2 despite library support for Py3 having been solid for years, migration costs are pretty low (you can migrate a fairly large codebase in a weekend). It seems like there’s pretty good evidence that the reason Py3 adoption is slow is because people don’t particularly want to work in Py3, so it’s natural that major libraries dropping support for Py2 isn’t happy news: if forces us to use something we otherwise wouldn’t.

                                                                            1. 9

                                                                              Silicon Valley doesn’t get out much

                                                                              This made me smile :-) A real writing gem :-)

                                                                              1. 3

                                                                                As if it’s the tools that are the main obstacle for effective communication… And not people who drop conversations, ignore all but the single topic in an email, reply with empty ideas in the hopes that it’s someone else whose job is to understand and organize everyone’s thoughts. Or the people who turn every code review into a War of Programming Paradigms starting with something as minute as a variable name. But yes, I sure hope yet another integrated system is going to beat sense into everyone. Because integrated. And because GitHub.

                                                                                1. 5

                                                                                  Why does every headline mention “MINIX based” now? MINIX is not what’s bad about it >_<

                                                                                  1. 4

                                                                                    On the other hand if “Minix” becomes synonymous with “that spyware OS” in public perception maybe it will get Tannenbaum to realize the whole “BSD licensing offers the users maximum freedom” schtick is hilariously backwards.

                                                                                    1. 4

                                                                                      Tannenbaums statement about the news MINIX was being used continued to support the BSD license. He only wished that Intel had told him, cause it would have been cool to know.

                                                                                      1. 0

                                                                                        He also said “this bit of news reaffirms my view that the Berkeley license provides the maximum amount of freedom to potential users” which is just utterly delusional.

                                                                                        1. 12

                                                                                          Intel is the user. Intel got maximum freedom. I don’t see what is ambiguous about that.

                                                                                          Unless, are you are recursively applying a broader concept of freedom to all users potentially affected by consequences of the license choice? Because that’s an entirely separate matter altogether. And highly subjective.

                                                                                          1. 7

                                                                                            It seems to me that I am the user of my CPU and all the software on it, Intel is just the manufacturer. At least legally, morally, and in terms of how GP used the term. Unfortunately there may be an argument that Intel is a user in reality.

                                                                                            1. 5

                                                                                              You’re a user of your CPU as a complete product, not of MINIX. Intel is the user of MINIX, they are the ones the license applies to. Legally speaking, that much is completely unambiguous.

                                                                                              1. 3

                                                                                                Intel is the distributor of Minix, they require a license to create copies and distribute it because that’s how copyright works.

                                                                                                I do not need a license for my use of Minix because my use does not create a copy or otherwise implicate copyright law. That does not mean I am not the user, legally or otherwise. Just as I am the user of a book when I read it, but I do not require a license to do so.

                                                                                                1. 4

                                                                                                  Precisely, Intel is the user of the license. That was the intended meaning of user in Tannenbaum’s letter.

                                                                                                2. 1

                                                                                                  Hmmm. Just like I may be a user of a Dell Machine with Windows on it? But in that case, the license applies to me.

                                                                                                  MINIX’s license applies equally to source and binary forms, so the “user” is actually quite questionable. Technically, it seems that the license is passed on to me, the user of the CPU, since the copyright notice and such must be distributed along with a binary distribution…

                                                                                                  So, I guess I could legally redistribute my changes to the binary blob that Intel puts on the CPU, too, no? Of course, provided my changes are also released under a BSD license. (Difficulty of this aside)

                                                                                                  Disclaimer: IANAL.

                                                                                                  1. 4

                                                                                                    Hmmm. Just like I may be a user of a Dell Machine with Windows on it? But in that case, the license applies to me.

                                                                                                    Totally different. Intel is licensing MINIX as a component. Dell is an authorized reseller of Windows, i.e. they are authorized to sell you a Windows license along with their product. While they probably license Windows for their employees, they don’t license Windows as a part of the product. Their terms of resale allow them to modify the original distribution, to include drivers and so on. Also crapware, apparently.

                                                                                                    MINIX’s license applies equally to source and binary forms, so the “user” is actually quite questionable.

                                                                                                    No, it isn’t. The user of the license is the distributor. The license notice must be attached. That’s all.

                                                                                                    Technically, it seems that the license is passed on to me, the user of the CPU, since the copyright notice and such must be distributed along with a binary distribution…

                                                                                                    A notice of license use does not constitute a license grant. That is, if I buy a software library A and include it in my product, that does not transitively grant a license for A to all of my users. That would be absurd.

                                                                                                    So, I guess I could legally redistribute my changes to the binary blob that Intel puts on the CPU, too, no? Of course, provided my changes are also released under a BSD license.

                                                                                                    BSD does not require you release derivatives under a BSD license, only that you attach the original license in the documentation or other materials provided with your derivation. And you could only redistribute changes if Intel’s license for their blob permits redistribution.

                                                                                            2. 3

                                                                                              He also said “this bit of news reaffirms my view that the Berkeley license provides the maximum amount of freedom to potential users” which is just utterly delusional.

                                                                                              How is it delusional exactly? Seems to be correct, the freedom for intel to use it in the way they see fit is preserved.

                                                                                              1. 2

                                                                                                BSD is about developer freedom whereas GPL is about end user freedom. For Tannenbaum to claim otherwise is bizarre. He should be arguing for the license he chose on its merits.

                                                                                                1. 5

                                                                                                  What are you talking about? He said BSD provides maximum freedom to potential users. And the next sentence makes it extremely clear he is referring to developers like Intel, not end users.

                                                                                                  So as far as I’m aware Tannenbaum never made any such claim. He certainly didn’t in his open letter to Intel.

                                                                                            3. 1

                                                                                              Intel is the user here, and Intel indeed got maximum freedom. I see nothing wrong with that.

                                                                                              What kind of license would you suggest?

                                                                                              GPL/copyleft? Wouldn’t do anything, Intel would just reluctantly post an uninteresting dump of MINIX source with the tiny modifications they made to make it fit in a small device.

                                                                                              “Don’t use this for evil” licenses? They’re just broken. Incompatible with any existing FOSS licenses. No one will use your code.

                                                                                              1. 12

                                                                                                GPL/copyleft? Wouldn’t do anything

                                                                                                The whole point of the tivoization clauses of the GPLv3 is to make it illegal to prevent the end user from modifying this kind of thing and allowing them to remove user-hostile behavior.

                                                                                              2. 1

                                                                                                BSD forbids the use of the original name without author’s permission, so the license is fine. But no license is going to protect you from FUD and journalist misinterpretation.

                                                                                            1. 5

                                                                                              When I was but a wee child I was told by a fellow colleague that UML would fundamentally change the way code was written, that it was the next revolution. I didn’t really believe him back then mostly because I hated his guts but it’s almost ten years later now and I have decent experience now, and I like to think I’m also slightly wiser.

                                                                                              “I assure you this one tool will fix all our problems”, isn’t that exactly what we talk about when we talk about silver bullets? Don’t get me wrong, I’m convinced AI has a very important place in our collective future as programmers (heck, even the present for a lucky few). Experience has shown for me that it’s unlikely to be a magical problem solving thing, very much like UML was not. I’m sure history is littered with such broken promises of things that are nowadays tools we use daily.

                                                                                              1. 2

                                                                                                Exactly. And it’s actually easy to spot the problem right in the text where the author says that “we specify some constraints on the behavior of a desirable program”, and the “program” is then deduced by a neural network. Shifting the actual hard part — decision making — to some other stage and not consider it a part of coding still doesn’t make it go away.

                                                                                              1. 11

                                                                                                This article right here in a nutshell is the good, bad and ugly of the web application platform:

                                                                                                Good: Browsers can implement whatever the heck they like, with amazing innovative results

                                                                                                Bad: Other Browsers don’t support these things out of the gate, so it is left as an exercise for the developer (or they just give up and only support one browser - a highly popular approach in the late 90s and early 00s)

                                                                                                Ugly: Stuff just breaks all the time and there is no accountability. Standards are skirted and ignored. Committees are formed and deemed too slow/unfriendly to innovation, creating rival committees (W3C vs WhatWG, etc).

                                                                                                If you read this far, I hope you weren’t expecting a proposal to fix it? ;)

                                                                                                1. 9

                                                                                                  That is why I never use $MOST_POPULAR_BROWSER_ENGINE. I hope it will help avoiding monopolisation.

                                                                                                  1. 3

                                                                                                    Well, to be honest, WhatWG was the right thing to do to jolt W3C out of its self-induced XHTML 2 coma.

                                                                                                    1. 2

                                                                                                      I was an XHTML2 believer back when I thought the W3C was still a real thing. Now they just whitewash stuff vendors have already shipped.

                                                                                                      1. 11

                                                                                                        If you rephrase it as “they standardize proven implementations” it becomes more palatable. And history actually shows that it’s the only way to produce useful, usable standards. You can’t invent a spherical XHTML in a vacuum and expect it to be implementable.

                                                                                                  1. 1

                                                                                                    That went smooth! Thank you all!

                                                                                                    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.