1. 3

    In my experience, with anything of any significant complexity, this sort of approach ends up being more work than straight LaTeX. On top of that, the conversion tools change too much inbetween versions to guarantee longevity.

    1. 2

      Having worked on a 1,200 page book I am going to concur. I started out using markdown+Pandoc and it became a time loss pretty quickly.

    1. 29

      This is pretty wonderful. I’m happy to help you run stats like these for a quantitative post, but the moral of this story is the importance of human connections, I think you have captured here most of what there is to learn.

      I still was routinely downvoted as “troll”.

      This surprises me a bit. I hope the incidence was much lower, but perhaps it can be explained as reputation carrying over, people read comments in your old tone. Then perhaps we’d see them on posts a sentiment analyzer judged as ambiguous or intermediate. Hm.

      1. 15

        but perhaps it can be explained as reputation carrying over, people read comments in your old tone

        I’m guilty of doing this. I thought the friendlysock name change was one big troll. It wasn’t until reading this post that I even knew it was an earnest attempt to be nicer. Sorry @friendlysock :-(

        1. 9
          I still was routinely downvoted as “troll”.
          

          This surprises me a bit. I hope the incidence was much lower, but perhaps it can be explained as reputation carrying over, people read comments in your old tone. Then perhaps we’d see them on posts a sentiment analyzer judged as ambiguous or intermediate. Hm.

          At first blush this surprised me too, but honestly I think there are some people who mis-understand what “troll” is for and are a bit too quick to pull this particular trigger.

          1. 12

            I get downvoted as troll most often in contexts where I’m replying earnestly and constructively. It doesn’t get used well and the only way to avoid it is not to disagree with anyone and avoid posting in threads where people you disagree with might be reading.

            1. 3

              I would love to see downvotes only when commenting (so you can explain downvotes). Sometimes I see totally valid comments (for my point of view) being downvoted, and as a reader I don’t know why… it’s probably frustrating for the commenter and the readers.

              1. 5

                I’m not sure that’s a good idea. If I disagree with someone or maybe I don’t understand their position, I write a comment, and don’t downvote.

                Requiring a comment for a downvote can lead to the following undesirable behaviors:

                • Trolls feed on attention, someone actually sitting down and writing a disagreement will only ensure they have been succesfull.
                • It attaches a username to a disagreement, possibly leading to harassment, retaliatory downvotes, etc.
            2. 4

              I still was routinely downvoted as “troll”.

              This surprises me a bit. I hope the incidence was much lower, but perhaps it can be explained as reputation carrying over, people read comments in your old tone.

              Could have been me. I’ve downvoted @friendlysock and other’s posts as troll before when I thought they were politely defending/promoting caustic attitudes, discrimination, or other behavior damaging to a community. I realize there are a lot of folks who prefer a written explanation, but I rarely have the bandwidth to sit down and compose a response.

              That said, I do appreciate @friendlysock’s reflection and change in communication style despite our differences in perspective on other subjects.

            1. 2

              I work too much but that’s because of my side projects like the book and OSS stuff. This is nothing my employer asks or expects of me.

              1. 5

                For work: I’m re-implementing some abandoned cart handling in the CMS we’re migrating to.

                For me: I’m continuing work on siftrss, fleshing out my unit test suite to better cover edge cases concerning feeds with off characters, encodings, namespaces, etc. Ahhh, they joys of working with XML for no money. :)

                1. 2

                  I used your project as inspo for some Rust code I hacked on while streaming.

                  1. 2

                    Hey, it’s you! I saw that a while back when I happened to search for mentions of siftrss on Twitter. I’m glad I could lend some inspiration for your project!

                    I love how clean your code is. I don’t know much about Rust, but your code makes me want to give it a go. I’ve been meaning to get around to writing a serious project in a functional language.

                    1. 3

                      Thank you very much!

                      My main thing (day job and personal projects) is Haskell, which may have something to do with the style of my Rust code. There’s a lot of idioms I ignore/wrap in Rust.

                      Case in point, I got irritated with the useless (IMO) information hiding in the rss crate so I forked and patched it: https://github.com/bitemyapp/shiftrss/blob/master/Cargo.toml#L15

                      Didn’t get upstreamed, they special-cased a setter or whatever for the thing I was doing.

                      I use Rust because it’s a reasonably type-safe language with sweet-spots (super perf sensitive, no GC) that are complementary to Haskell (everything else)

                      1. 1

                        Right on! I’ve poked at Haskell a couple times, but never used it to write anything of substance. Of course, my list of languages to try out grows faster than my list of projects… which is often longer than I have time for in the first place, haha. I’ve been meaning to try out Elm, as I wanted something new to play around with on the front end.

                        Rust sounds very interesting. Consider my interest piqued!

                1. 3

                  Instead of reaching for MSG as a shortcut to Umami Town, consider Worcestershire sauce, light soy sauce (like usukuchi), and/or a dash of fish sauce. Garum has been used for thousands of years to enhance savory dishes; don’t fight it. Just don’t add it too late in the cooking process or you will have a fishy aftertaste instead of the small peptides and free amino acids you’re after.

                  1. 2

                    It’s very funny that so many people use MSG for stews. I’ve always been cooking them without and never needed it. But you have to use very fat cuts of meat + ones with bones (oxtail, …), which is nice since they’re the cheap parts.

                    1. 1

                      I used worcestershire-and-butter browned mushrooms in the example recipe I made last week. Scroll down to near the bottom of the post and click the link.

                      I just also use MSG because I’m not going to eat less tasty food for the sake of other peoples’ snobbery.

                      I’m familiar with the use of soy and fish sauce of various kinds (see my reference to Sichuan cooking), but I don’t feel they’re compatible with the flavor I go for in my stews.

                    1. 13

                      Except that, even though you knew the type, you still knew nothing about the structure of that JSON

                      That’s nonsense, use Generics or TemplateHaskell and make a config that fits the pattern you want and you get automatic JSON parsing from your types in addition to getting to know the structure of the JSON based on the structure of the data type. This isn’t a property some Haskellers actually want, but the option is there if you do.

                      What we wound up doing was nesting pattern matching to get at the value we wanted. The deeper the JSON nesting, the deeper our pattern matching. We wrote functions to wrap this up and make it easier. But in general, it was a slog. The tools Haskell gives you are great at some things, but dealing with arbitrarily nested ADTs is not one of them.

                      This is utterly unnecessary for both the JSON handling itself: https://github.com/bitemyapp/bloodhound/blob/master/src/Database/V5/Bloodhound/Types.hs#L1951-L1965

                      And for working with nested types in general: you can use lenses, but even with a very nested API like Elasticsearch’s just being able to compose accessors is generally enough.

                      I’m familiar with this guys’ schtick, he did some Haskell back in like 2010 with a Happstack based application and nothing was particularly nice. If I was stuck with Happstack, I’m not sure I would want to use Haskell either.

                      Rich had some good points about positional semantics. When defining an ADT, positional semantics make it hard to read the code. If you’ve got seven arguments to your ADT’s constructor, you’ve probably got them in the wrong order and you’ve forgotten one.

                      First, I avoid passing a bunch of the same type in consecutive order to a data constructor.

                      I avoid Text -> Text -> Int -> Int -> MyType and replace it with: HostName -> Alias -> PortNumber -> WorkerCount -> MyType or some-such, further, if there’s more a few arguments to a data constructor I’ll use record syntax to construct the value:

                      MyType {
                           hostname = myHostname
                        ,  alias = myAlias
                        ,  portnumber = myPortnumber
                        ,  workercount = myWorkercount
                        }
                      

                      Then ordering doesn’t matter. I usually set record fields strict, especially if I plan to use the record syntax, so that I can’t forget anything.

                      The fact is, in real systems, these ADTs do accrete new arguments.

                      I can’t say I recall the last time Value got a new constructor or one of its data constructors got a new argument, but I’d sure be grateful that my type system would be there to tell me everywhere in my project I need to fix the code if it did.

                      I don’t have the patience for the rest of this.

                      — Went from Clojure -> Haskell

                      1. 8

                        Don’t waste your breathe dude there is a much simpler rebuttal: static and dynamic types are a false dichotomy so any attempt to discount one in context of the other is an invalid argument

                        Instead weight the specific features of the type systems against each other. In the case of Haskell vs Clojure, GHC gives you much more feedback than the entire Clojure ecosystem of spec/schema etc so if the criteria for choosing a language is type safety then Haskell wins.

                        1. 12

                          static and dynamic types are a false dichotomy

                          Absolutely. People have written some useful stuff about this:

                          https://existentialtype.wordpress.com/2011/03/19/dynamic-languages-are-static-languages/

                          1. 2

                            I actually don’t totally agree with that article. I’m channeling Foucault here: our understanding of type systems is dependent on the context of type theory. How do we know our type theory is the most true? Sure it allows us to prove lots of things, but that is a pragmatic measure. If type theory has pragmatic value, then our type systems should be measured pragmatically as well. Clojure actually wins in many respects because you get lots of monadic interfaces (the collection abstraction) that allow for reusuable code without the difficulty of the IO monad etc. This is not true in many other dynamic languages, e.g. Python.

                            So the “false dichotomy” is really apparent when you compare the monadic-ness of Python, C, Haskell, and Clojure. Clearly Clojure and Haskell fall into the “monadic” category and Python and C into the “non-monadic”. This “monadic-ness” distinction tells us more about how composable functions and data structures are than the “static” or “dynamic” distinction, which means that “static” and “dynamic” categories aren’t the most useful categories to put languages into.

                            1. 3

                              How do we know our type theory is the most true?

                              Is this really the question at stake? If a language tells me a variable is a certain type, I tend to believe it. Truth doesn’t seem to be an appropriate axis for evaluating type systems.

                              There’s definitely lots of variety regarding what a type system can tell you. The static/dynamic distinction is about when you can know the type information. Static languages allow you to know the types at compile time, whereas dynamic languages force you to wait until runtime.

                              1. 1

                                Is this really the question at stake? If a language tells me a variable is a certain type, I tend to believe it. Truth doesn’t seem to be an appropriate axis for evaluating type systems.

                                Within the context of your language, a variable has a type; this is the truthiness of that type. Within the context of type theory, the type system of that language has a certain truthiness to it. Within the context of the real world, type theory has a truthiness to it. The implied question in most static vs dynamic debates is, how true is my type system? Which begs the question, how true is type theory?

                                The answer is that it doesn’t matter. What matters: how useful is type theory generally? How useful is the specific type system I’m using? The static vs dynamic distinction doesn’t do much to help us answer this usefulness question. Understanding when types become relevant in a language definitely does help you, so I agree with you on that, but there are other more interesting aspects of type systems too.

                                1. 3

                                  Maybe it’s just me but I really can’t follow.

                                  Within the context of your language, a variable has a type;

                                  Sure, no qualms yet.

                                  this is the truthiness of that type.

                                  Completely lost. What is the truthiness? I don’t know what your pronoun “this” is referring to.

                                  I think I will continue to be lost until you can explain what it means for a type system to be false. “True” does not signify anything to me here.

                            2. 1

                              That is the most absurd thing I’ve read. Static typing is necessarily more restrictive because you have to express yourself in a way that can be verified by the type checker at compile time. Thanks to Godel, we know that the set of provable statements is a subset of all valid statements. Since dynamic languages do not attempt to prove correctness, they allow you to make many interesting statements that are impossible to make in a static language. Here’s a trivial example:

                              (eval ’(defn add-one [x] (inc x)))

                              (add-one 10)

                              You should also read this in depth rebuttal to the link you posted http://tratt.net/laurie/blog/entries/another_non_argument_in_type_systems.html

                              1. 14

                                That whole rebuttal rests on a conflation of dynamic types and static types. This is the standard stance for folks arguing from the dynamic camp (specifically, they’re two of the same sort of thing) and the opposite is so basic to the mental space of the static camp that it almost always goes unspoken.

                                In summary, if Bob’s article had explicitly stated that he was solely considering static expressivity… I would have agreed with it.

                                So, yes, Bob did not state that explicitly but it is taken without need for explicitness within static typing literature.


                                My take is that there are two “kinds of power” any formal language may be judged upon and that they are in tension. They are: the power to create and the power to analyze (deconstruct).

                                The more power to create a formal system affords the greater richness of expression exists and the more complex of “values” (whatever that might mean) can be constructed.

                                The more power to analyze a formal system affords the greater richness of semantics the values of the language have and the greater information can be extracted from each one.

                                Types are an alternative semantics to runtime evaluation. Thus, asking for types is asking for greater power to analyze and comes at a cost of power to construct.

                                From here, an argument must move on to tradeoffs between power to analyze and power to construct. Why wouldn’t you want to just side entirely with power to construct?

                                Most arguments of the static typing apologist end up being arguments for the value of power to analyze. Essentially, having more parallel semantic interpretations makes the system you’re working with more stable (fewer bugs, easier refactoring, partial verified documentation) and also opens up doors for other systems to exploit those other interpretations (typeclass resolution, servant, dependent types at large).

                                So which is better?

                                This is just a value judgement now. Nobody can answer for anyone else.

                                But I think that power to construct/power to analyze tradeoffs happen constantly so it’s a good concept to have an eye on.

                                1. 1

                                  I pretty much agree with what you’re saying, and that’s ultimately the tradeoff between static and dynamic typing. Depending on your situation one or the other might be preferable.

                                  1. 4

                                    I think an extension on this is that the technology already exists to make those tradeoffs locally within a single program. Haskell excels at this

                                    • the ability to embed DSLs and effect contexts lets you pick and choose this power tradeoff
                                    • the existence of the IO monad (as much as it is sometimes maligned) means that there’s an “escape hatch” to compare all of your more analyzable structures against
                                    • the existence of the Dynamic type as well as other “semi-dynamic” types like Json gives you opportunity for greater power at the cost of analyzability

                                    I think what’s most interesting is that the third point about is rarely explored. The real place where this exploration seems to happen is in row typing/structural typing a la Purescript or OCaml, but we could be building more and more sophisticated ways of working with the Json type without constraining its type.

                                    I think the lack of this development is why Haskell is really bad for exploratory data analysis, but it’s mostly the lack of exploration/development rather than a total failure, I believe.

                                    On the other hand, gradual typing systems also are an attack at the middle ground but I’d place a smaller bet on them. Ultimately, I think it’s easier to “forget” analytical power and regain constructive power than it is to go the other way. I’d be willing to put some money on this being a very fundamental logical tradeoff.

                                    So: where are the research projects for EDA in Haskell? I’d love to see them.

                                    1. 2

                                      While this is all true, the actual workflow is quite different than it is in a language like Clojure. A lot of the time I don’t know the solution up front, and I don’t know what the types are going to be in the end. It’s actually valuable to me to be able to work with an incomplete solution. With Clojure, I can use the REPL to explore the shape of the solution. I can also do a workflow that’s very similar to type driven development with Spec as seen here.

                                      Personally, I find that I generally want a specification at the API level, as opposed to having to structure all my code around types. For me, Clojure default is simply more ergonomic. Meanwhile, Spec provides me both with a sufficient guarantees regarding what the code is doing, and a meaningful semantic specification.

                                2. 3

                                  Any dynamic procedure can be implemented in any turing-complete static language; you just have to express your uncertainty about its runtime behavior in the type system. Even in a total language, you can build your entire program out of partial functions just by modeling that partiality with Maybe return values. Even in a pure language, you can build your entire program out of impure functions just by modeling that impurity with an IO monad or something similar. Even in a language with strong data types, you can write all the dynamically-typed code you want just by creating a large sum type of possible cases and using those overly-broad types everywhere (which will almost certainly require modeling some partiality as well). In general, you can write arbitrarily dynamic code if you’re willing to get very few useful guarantees from your type system. That may sound bad, but it’s no worse than writing in a dynamic language, where you get no static guarantees at all from your language (except maybe some very broad invariants about, for example, memory safety).

                                  1. 1

                                    And everything you can do in a language like Haskell, can be done using assembly. Yet, I think we’ll agree that ergonomics of writing assembly are not the same. It’s simply not interesting to discuss what’s possible in principle, it’s the actual workflow that the language facilitates that matters. The way you express yourself in a dynamic language is very different from the way you express yourself in a static one.

                            3. 7

                              I watched Rich’s talk a couple of times, and I think that positional issues can’t be dismissed. Even if you have record syntax for data, to my knowledge you don’t have this for types. Every time I pull up one of the more complex Haskell libraries, I first have to spend a bunch of time deciphering what I need to put in each position of the types. You end up having to rely on convention and hoping people don’t reorder.

                              named arguments are somewhat self-documenting and help with the debugging scenario as well.

                              I like that ADTs end up breaking all over the place in code when I change things, but I also like how my Python code and things likes dictionaries mean that I can work on objects by concentrating only on the parts that “matter”. It’s a tension, but I don’t think it’s a dicothomy and we can have solutions.

                              ADTs that represent objects (Money or Complex) are definitely of the kind where you want to reconfirm everything, but what about ADTs for configuration objects? Does adding another configuration parameter really require auditing everything? The canonical solution might be to decompose that a bit further to avoid this, then you run into the acretion problem. I’m writing wrappers upon wrappers for things.

                              It’s a shame that Rick decided to be so rant-y, because there were some valid points in there. The common ADT patterns force us down a very specific kind of static verification that end up shoehorning us into verbose patterns. I disagree about overall maintenance, but it does lead us to boilerplate.

                              1. 7

                                The issue with losing positional arguments in types is that it’s desirable to be able to talk about partial application without creating new type names (as equality in types gets more complex you run into hairy, very difficult problems quickly, so: if you solve partial application with aliases, how do aliased types equate?).

                                For instance, Scala has the worst of both worlds: positional types and very, very painful partial application.

                                With respect to your earlier statements though I agree a lot. ADTs are overly strict in that they represent a demand of both existence and completeness. Most Python idioms rely on an informal “structural subtyping” formalism (what people call duck typing sometimes) which is verrrry nice.

                                This works very well in the statically typed world: see OCaml or Purescript’s record types (and open variants).

                                1. 1

                                  Most Python idioms rely on an informal “structural subtyping” formalism (what people call duck typing sometimes) which is verrrry nice.

                                  I guess you’re referring to stuff like __iter__ and __str__ etc? It’s been a long time since I used Python, but I did like those “duck typed interfaces”.

                                  But did you know there’s something similar in Clojure, with “protocols”? :)

                                  1. 2

                                    I meant to point more at the heavy use of dictionaries in Python, though the more I think about it the less it seems like a clear example.

                                    Clojure really is one of the clearest examples. Idiomatic Clojure just involves passing dicts around and assuming you’ve got the right keys, hoping that there’s a solution (is there an intersection between the keys produced and the keys needed across all points in dataflow?). This is quintessentially “duck typing” and I think it’s a practice that’s well explored in the world of row types.

                                2. 2

                                  It’s a shame that Rick decided to be so rant-y

                                  How exactly was he ranty?

                              1. 27

                                I appreciate the detailed response and very thankful for the code changes regarding how thread deletion works. I do believe that having the ability to remove pin-pointed comments without whole threads is a better mechanism.

                                I am concerned how and where moderation is going. I asked yesterday on IRC:

                                21:16 < mulander> pushcx: is this your site or do we curate content as a community?
                                21:16 < mulander> if it's your site and your content than I have nothing more to say than to step down
                                21:16 < mulander> and just shut up.
                                21:17 < mulander> if we are moderating as a community then sometimes the moderation has to accept that a large portion of the userbase wants some content present
                                

                                to which you replied:

                                21:17 < pushcx> mulander: It's both.
                                

                                I don’t think ‘both’ works. With the last mod action we as a community exercised moderation transparency and I think that worked out fine as it did many times before. I do believe a site needs moderation but it should always be the last resort and I hope this site will not end up with yet another pamphlet that I will have to cross reference before posting an article or a comment.

                                1. 16

                                  I do believe a site needs moderation but it should always be the last resort and I hope this site will not end up with yet another pamphlet that I will have to cross reference before posting an article or a comment.

                                  “Moderation as a last resort” is - in my opinion - something that comes from a very narrow view of what moderation is. Moderation that only applies at the very last moment is bad moderation. It’s an ongoing process, which only rarely shows in technical moderator action like deleting complete or parts of posts.

                                  It can definitely be both. In the end, pushcx is the person willing to keep the lights on and to deal with all ramifications of running this site. I’m fine with that person being the final instance. That can definitely be both - there’s interactions between the person running the site and those willing to support, and in that interaction lies a lot of potential.

                                  1. 7

                                    “Moderation as a last resort” doesn’t preclude moderator intervention, it’s about having a gradient for how problem behavior is dealt with. I’ve been able to keep the number of people I had to ban in #haskell-beginners on Freenode IRC very low (only a couple occurrences) despite building a constructive, focused, and friendly community because I was present and responded to problems in ways other than banning people. It’s now one of the more peaceful and helpful IRC channels I’ve ever had the pleasure of participating in and it’s not so because I resorted to the banhammer every-time someone said something I felt was out of step with my goals for the community.

                                    1. 3

                                      Sure. The whole point of my post is that moderation is so much more then wielding the banhammer. “Moderation as a last resort” excludes that viewpoint, though, by focusing on only the technical details.

                                  2. 17

                                    Thank you sharing your concerns. And for bringing up this conversation, because I think there’s more worth talking about.

                                    I said “It’s both” because neither perspective can give a full understanding of Lobsters alone (or of any social site). I especially think it’s not only the first because no one can exercise dictatorial power over a voluntary community, everyone is free to leave at any time. And people have left in Lobsters’ history over the near-absence of moderation, mostly quietly. But there’s some maintenance and moderation that need a single person. I’ve been debugging log rotation and backups for the last week, I can’t post root’s ssh key for the community to take over the task. And less frequently, that means deliberately setting norms and expectations for the community, like that we need to prefer substantive counterpoints to dismissive repartee.

                                    I think aside from the confusing moderation log message I wrote, the biggest problem with that action was that it was unpredictable. Predictability is vital for effective moderation, and it’s clear from the reaction that I wasn’t. I’ve been working on updating the about page that has not seen much updating since Lobsters was much, much smaller and being vague was a virtue that led to the community experimenting and defining itself. I haven’t rushed to finish because I’m trying to take my time and think hard about what Lobsters has grown into the last five and a half years, and the challenges it faces as it continues to grow, rather than slap something up. Which… is what I did with a thoughtless moderation log entry.

                                    I agree and disagree with the idea that moderation should be a last resort. In a large community the little nudges I wrote about in this post are useful for avoiding Eternal September. But the large actions like banning users absolutely need to be a last resort after every other option has failed.

                                    And I share your fear of a site where opinions are so constrained that there might as well be a list of orthodox positions. We’ve had some wonderful conversations where people have disagreed about technical and even political topics, which is rare and valuable on the web. I hope to preserve and expand our ability to have those conversations. A pamphlet of required opinions would be an abject failure.

                                    1. 17

                                      And less frequently, that means deliberately setting norms and expectations for the community, like that we need to prefer substantive counterpoints to dismissive repartee.

                                      With the utmost respect for the work you put in and your contributions to the site, please do not use your moderator powers to try and shape the norms of the community.

                                      1. 11

                                        Could you point to communities where you think this has worked out particularly well? In the last few weeks I’ve been analyzing all the communities I’ve participated in or read substantially, and they’ve either been so small that everyone knows everyone or have moderators doing exactly this. (And it’s certainly been the case on the ones I’ve moderated.) But this could totally be personal style of what I think is a healthy community causing selection bias, and I’d love to break out of it if that’s the case.

                                        1. 12

                                          I could, but you might not agree with what I believe to be successful communities. That is why I ask that you don’t use your moderator powers to try and shape the community.

                                          You are already very influential within the community, so I feel that a lead-by-example approach is more appropriate and effective than trying to tailor the content of the site to what you feel the community wants.

                                          1. 15

                                            So, let’s just state an obvious examples of a “successful” community with low moderation: 4chan.

                                            A large part of Internet shibboleths come directly from there. A lot of really influential art and music and even code originated there.

                                            But, is it really worth it to wade through all of the garbage every day? Is it worth skipping every third post from some /pol/ idiot blathering on about white-supremacy? Do you really want to see yet another low-quality bait post about intel and AMD?

                                            Similarly, HN used to be fairly lightly moderated (and the current system has its flaws, Lord knows!). But a lot of just plain spam and garbage became cultural norms there: product posts, trivial tech news, politics, whatever.

                                            When reflecting on this problem, my advice would be: don’t only consider what moderation would censor, consider what no moderation would allow.

                                          2. 5

                                            https://lobste.rs/s/kmpizq/deleting_comments_instead_threads#c_uh4my1

                                            I successfully shaped the norms of #haskell-beginners without wielding a banhammer. Only a couple problem people have had to get banned in the channel since it started in May 2014.

                                            1. 4

                                              One thing to consider is the different audience sizes between a Haskell beginners IRC channel and a general technology link sharing website. What works for one might very well not work for the other.

                                              We’ve witnessed time and time again how the quality of gathering places went to shit as the audience size increased and TBH, I would love to find a place where this doesn’t eventually happen. If heavy moderation is a way to get there (these various other places always felt like places where only little to no moderation was happening), so be it.

                                          3. 1

                                            With the utmost respect for the work you put in and your contributions to the site, please do not use your moderator powers to try and shape the norms of the community.

                                            I don’t see where that was implied.

                                            1. 2

                                              I stated it pretty explicitly:

                                              And less frequently, that means deliberately setting norms and expectations for the community, like that we need to prefer substantive counterpoints to dismissive repartee.

                                              1. 3

                                                I was more at miss with the “using moderator powers” part. There’s so many more ways to shape norms.

                                                1. 4

                                                  I could’ve been clearer there. I was specifically referring to shaping the norms of the community by means that are not available to every other user - such as removing content.

                                        2. 4

                                          I hope this site will not end up with yet another pamphlet that I will have to cross reference before posting an article or a comment.

                                          I seriously doubt that will happen, and agree that I don’t want it to happen.

                                          And I think ‘both’ does work.

                                          1. 25

                                            wait, it has 17 upvotes (if one is to believe the archived version) and then got deleted?

                                            edit: and the “hate post” self-description was clearly sarcasm. even a non native speaker can see that. can we pretty please just use the voting system for moderation except for extreme cases (like, real hate speech)?

                                            1. 34

                                              Yeah, I’m not immediately sure how I feel about this. I agree that the comment was low-value, but I also haven’t traditionally felt that my feeling alone should be sufficient justification to delete, in part because others might disagree. That’s never been how lobste.rs does things.

                                              I do acknowledge that without the accidental recursive deletion, the impact would have been lower, and of course that aspect of it was a one-off.

                                              Now that the technical migration is done, the new leadership team should all talk at some point about moderation philosophy and get on the same page.

                                              1. 13

                                                why was it low-value? just because of the wording? the title said “minimal”, and that is at least a bit hazy in its meaning. so saying that electron isn’t minimal is a valid point in the discussion. even with a grain of sarcasm.

                                                1. 7

                                                  To me personally it was low-value because it took me a while to understand (might have been easier if I’d seen it while it was up and therefore the article’s subject matter in mind…), and because I didn’t feel that I got much out of it after putting in that effort. It was a valid and accurate criticism of Electron and of the article, without being a constructive one.

                                                  It’s certainly legitimate to express feelings about the article and about Electron, and I appreciate that many people have strong feelings on technical subjects, and I wouldn’t ask anyone to suppress those feelings. I don’t think it’s something that shouldn’t have been said. But if I’d personally said something this short I’d have expected to be downvoted.

                                                  My personal approach is that if I don’t have anything to add about how we got to this bad situation, or how we might get out of it, I just don’t say anything. This is out of respect for the time people spend reading this kind of remark, and with awareness that it takes time away from reading other pithy critiques. :) I do not consider it appropriate to enforce that on others though.

                                                  1. 1

                                                    My personal approach is that if I don’t have anything to add about how we got to this bad situation, or how we might get out of it, I just don’t say anything. This is out of respect for the time people spend reading this kind of remark, and with awareness that it takes time away from reading other pithy critiques.

                                                    If it comes in the form a one-line comment less than twenty words long, I think the dear citizens of Lobsters will be able to stomach having your opinion fly across their screen without much hazard, no matter how non-substantive it is.

                                                    1. 3

                                                      That’s fair. I guess I over-emphasized concern for others’ reactions: Only saying things I consider worth saying is mostly a thing I do for myself.

                                                2. 9

                                                  And, hopefully, have that moderation philosophy align with the people using the site!

                                                  1. 17

                                                    It does to be fair go in both directions to some extent, since moderation philosophies impact who you get on a site and vice versa. But it’s tricky here because it’s a change in moderation team. People signed up basically expecting the jcs+Irene brand of moderation, but it’s not clear the pushcx brand is the same as that one. I personally feel very comfortable with the previous two moderators, and if they wanted to become a bit more hands-on as the community grows, I wouldn’t be too worried, because I trust how they’ve moderated the site so far. But a new moderator becoming significantly more hands-on than the existing moderation team makes me more nervous.

                                                    1. 4

                                                      I can’t speak for pushcx; I’ve always considered that a constraint. I believe I’m on record with it, although I can’t find the comments right now.

                                                    2. 5

                                                      FWIW, I think that any shift in moderation philosophy isn’t necessarily bad - I just hope it’s something discussed openly as a meta post, considered thoughtfully, and implemented transparently. That transparency was one of the features that pulled many people here and I’d hate to see it change.

                                                      1. 4

                                                        It had a lot of value for me, it told me that it uses Electron, which I try to avoid. Just because something has low value for you does not mean it has low value for everybody.

                                                        1. 0

                                                          Yeah, I’m not immediately sure how I feel about this.

                                                          I am: a censor abused his powers. In a just world, he would be forced to step down and suffer with the rest of us mortals. Fortunately for him, this is not a just world.

                                                        2. 11

                                                          Final count according to the author was 23 and -4

                                                          1. 9

                                                            Upvotes are not necessarily a good way to judge a comment. People are herd animals, and it’s easy to upvote. There is a type of post that optimizes for “time taken” and “upvotes received:” the “zinger.”

                                                            1. 20

                                                              up/down votes are imho a clearly better moderation system than randomly deleting posts out of a mood.

                                                              1. 11

                                                                I don’t agree. Upvotes are very prone to herd movements and rarely express a useful policy in aggregates.

                                                                1. 7

                                                                  Since we’re in meta territory here: I’ve found that the score hiding feature at least seems to weed out some of the herd tendencies.

                                                                  Maybe we should look at adjusting the score visibility threshold up? Or keep the score hidden for a bit longer?

                                                                  1. 8

                                                                    maybe just don’t show the score except for the poster so the feedback is still there, but the herd effect doesn’t kick in

                                                                  2. 3

                                                                    but what’s a better alternative? at least with (down-)votes there is a feedback, maybe to better state a point via an edit. i always had the feeling the votes worked rather good here.

                                                                    1. 5

                                                                      This still doesn’t make them “clearly a better moderation system”. A mix of both is very usual and proven.

                                                                      1. 5

                                                                        This still doesn’t make them “clearly a better moderation system”.

                                                                        like i’ve said: “imho”, but i have felt as i typed “clearly” that it would be a point of criticism for some.

                                                                        A mix of both is very usual and proven.

                                                                        to quote myself:

                                                                        can we pretty please just use the voting system for moderation except for extreme cases (like, real hate speech)?

                                                              2. 1

                                                                can we pretty please just use the voting system for moderation except for extreme cases (like, real hate speech)?

                                                                And how is “real” “hate speech” defined? In reality, the term is just a catch-all excuse for censorship of various kinds.

                                                              3. 0

                                                                if this causes a “problem” in moderation lobste.rs is pretty much dead to me.

                                                              1. 10

                                                                Anyone interested in total languages might like Idris, Agda, or Coq:

                                                                In particular, some interesting approaches to services with an indefinite lifespan (like a daemon) were explored with codata in Agda:

                                                                1. 1

                                                                  Going to “Your Threads” seems slower now, probably database limited but I don’t know.

                                                                  1. 2

                                                                    It turns out the URL in the description is not for video linked from the heading. I was quite confused for a while there.

                                                                    1. 3

                                                                      Wondered when somebody would trip over the easter egg, sorry :)

                                                                      1. 2

                                                                        Once I figured out what had happened, I was amused, so no worries. :)

                                                                        1. 1

                                                                          I did and came back to the Lobster link thinking that there must be more to listen to. Great one indeed ;)

                                                                      1. 13

                                                                        @bitemyapp

                                                                        Lots of good and funny stuff in this video. I gotta smash one point, though.

                                                                        “consider it a moral imperative to live up to the economic value we’re extracting out of the companies we work at”

                                                                        Heck no, we shouldn’t! They don’t operate on any such morals. Their value is to get more while giving less in every deal they can. If that’s our system, then we should be doing the same. People wanting more morality should be working for increasing regulations or liability in reasonable ways in Washington. You know: arguing and lobbying to change the system like the rich and powerful software companies did to get their power and money. Alternatively, working at a non-profit or public benefit company that is legally required to produce benefits for the public. Being moral in dealings with such an organization would make sense. Focusing on utilitarianism with average company doing capitalism is like always doing the share option when opponents might steal in Golden Balls.

                                                                        https://www.schneier.com/blog/archives/2012/04/amazing_round_o.html

                                                                        Your later anecdote on Apple salaries is a good example. The company is screwing them over because it can. The company will market itself in such a way to convince people to work at that rate anyway. It’s acting solely in its self interest to maximize profit. Developers should do so, too, which should reduce the number of smart developers that work there. The companies might even respond to this by increasing pay or other perks/benefits as a differentiator. Some do this to a degree.

                                                                        “how many of you have the title ‘software engineer?’ How many of you are lying?”

                                                                        Probably all of them unless some Galois or Altran/Praxis people showed up. I know both have people doing formal methods in real-world software. Maybe if some from safety-critical industry (esp DO-178C) showed up we count them, too. Nancy Levison’s Safeware and those following such things come to mind. Those have to be systematic about correctness of design, implementation, and documentation. Maybe count people doing apps in logic, programming paradigm encoding all their assumptions, too. These are examples of kinds of people who might be called software engineers.

                                                                        Here’s what such processes look like:

                                                                        http://www.anthonyhall.org/c_by_c_secure_system.pdf

                                                                        http://www.methode-b.com/wp-content/uploads/sites/7/2012/08/ClearSy-Industrial_Use_of_B1.pdf

                                                                        http://www.mys5.org/Proceedings/2009/Wed/PDFs/(7)%20Bridging%20the%20Gap%20(Rockwell%20Collins).pdf

                                                                        http://compcert.inria.fr/compcert-C.html

                                                                        Most so-called “software engineers” can neither do that nor afford to try given the constraints of their work environment. Cleanroom and Design-by-Contract can often work cost-effectively but employers don’t care enough to push stuff like that for reasons in your talk. Assuming they’ve done enough research to even know they exist which is another problem in our immature profession. In any case, I knew the software profession was a joke by engineering standards when I saw actual software engineering like above done with its associated reduction in defects in development and maintenance phases. Developers don’t deserve to be called engineers except the rare, rare, rare few doing engineering.

                                                                        That doesn’t mean what they’re doing is necessarily bad given one should always do what works best in given environment. Develop, review, and test cycle with practice seems to allow us to write “good enough” software in general case. It’s just not engineering. We might create meaningful changes in market supply of developers vs engineers at different price points and process/tooling standards if we first get rid of the lie that the former are doing engineering.

                                                                        “medical professionals have to do for continuing education”

                                                                        I can confirm even tracking all the stuff in software assurance is by itself a lot of work. Then, there’s all the other sub-fields covering various attributes of software development. I track some of them. It’s like CompSci version of continuing education. Then, there should also be an expectation of trying to solve new types of problems with new tools to expand one’s mind. I support a CE paradigm for software engineers if we’re to use the label.

                                                                        1. 2

                                                                          They don’t operate on any such morals.

                                                                          The employer-employee relationship has nothing to do with what I’m talking about. I’m an advocate of programmers working from as strong a bargaining position as possible and of discussing salaries. The scope is broader but I didn’t want to stray too far from the core message in the talk.

                                                                          “how many of you have the title ‘software engineer?’ How many of you are lying?”

                                                                          Probably all of them

                                                                          Yes, that’s my point.

                                                                          Most so-called “software engineers” can neither do that nor afford to try given the constraints of their work environment.

                                                                          Which is why I want to grapple with those limitations by strengthening our economic position so that we can push back on strong managerial time preference but also improve how we work so that it’s more economic to Do The Right Thing.

                                                                          I can confirm even tracking all the stuff in software assurance is by itself a lot of work.

                                                                          I’m glad you’re tracking these fields but very few programmers are. Most I run into are struggling with whether to use Angular 2, Vue, or React.js.

                                                                          Glad you liked the talk, thank you for adding your thoughts. I think it does a lot of good to share how formal methods is being developed and applied.

                                                                          1. 1

                                                                            Oh, OK. Do you have another write-up on what you were talking about regarding employees giving their money’s worth and bargaining?

                                                                            1. 1

                                                                              Not as a blog post, usually something I discuss with programmers interpersonally.

                                                                        1. 1

                                                                          @bitemyapp The talk seemed to end rather abruptly, at least as shown in the Youtube video. Was that intentional, or just a consequence of something at the conference?

                                                                          1. 1

                                                                            I didn’t have a well formed coda beyond the exhortation that had preceded, so that was just where it ended, sorry :\

                                                                          1. 41

                                                                            Not for proving theories about […]

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

                                                                            I, for one, embrace having become a cyborg.

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

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

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

                                                                            Other good replies

                                                                            1. 16

                                                                              It makes the code more amenable to human comprehension

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

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

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

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

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

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

                                                                              1. 8

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

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

                                                                                1. 3

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

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

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

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

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

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

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

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

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

                                                                                  1. 4

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

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

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

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

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

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

                                                                                    1. 1

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

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

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

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

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

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

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

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

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

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

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

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

                                                                                      1. 2

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

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

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

                                                                                        1. 1

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

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

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

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

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

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

                                                                                          1. 2

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

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

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

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

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

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

                                                                                            1. 1

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

                                                                                  2. 17

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

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

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

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

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

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

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

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

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

                                                                                    1. 5

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

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

                                                                                      1. 12

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

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

                                                                                        1. 3

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

                                                                                          1. 0

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

                                                                                            1. 10

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

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

                                                                                              1. 1

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

                                                                                              2. 8

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

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

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

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

                                                                                                1. 2

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

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

                                                                                                    1. 2

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

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

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

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

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

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

                                                                                                      (~crossposted from hn thread)

                                                                                                      1. 2

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

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

                                                                                                        1. 3

                                                                                                          Very well; I eagerly await the studies then.

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

                                                                                                          1. 2

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

                                                                                                        2. 1

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

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

                                                                                                          1. 1

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

                                                                                                            1. 3

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

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

                                                                                                        3. 2

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

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

                                                                                                          1. 0

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

                                                                                                            1. 2

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

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

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

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

                                                                                                              1. 1

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

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

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

                                                                                                                1. 3

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

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

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

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

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

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

                                                                                                                  and do generative testing against it.

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

                                                                                                                  1. 2

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

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

                                                                                                                    1. 1

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

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

                                                                                                                      1. 2

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

                                                                                                                        1. 1

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

                                                                                                                          1. 3

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

                                                                                                                            1. 4

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

                                                                                                                    2. 1

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

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

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

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

                                                                                                            2. 2

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

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

                                                                                                              1. 0

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

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

                                                                                                                1. 1

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

                                                                                                                  1. 1

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

                                                                                                                    1. 2

                                                                                                                      Appears I misread your comment.

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

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

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

                                                                                                                      Ultimately, your formal specification can be wrong as well

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

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

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

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

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

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

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

                                                                                                                        1. 1

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

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

                                                                                                                          1. 1

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

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

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

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

                                                                                                                            1. 2

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

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

                                                                                                                              1. 1

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

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

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

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

                                                                                                                                1. 1

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

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

                                                                                                                                  1. 1

                                                                                                                                    Are you talking about languages like Coq here?

                                                                                                                                    No. Plain paper and pen proofs.

                                                                                                        4. 11

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

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

                                                                                                          1. 3

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

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

                                                                                                            1. 2

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

                                                                                                              1. 7

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

                                                                                                            2. 7

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

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

                                                                                                              1. 3

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

                                                                                                                1. 8

                                                                                                                  The thing you are missing:

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

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

                                                                                                                  1. 2

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

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

                                                                                                                    1. 1

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

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

                                                                                                                      1. 8

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

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

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

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

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

                                                                                                                        1. 1

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

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

                                                                                                                          1. 3

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

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

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

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

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

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

                                                                                                                        2. 4

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

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

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

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

                                                                                                                          Let’s just disagree on that.

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

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

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

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

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

                                                                                                                          1. 3

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

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

                                                                                                                        3. 7

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

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

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

                                                                                                                          1. 5

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

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

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

                                                                                                                            1. 1

                                                                                                                              Agree completely.

                                                                                                                        4. 5

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

                                                                                                                          1. 0

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

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

                                                                                                                            1. 14

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

                                                                                                                              Yes, but that is overly categorical.

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

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

                                                                                                                              1. 1

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

                                                                                                                                1. 4

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

                                                                                                                                  1. 2

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

                                                                                                                                    1. 3

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

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

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

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

                                                                                                                              2. 3

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

                                                                                                                                1. 1

                                                                                                                                  Please do elaborate.

                                                                                                                                  1. 3

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

                                                                                                                            2. 4

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

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

                                                                                                                              1. 5

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

                                                                                                                                1. 2

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

                                                                                                                                  1. 1

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

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

                                                                                                                                    1. 1

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

                                                                                                                                      1. 1

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

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

                                                                                                                                        Concretely, in some imaginary type system

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

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

                                                                                                                                          1. 1

                                                                                                                                            I don’t understand what you mean.

                                                                                                                                            1. 1

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

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

                                                                                                                                2. 2

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

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

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

                                                                                                                                  1. 0

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

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

                                                                                                                                    1. 3

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

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

                                                                                                                                      1. 1

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

                                                                                                                                        1. 4

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

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

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

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

                                                                                                                                          1. 0

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

                                                                                                                                            1. 5

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

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

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

                                                                                                                                              1. 0

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

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

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

                                                                                                                                                1. 2

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

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

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

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

                                                                                                                                                  1. 0

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

                                                                                                                                                    1. 5

                                                                                                                                                      Humans and computers have different strenghts:

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

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

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

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

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

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

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

                                                                                                                                          2. 3

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

                                                                                                                                            Here’s a well-typed program

                                                                                                                                            add3 x y z = x + y + z
                                                                                                                                            

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

                                                                                                                                            1. 1

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

                                                                                                                                              1. 2

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

                                                                                                                                                1. 1

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

                                                                                                                                                  1. 3

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

                                                                                                                                              2. 0

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

                                                                                                                                                1. 4

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

                                                                                                                                3. 2

                                                                                                                                  Have some thoughts on this, but first of all:

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

                                                                                                                                  That’s very rude of you.

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

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

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

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

                                                                                                                                  1. 3

                                                                                                                                    dynamic typing and static typing are not exclusive

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

                                                                                                                                    All dynamic typing means is that types exist at runtime.

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

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

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

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

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

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

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

                                                                                                                                    1. 3

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

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

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

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

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

                                                                                                                                      1. 2

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

                                                                                                                                    2. 3

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

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

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

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

                                                                                                                                      1. 2

                                                                                                                                        All dynamic typing means is that types exist at runtime.

                                                                                                                                        I’m not sure how this can be true:

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

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

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

                                                                                                                                        1. 1

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

                                                                                                                                          1. 2

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

                                                                                                                                            1. 2

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

                                                                                                                                              1. 2

                                                                                                                                                The definition is a literal quote from Pierce.

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

                                                                                                                                                1. 2

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

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

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

                                                                                                                                                  1. 2

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

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

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

                                                                                                                                    1. 2

                                                                                                                                      Here’s a question for the ages: are there any actually-existing good hosted CI providers out there?

                                                                                                                                      1. 7

                                                                                                                                        Not if you need speed: http://bitemyapp.com/posts/2016-03-28-speeding-up-builds.html

                                                                                                                                        I would honestly pay good money for reliable, tested deployment automation that stood things like CI up.

                                                                                                                                        1. 1

                                                                                                                                          Who’d you end up going with for the dedicated server / what are the specs on that machine like?

                                                                                                                                          1. 2

                                                                                                                                            Approximately this with NVMe RAID: https://www.ovh.com/us/dedicated-servers/infra/173eg1.xml

                                                                                                                                            tbqh, most the time we saved on compilation was lost to the GHCJS build later on. I was very sad.

                                                                                                                                        2. 5

                                                                                                                                          We use buildkite at my company. One nice aspect is that we get an agent to run on /our/ “hardware” (we just use large vm instances). It works pretty well.

                                                                                                                                          1. 3

                                                                                                                                            Another vote for buildkite here - their security posture is markedly better and you have much more control over performance.

                                                                                                                                            1. 2

                                                                                                                                              It’s probably worth mentioning here that GitLab offers similar functionality with their GitLab CI offering. You can use their infrastructure or install runners (their equivalent of agents) on as many machines as you like. Disclaimer: I haven’t used either yet but attended a meetup event where somebody praised them highly and ditched their Atlassian stack for that single reason.

                                                                                                                                              1. 1

                                                                                                                                                Their website looks intriguing could you elaborate on their security posture? Is it just an artifact of the on-premise build agent, or is there more to it than that?

                                                                                                                                            2. 5

                                                                                                                                              If you happen to run on Heroku, Heroku-CI works quite well. You don’t wait in a queue—we just launch a new dyno for every CI run, which happens while you blink. It’s definitely not as full features as Circle, or even Travis, but it’s typically good enough.

                                                                                                                                              1. 1

                                                                                                                                                At $WORK we run some things on Heroku but we can’t or don’t want to for most things — it’s either too expensive or the workload isn’t really well-suited for it.

                                                                                                                                              2. 4

                                                                                                                                                What do you need? I like Travis, they also get vastly better when you actually use the paid offering and they offer on-premise should you actually need it.

                                                                                                                                                1. 2

                                                                                                                                                  I need builds to not take 25-30 minutes.

                                                                                                                                                  Bloodhound averages 25 minutes right now on TravisCI and that’s after I did a lot of aggressive caching: https://travis-ci.org/bitemyapp/bloodhound/builds/286053172?utm_source=github_status&utm_medium=notification

                                                                                                                                                  Gross.

                                                                                                                                                  1. 2

                                                                                                                                                    I was asking cmhamill.

                                                                                                                                                    But, just to be clear: your builds take 8-14 minutes. What takes time for you is the low concurrency settings on travis public/free infrastructure. It’s a shared resource, you only get so many parallel builds. That’s precisely why I referred to their paid offering: travis is a vastly different beast when using the commercial infrastructure.

                                                                                                                                                    I also recommend not running the full matrix for every pull request, but just the stuff that frequently catches errors.

                                                                                                                                                    1. 3

                                                                                                                                                      I was asking cmhamill.

                                                                                                                                                      You were asking in a public forum. I didn’t ask you to rebut or debate my experiences with TravisCI. https://github.com/cmhamill their email is on their GitHub profile if you’d like to speak with them without anyone one else chiming in. I’m relating an objection that is tied to real time lost on my part and that of other maintainers. It is a persistent complaint of other people I work with in OSS. I’m glad TravisCI’s free offering exists but I am not under the illusion that the value they’re providing was brought into existence ex nihilo with zero value derived from OSS.

                                                                                                                                                      It’s a shared resource, you only get so many parallel builds. That’s precisely why I referred to their paid offering: travis is a vastly different beast when using the commercial infrastructure.

                                                                                                                                                      We use commercial TravisCI at work. It’s better than CircleCI or Travis’ public offering but still not close to running a CI service on a dedis (singular or plural).

                                                                                                                                                      I had to aggressively cache (multiple gigabytes) the build for Bloodhound before it stopped timing out. I’m glad their caching layer can tolerate something that fat but I wish it wasn’t necessary just to keep my builds working period.

                                                                                                                                                      That combined with how unresponsive TravisCI has been in general leaves a sour taste. If there was a better open source CI option than something like DroneCI I’d probably have rented a dedi for the projects I work on already.

                                                                                                                                                      1. 5

                                                                                                                                                        You were asking in a public forum. I didn’t ask you to rebut or debate my experiences with TravisCI.

                                                                                                                                                        You posted in a public forum and received some valid feedback based on the little context of your post ;)

                                                                                                                                                    2. 1

                                                                                                                                                      How long does it take on your local machine as a point of comparison?

                                                                                                                                                      1. 2

                                                                                                                                                        https://mail.haskell.org/pipermail/ghc-devs/2017-May/014200.html

                                                                                                                                                        That’s just build, doesn’t include test suite, but the tests are a couple more minutes.

                                                                                                                                                        1. 1

                                                                                                                                                          Hm, that’s roughly the time your travis needs, too?

                                                                                                                                                          https://travis-ci.org/bitemyapp/bloodhound/jobs/286053181#L539 -> 120.87s seconds

                                                                                                                                                          1. 0

                                                                                                                                                            Nope, the mailing list numbers do not include --fast and that makes a huge difference.

                                                                                                                                                            You are off your rocker if you think the EC2 machines Travis uses are going to get close to what my workstation can do.

                                                                                                                                                            1. 2

                                                                                                                                                              Would you rather pay for a licensed software distribution that you drop in a fast dedicated computer you’ve bought and it turns that computer into a node in a CI cluster that can be used like Travis?

                                                                                                                                                              Would you rather pay for a service just like Travis but more expensive and running on latest-and-greatest CPUs and such?

                                                                                                                                                              1. 3

                                                                                                                                                                Would you rather pay for a licensed software distribution that you drop in a fast dedicated computer you’ve bought and it turns that computer into a node in a CI cluster that can be used like Travis?

                                                                                                                                                                If it actually worked well and I could test it before committing to a purchase, probably yes I would prefer that to losing control of my hardware or committing to a SAAS treadmill but businesses loooooooove recurring revenue and I can’t blame them.

                                                                                                                                                                Would you rather pay for a service just like Travis but more expensive and running on latest-and-greatest CPUs and such?

                                                                                                                                                                That seems like a more likely stop-gap as nobody seems to want to sell software OTS anymore. Note: it’s not really just CPUs, it’s tenancy. I’d rather pay SAAS service premium + actual-cost-of-leasing-hardware and get fast builds than the “maybe pay us extra, maybe get faster builds” games that most CI services play. Tell me what hardware I’m actually running on and with what tenancy so I don’t waste my time.

                                                                                                                                                    3. 1

                                                                                                                                                      Has anyone done this kind of dependency scan on Travis that this guy did on CircleCI? I suspect you will see much the same.

                                                                                                                                                      Travis does have one clear advantage here in that it’s OSS so you can SEE its dependencies and make your own decisions. See my note about CircleCI needing to be better about communication above.

                                                                                                                                                      1. 3

                                                                                                                                                        Well… “scan”. They posted a screenshot of their network debugger tab :).

                                                                                                                                                        Travis (.org) uses Pusher, but not their tracking scripts. It integrates Google Analytics and as such, communicates with it. ga.js is loaded from google.

                                                                                                                                                        The page connects to:

                                                                                                                                                        • api.travis-ci.org
                                                                                                                                                        • cdn.travis-ci.org (which ends up being fast.ly)
                                                                                                                                                        • gravatar.com (loading avatar images)
                                                                                                                                                        • statuspage.io (loading some status information as JSON)
                                                                                                                                                        • fonts.googleapis.com (loading the used fonts)
                                                                                                                                                        • ws.pusherapp.com

                                                                                                                                                        All in all, it is considerably less messy then circle-ci’s frontend.

                                                                                                                                                        Also, Travis does not have your tokens or code in their web frontend, code is on Github, tokens should be encrypted using the encrypted environment: https://docs.travis-ci.com/user/environment-variables#Defining-encrypted-variables-in-.travis.yml

                                                                                                                                                        1. 2

                                                                                                                                                          You have proven my point perfectly.

                                                                                                                                                          CircleCI’s only sin here is one of a lack of communication. There is nothing actually wrong with any of the callouts the article mentions, they just need to be VERY sure that their users are aware of exactly who is seeing the source code they upload. This should be an object lesson for anyone running a SaS company, ESPECIALLY if said SaS company caters to developers.

                                                                                                                                                          1. 4

                                                                                                                                                            This is not an apples to apples comparison, in my post I cited Javascripts only (which can make AJAX requests and extract source code), @skade cites that Travis loads fonts, images, and CSS from third party domains, which don’t have those properties; a compromise in CSS might change the appearance of a page but generally can’t result in your source code/API tokens being leaked to a third party.

                                                                                                                                                            As far as I follow the only external Javascript run by Travis CI is Pusher. So, no, it has not proven your point perfectly, in fact it demonstrates the opposite.

                                                                                                                                                  1. 2

                                                                                                                                                    Nice work mate. The only thing that stood out to me was defining updateMap when insertWith exists and would be more efficient by avoiding the member lookup first.

                                                                                                                                                    1. 1

                                                                                                                                                      Thank you! I stared at insertWith and ruled it out for some reason. Ended up resorting to updateMap which I wrote for a different blog post. I wrote this while streaming (2 hours and change). I’ll upload the video if this noise reduction filter doesn’t make the audio sound watery this time.

                                                                                                                                                      Update: good catch, I’ve fixed it and replaced it with insertWith

                                                                                                                                                    1. 2

                                                                                                                                                      Fernand Braudel’s A History of Civilizations

                                                                                                                                                      Watt’s Echopraxia (not enjoying this as much as Blindsight)

                                                                                                                                                      1. 2

                                                                                                                                                        If you like Braudel you will probably also like DeLanda’s books: https://en.wikipedia.org/wiki/Manuel_DeLanda

                                                                                                                                                        1. 3

                                                                                                                                                          FWIW Stack should be getting an official OpenBSD release soon, https://github.com/commercialhaskell/stack/issues/3313 which should reduce the amount of faffing about required.

                                                                                                                                                          1. 2

                                                                                                                                                            ByteString isn’t a string, it’s a sequence of bytes analogous to how other languages use arrays of bytes.

                                                                                                                                                            1. 1

                                                                                                                                                              ByteString is a string (of bytes, not characters)

                                                                                                                                                              1. 2

                                                                                                                                                                :i Data.String.IsString agrees, but I’m quite confident that /u/bitemyapp is aware of that, and was pointing out that ByteString is intended for lower level purposes.