1. 3

    I don’t want to stop anyone creating or signing any oath they like, but if I were to sign one with an “honest and moral work” clause then I’d want to be sure that my fellow signers agreed with my view on what comprises moral work.I’m pretty sure that most people here would disagree on which of the following fall under that banner:

    • Creating an ad server that uses supercookies
    • Building a mashup of airbnb, uber and tinder data
    • Writing robocall software for the GOP
    • Writing a cryptocoin miner in javascript
    • Creating a website to hook Ohmibod users up with patrons
    • Writing firmware that misreports emissions data when a car undergoes regulatory testing
    • Writing an Android app to teach bump stock modifications
    • Adding password decrypt into your service to allow SRE to diagnose user account problems
    • Creating a query interface for a database of racial profiles
    • Writing a “find my nearest abortion clinic” app
    • Employing machine learning during hiring to predict amount of time candidates will take off from work for medical reasons
    1. 1

      Well said, this is the biggest problem with the oath as it stands. Oaths like these aren’t supposed to just say, “Hey, be Good,” but are supposed to help define what Good looks like. This is especially true when you have a profession like ours where the creation of a software artifact is so far removed from the circumstances in which it might be used.

    1. 6

      I really need to get around to writing my sum type proposal for Go.

      Instead of introducing an entirely new feature, the idea is to tweak the existing features to support it.

      The bare idea is simple: “closed” interfaces. If you declare an interface as closed, you pre-declare all the types that belong to it, and that’s it. The syntax could be something like

      type Variant1 struct {..}
      type Variant2 struct {..}
      type Foo interface {
          // methods
          for Variant1, Variant2
      }
      

      You continue to use type switches (i love type switches) with these interfaces, except that the default case can’t be used for exhaustive switches (you can also enforce that in non-exhaustive switches).

      It would also be nice to lift the restriction for implementing methods on interfaces; and make it be possible to run interface methods on explicitly-interface (not downcasted) types. There was a proposal for that too..

      Under the hood, these could possibly be implemented as stack-based discriminated unions instead of vtable’d pointers, though there might be tricky GC interaction there.

      I haven’t really written this up properly, but I suspect it might “fit well” in Go and be nicer than directly adding sum types as a new thing.

      1. 4

        I encourage you to make this suggestion on https://github.com/golang/go/issues/19412 which was recently marked as “For Investigation” which suggests someone is collating ideas.

        1. 2

          +1, that’s an excellent thread with a lot of interesting insights about the constraints that the core language devs are battling with when introducing a new feature like this. It’s super long but I’ve found the discussion to be really informative.

          1. 1

            I actually just wrote https://manishearth.github.io/blog/2018/02/01/a-rough-proposal-for-sum-types-in-go/ yesterday

            But I don’t have the time/desire to really push for this. Feel free to use this proposal if you would like to push for it!

        1. 3

          This looks racy to me, can someone explain where I’m going wrong?

          Thread A is the first to acquire the benephore, checks and increments the atomic variable, finds it is zero and proceeds without acquiring the semaphore.

          While Thread A is in the critical section Thread B arrives and acquires the benephore, finds the atomic variable to be non-zero so acquires the semaphore. Because it has the semaphore it proceeds into the critical section. Now there are two threads concurrently in the critical section.

          What prevents this scenario?

          1. 3

            I think you’re right, unless I’m missing something obvious.

            Worse still, if T1 enters the critical section and is followed by T2, if T1 now makes progress it will find benaphore_atom > 1 and call release_sem() on a semaphore it doesn’t hold. Which is probably either a crash or UB, who knows.

            I was missing something obvious.

            The semaphore, is initialized into an ‘unavailable’ state.

            When Thread B attempts to acquire the newly initialized semaphore, it blocks as the semaphore is in its ‘unavailable’ state. Thread A later finishes up in its Critical Section, and seeing that benaphore_atom > 1 it increments the semaphore, allowing Thread B to make progress.

            At the end of this execution, T2 sees !(benaphore_atom > 1) and continues without marking the semaphore as available.

            1. 1

              Semaphores don’t provide mutual exclusion.

              You use them to e.g. count the number of items in a queue and wake up enough threads to process them. Then those threads use a separate mutex to synchronise any operations on the queue.

            1. 3

              Nope. It’s 2017, it’s time to stop parsing strings with regular expressions. Use structured logging.

              No thanks! I’ll stick to strings.

              1. 2

                Could you please explain why? Your comment, as it is, is not bringing any value.

                1. 1

                  Not the OP but here’s why I don’t like structured logging

                  • logs will ultimately be read by humans and extra syntax gets in the way.
                  • structured logging tends to bulk the log with too much useless information.
                  • most of the use cases of structured logging could be better handled via instrumentation/metrics.
                  • string based logs can be emitted by any language without dependencies so every system you manage could have compatible logging.

                  Arguably a space separated line is a fixed-schema structured log with the least extraneous syntax possible.

                  1. 6

                    To me (in the same order):

                    • logs are ultimately read by human once correctly parsed/sorted. Which means that it should be machine readable first so that it can be processed easily to create a readable message.
                    • Too much informations is rarely a problem with logging, but not enough context is often an issue.
                    • Probably, but structured logging still offers some simpler ways for this.
                    • You just push the format problematic from the sender (that can use a simple format) to the receiver (that has to parse different formats according to what devs fancy)

                    To me the best recap on why I like structured logging is: https://kartar.net/2015/12/structured-logging/

                    1. 2

                      most of the use cases of structured logging could be better handled via instrumentation/metrics.

                      Speaking as a developer of Prometheus, you need both. Metrics are great for an overall view of the system and all its subsystems, but can’t tell you about every individual user request. Logs tell you about every request, but are limited in terms of understanding the broader system.

                      I’ve wrote a longer article that touches on this at https://thenewstack.io/classes-container-monitoring/

                1. 2

                  Another approach is to do neither and avoid exposing properties at all, especially ones where you’re just getting another object to operate on (i.e. Law of Demeter). The pattern was written up as Tell Don’t Ask at https://pragprog.com/articles/tell-dont-ask

                  1. 4

                    Postings for previous revisions: 1 2. And a related story. As long as I’m linking, my comment on one became a blog post, and I especially like the post @screwtape linked on standardizing errors.

                    1. 2

                      (off-topic) in your blog post the quote from “RFC 760, Jan 1980” seems to have some copy/paste noise in the middle of the last sentence.

                      1. 1

                        Thanks, I fixed it.

                      2. 1

                        Ah, thanks for the links. Damn changing URLs make it tricky to spot a duplicate with a simple search :(

                        1. 1

                          A repost is just fine, especially with it being a new version.

                      1. 10

                        I don’t understand at all why so much arguing happens over code of conduct pages on projects. Don’t be a fuckin dick to each other, nerds. How is that hard, and how is that hard to enforce?

                        1. 33

                          it happens because some folks know they are dicks and they stick up for other dicks. If you’re working on something alone you can be as much of a dick as you want, but if you’re working on a team it’s pretty fucking reasonable to have some ground rules that everyone agrees on.

                          1. 10

                            If you read any deployed CoC, they’re vastly more overbearing than “don’t be a dick”. If a CoC was literally those four words, I would support it wholeheartedly, but it never stops there.

                            I also disagree that every social interactions needs explicit rules. I don’t really feel the impulse to codify social interaction. If someone is being a dick, I will respond according to the situation rather than preemptively trying to bring playground-style rules into the mix.

                            1. 15

                              People come from different backgrounds and cultures where one set of behaviours might be socially acceptable, so yes - sometimes, it needs to be spelt out.

                              1. 14

                                How does this work when the power dynamic is working against the person who is harassed? What if the harasser is a star contributor or friend?

                                Hasn’t “don’t be a dick” been historically insufficient?

                                1. 5

                                  Not sure how the code of conduct changes that. If the high council of conduct adjudication are the ones doing the harassing, what happens then?

                                  1. 20

                                    If the high council of conduct adjudication are the ones doing the harassing, what happens then?

                                    That is part of the reason why this situation is so contentious; that’s what’s happened here.

                                  2. 4

                                    Hasn’t “don’t be a dick” been historically insufficient?

                                    Yes if there’s good management or moderation that actually care about the work above the politics. If they value politics more, then it’s not sufficient since they’ll protect or reward the dicks if they politic correctly. The leadership’s priorities and character are almost always the most important factor. The rest of the benefits kind of spread as a network effect from that where good leadership and good community members form a bond where bad things or members get ejected as a side effect of just doing positive, good work or having such interactions. I’ve seen so many such teams.

                                    Interestingly enough for purposes of CoC’s and governance structures, I usually see that break down when they’re introduced. I’m talking governance structures mainly as I have more experience studying and dealing with them. The extra layers of people doing administrative tasks setting policies can create more trouble. Can, not necessarily do since they reduce trouble when done well. Just the indirection or extra interactions are a risk factor that causes problems in most big projects or companies. A good leader or cohesive team at top keeping things on track can often avoid the serious ones.

                                  3. 4

                                    If it wasn’t broadly worded, it’d be harder to aim at the people we don’t like.

                                    1. 18

                                      If it wasn’t broadly worded, it would be easier to abuse loopholes in order to keep being a dick within the letter of the CoC.

                                      The things are broadly worded for a reason, and it’s not “to enforce it arbitrarily”.

                                      1. 4

                                        Is that more of a real or hypothetical concern? Any examples of a project that adopted a code of don’t be a dick, then a pernicious dick couldn’t be stopped, and the project leadership threw up their hands “there’s nothing to be done; we’re powerless to stop his loopholing.”?

                                        1. 7

                                          Boom, you said it. I’ve usually seen the opposite effect: people make broad rules specifically to attack or censor opponents by stretching the rules across grey areas. Usually, the people surviving in projects of multiple people due to “loopholes” are actually there for another reason. As in, they could be ejected if they were so unwanted but whoever is in power wants them there. Those unstated politics are the actual problem. In other cases, the rules were created for political reasons, often through internal or external pressure, rather than majority of active insiders wanting them there with enforcement pretty toothless maybe in spite. The OP and comments look like that might be the case if they voted 60% against getting rid of this person.

                                          Also, I noticed the number of people and their passion on these “community enforcement” actions goes way up with most of them not being serious contributors to whatever they’re talking about. Many vocal parties being big on actions to control or censor communities but not regularly submit content or important contributions to them. I’m noting a general trend I’ve seen on top of my other claim rather than saying it’s specific to Node which I obviously don’t follow closely. Saying it just in case anyone more knowledgeable wants to see if it’s similar in terms of people doing tons of important work in this project cross-referenced against people wanting one or more key contributors to change behavior or disappear. If my hypothesis applies, there would be little overlap. The 60% number might give indicate unexpected results, though.

                                          EDIT: For broad vs narrow, just remembered that patent trolls do the same thing. They make the patents broad as possible talking up how someone might loophole around their patent to steal their I.P.. Then, they use the patent to attack others who are actual contributors to innovation asking them to pay up or leave the market. Interesting similarity with how I’ve seen some CoC’s used.

                                          1. 4

                                            Yeah that’s what I don’t get. If someone was being a jerk on a project I was on I wouldn’t think twice about banning them once they’ve proven they’re a repeat offender.

                                            1. [Comment removed by author]

                                              1. 2

                                                Do codes help or hinder such agreement? Those I’ve seen applied have largely been counterproductive, as their definition of dickery has not aligned adequately with the wider project community’s.

                                            2. 2

                                              node.js could serve as an example.

                                              1. 5

                                                Of the opposite? A code of don’t be a dick doesn’t work in theory because there’s no agreement. So node has this nice long list of banned behaviors and remedial procedures, but what good has that done them? Meanwhile it seems everyone agrees Rod was being a dick, so if the code were that simple it’d be a fine deal.

                                                I mean, I don’t really know what’s going on since it’s all wrapped in privacy, but the more complicated the rules the more likely it is someone will play them against you. Better to keep it simple.

                                                1. 10

                                                  Part of having a CoC is enforcing a CoC. Yeah, the CoC doesn’t mean much if it isn’t enforced, but that’s not an argument against codes of conduct. By anology: the fact that people break laws isn’t an argument against the rule of law.

                                                  1. 2

                                                    Right, but if a law didn’t bring any clarity to the community - if it wasn’t clear who was and wasn’t breaking it, or it wasn’t able to be enforced consistently, or it was applied consistently but still seemed to be capricious in who it punished and who it didn’t - then it would be a bad law. The criticism isn’t that this “Rod” broke the CoC, it’s that the CoC didn’t seem to help the community deal with his behaviour any better than it would have without the CoC, indeed possibly worse.

                                                    (my general view, particularly based on seeing them in the Scala world, is that CoCs as commonly applied are the worst of both worlds: they tend to be broad enough to have decent people second-guessing everything they say, but specific enough that less decent people can behave very unpleasantly without obviously violating the code)

                                        2. 2

                                          “don’t be a dick”. If a CoC was literally those four words, I would support it wholeheartedly, but it never stops there.

                                          Sorry bro^Wsibling, it’s not diverse enough. It would have to say “Don’t be an asshole” to be gender-inclusive.

                                          As for the CoCs working, I think it’s unreasonable to expect bad people to turn good because a file was committed into the git repository saying they should.

                                          Maybe something like a Code of Misconduct is even more important than the CoC. The link is for IRL events, and quite obvious, but online the escape hatch is to gtfo.

                                          1. 2

                                            Interesting. Didn’t know he wrote on that topic. He made some interesting points but oversimplified things. I think Stephanie Zvan has some good counterpoints, too, that identified some of those oversimplifications with a lot of extra details to consider. Her focus on boundaries over democratic behavior or tolerance reminded me of a video someone showed me recently where Kevin Spacey’s character argued same thing with appeal to a more mainstream audience:

                                            https://www.youtube.com/watch?v=sFu5qXMuaJU

                                            She’s certainly right that a focus on boundaries with strong enforcement can create followers of such efforts and stability (conformance) within areas they control. Hard to say if that’s idea versus the alternative where other folks than those setting the boundaries also matter.

                                            Edit: Read the comments. Lost the initial respect for Stephanie as it’s the same political dominance crap I argue against in these kinds of threads. The contrast between her style/claims and Pieters’ is strong and clear.

                                      2. 5

                                        Don’t be a fuckin dick to each other, nerds.

                                        Upvoted for this. Without actual decency, a CoC can only make the semblance of decency last for so long.

                                        1. 4

                                          People disagree vehemently about what it means to be a dick so that guideline is useless.

                                        1. 3

                                          I think the effects of this are being overblown. I’m perfectly happy running uBlock Origin everywhere, and that’s unlikely to change any time soon. Heck, I don’t even use Chrome as my primary browser on any device anymore. There’s multiple high quality browsers available on most platforms, so if you’re unhappy with one browser you can just switch to another that matches your requirements.

                                          1. 12

                                            The existence of alternatives does nothing for publishers if people don’t use them. Which empirically they don’t. The Chrome integration means if your ads don’t get the blessing of the Coalition for Better Ads then your ad revenue just got cut in half.

                                            1. 2

                                              Maybe if your service can’t sustain itself without scummy ads then people don’t value it as much as you think.

                                            2. 3

                                              Here is the unabridged list of common Chrome users, the fiftyish percenters, who care about ad oligopolies and privacy:

                                              (Now it might not seem like an overblown effect… Think of how huge Chrome is and how insanely huge the FB- and Google-driven ad space is.)

                                              1. 2

                                                Just to piggy back on this comment - my company (which manufactures a product) only advertises through Facebook and Google. We have partnerships with other businesses and stuff, but I don’t think that falls into the realm of “buying ad space”.

                                            1. 1

                                              Excellent advice in this article.

                                              1. 0

                                                I think the reason for doing this is more about jurisdiction than language. Google and the like need to know which country’s jurisdiction you are in so they can remove search results that courts have required them to. Potentially there are data protection laws that may affect how they track you that differ from country to country. Google maps shows different borders depending on your country etc.

                                                1. 4

                                                  I’m in complete agreement. The fixation with keeping your hands cramped on the home row needs to end. It’s 2017 and there is more to programming than typing. More than half my coding time is spent reading and exploring code. More than half of the remaining time spent thinking about the problem. Of that remaining typing time only a fraction is entering new code, the rest is refactoring and extending existing code.

                                                  For most of those tasks a mouse is simply faster. I don’t want to think about counting the number of words or letters I want to highlight or subselecting underscores with a regex. I just want to point and drag the text, with multiple cursors if need be. If I want to jump to the definition of a function I take 50ms to move my pointer there and ctrl+click. I don’t want to be forced to navigate line by line, word by word to get to the function name before jumping to its definition. The great thing is that with sublime/code/atom/gedit/geany/scite I get the best of both worlds and can use the right control for the situation.

                                                  1. 3

                                                    Relative line numbers genereally removes most of the hassle for me, using my mouse is generally a cognitive shift that makes it harder for me to stay concentrated

                                                    1. 5

                                                      I really like relative line numbers, but the actual line number on the line with the cursor. set rnu and set nu together does this in vim.

                                                      1. 1

                                                        using my mouse is generally a cognitive shift that makes it harder for me to stay concentrated

                                                        I’ve never been able to understand this sentiment. I’m currently a user of probably the most mouse-heavy editor ever invented but even when I was an emacs/vim user, I never understood the complaint here.

                                                        I’m wondering if it’s just a difference in development approach: the majority of my time isn’t spent writing code, but thinking about it - I tend to get most fussy about having a large, clean whiteboard with ultra fine tip markers.

                                                        When I do need to edit a large section of code, I find that the combination of structural regexes and sweeping a selection with the mouse is about as close to perfection as you can get. Much nicer than mucking about with line offsets or setting marks.

                                                        Not saying anything is wrong with it - I just find it very interesting that I can’t even relate to such a commonly held opinion. I’ll have to look around to see if there’s been any research done on this.

                                                        1. 1

                                                          My problem is that it feels jarring, but then maybe acme, not being a weird hybrid like most programs and jnstead being actually pointed towars efficient use of the mouse, does not feel like that, I’ll have to try it out

                                                      2. 1

                                                        I generally move by screens or “paragraphs” (ctrl u/d, {}) when doing that kind of stuff, and use visual mode liberally. Refactoring and stuff like that is when vim feels noticably awesome. Typing in new code you could be using word.

                                                        1. 1

                                                          I agree, see my other comment in this thread for a super rough demo of what i imagine might be a cool extension to these somewhat basic editors.

                                                        1. 2

                                                          In Go, you import packages by URL. If the URL points to, say, GitHub, then go get downloads HEAD of master and uses that. There is no way to specify a version, unless you have separate URLs for each version of your library.

                                                          This is a criticism of the go get tool, not Go in general. You can easily specify any version you like by checking it out in $GOPATH using git/svn/whatever. go get is just a convenience for quickly getting started with a package.

                                                          1. 3

                                                            This is a criticism of the go get tool, not Go in general.

                                                            It’s a criticism of the Go ecosystem. If the response to that criticism is “yes, but you can use general tools to manually manage package installation instead of using the tools provided by the ecosystem”, then it sounds like a valid criticism.

                                                          1. 1

                                                            But if your static analyzer can find the same problem, what’s the advantage?

                                                            1. 19

                                                              You know that everyone else in the community is also using the same static analyzer.

                                                              1. 1

                                                                But your static analyzer will also work across all the community code you compile into your program.

                                                                1. 16

                                                                  What do you do when it just fails, though? That’s a lot of vendored code to bugfix and a strong potential to lack the buy-in to do it. If the analyzer is just built-in to your compiler… that all evaporates.

                                                                  1. 0

                                                                    So we go from (a) “my new programming language solves a serious programming problem not solved by your old tatty one” to (b) “my new programming language bundles its solution to the problem into the compiler and your old tatty one has the solution in a standard tool”. To me, at least, (a) is a stronger argument than (b)

                                                                    1. 8

                                                                      Do you know of a static analysis tool for C and/or C++ that is simultaneously meets the following requirements?

                                                                      • Soundness: All memory-unsafe code is rejected.
                                                                      • Modularity: Modules can be analyzed and verified in isolation. Never do the implementation details of two or more modules have to be analyzed simultaneously.
                                                                      • Inference: Things that can reasonably be inferred will be inferred, to keep the annotation burden down to a tolerable level.

                                                                      That’s what it takes to compete with Rust.

                                                                      1. 3

                                                                        Soundness: All memory-unsafe code is rejected.

                                                                        Doesn’t Rust permit unsafe operation?

                                                                        Modularity: Modules can be analyzed and verified in isolation. Never do the implementation details of two or more modules have to be analyzed simultaneously.

                                                                        That’s an impressive feature. Composable properties is a tough problem. For example, if module A requests 55% of available heap and Module B also requests 55% the system (A;B) will fail even though both modules are “correct” on their own. Same with scheduling and timing or even mutual exclusion which is painfully dangerous. Does Rust mutex support solve the compositionality problem? Or am I misunderstanding what you wrote?

                                                                        1. 1

                                                                          Doesn’t Rust permit unsafe operation?

                                                                          Sure, but you have to explicitly request it. One good way to think of it is that Rust is actually two languages: safe Rust and unsafe Rust, and the keyword unsafe is the FFI between them. The relationship between safe and unsafe Rust is similar to that between Typed Racket and Racket: when things “go wrong” (language abstractions are violated), it’s never safe Rust or Typed Racket’s fault.

                                                                          That’s an impressive feature.

                                                                          It’s a feature of most type systems. For example, when you type check a C source code file, you don’t need access to the implementation of functions defined in other files. Though, of course, you might need to know the interfaces (prototypes) exposed by those functions.

                                                                          Does Rust mutex support solve the compositionality problem?

                                                                          It doesn’t. Rust is modest in what it tries to prevent. In particular, safe Rust doesn’t even try to prevent deadlocks. It only prevents issues that can be expressed in terms of “use after free” or “data races”.

                                                                          1. 1

                                                                            Ok, so what you mean by “ Modules can be analyzed and verified in isolation” is limited to type safety.

                                                                            1. 2

                                                                              Compositional verification happens to be a feature of most type systems, but there’s no law of nature preventing you from devising your own non-type-based compositional analyses.

                                                                              1. 1

                                                                                Maybe there is a law of nature. Discrete state systems are hard.

                                                                          2. 1

                                                                            Doesn’t Rust permit unsafe operation?

                                                                            This is actually a very good point and one that was raised with regards to Haskell many-a-time.

                                                                            What I wonder about is how to present some kind of debuggability around that – maybe there can be some kind of breadcrumb that indicates when a crash occurs, that it was in an unsafe operation?

                                                                        2. 6

                                                                          I agree, but I’m also pretty directly claiming that as far as “solving the problem” goes there’s a big gap between language-integrated solutions and “aftermarket” ones, even if they enjoy wide community adoption. In one case, the problem has actually vanished. In the other, there’s a means to tackle it if you want to spend the energy.

                                                                          1. 3

                                                                            A language is not just a spec but also a community and an ecosystem. If we’re comparing between “Rust” and “C with foo analyzer”, questions like “which has more libraries?” and “which is easier to hire for?” have quite different answers to when we’re comparing “Rust” and “C”.

                                                                    2. 2

                                                                      What is the state of the art for static analysis of C/C++? You can (fairly sure) find this kind of code and prohibit it entirely, but is it possible to allow it and make guarantees about its safety?

                                                                      I would have thought not, but I don’t really know that much about static analysis… Is it possible within some constraints? (For constraints that lie somewhere between “don’t ever allow this kind of code” and the constraints that Rust applies via the language.)

                                                                    1. 2

                                                                      Everyone should use Source Code Pro I think. Includes powerline symbols now, etc. And it’s just prettier.

                                                                      https://github.com/adobe-fonts/source-code-pro

                                                                      1. 2

                                                                        And it’s just prettier.

                                                                        Good that beauty is in the eye of the beholder.

                                                                        1. 2

                                                                          Does it contain a gopher? :)

                                                                          1. 2

                                                                            Monospace font for programming? Never! I use Lucida Grande for my text editor, a proportional font.

                                                                          1. 16

                                                                            The parts of your program that don’t have interesting names are the least interesting parts of your program.

                                                                            1. 6

                                                                              It’s best to make your program as boring as possible, that way it’s more likely to be correct.

                                                                              1. 7

                                                                                Can you see how that does not contradict what I wrote?

                                                                                1. 3

                                                                                  Looks like it just follows on: the parts of your program that don’t have interesting names are the least interesting parts of your program, so make your program as boring as possible…

                                                                                  1. -1

                                                                                    Technically correct statements that carry misleading implications are not a very productive contribution to the discussion.

                                                                                    1. 5

                                                                                      What is the misleading implication?

                                                                                      1. 1

                                                                                        That the parts of your program that don’t have interesting names are irrelevant to your program’s quality.

                                                                                        (I mean you evidently seemed to think you’d mislead me, given your condescending first reply)

                                                                                        1. 2
                                                                                          1. Being “least interesting” does not imply irrelevant to quality. I don’t see how one implies the other.

                                                                                          2. My first reply was a genuine question. I’m sorry you sensed condescension.

                                                                              1. 6

                                                                                “Read it as: If the property Q holds for all values of type T, then if every object of type S maps to exactly one object of type T, the property Q holds for all values of type S.”

                                                                                iow if: if S is a subset of T then every property of element of T is also a property of elements of S

                                                                                In other words, a subset is a subset.

                                                                                As far as I can tell, this is elementary school algebra, with a bunch of silly terms added. The original results in formal logic are kind of interesting, but what do we learn about programming here? I don’t see it - which may just mean I’m not seeing it.

                                                                                1. 9

                                                                                  Two things make it interesting

                                                                                  1) We’re dealing with types, not sets, so set-based intuition can be a guide but doesn’t always hold 2) OO types sometimes behave really weirdly

                                                                                  In particular, in an OO system you can implicitly treat any value of a type s : S as if it were a type T so long as S is a subtype of T. This creates a map, as we’re asking for, letting us consider each value s : S as if it were a value of T—as we ask.

                                                                                  Unfortunately, this mapping may not always convey all of the properties we’re interested in. LSP warns about this and says we ought to be careful. In particular, it’s up to us to ensure that all supertype coercions respect all possible properties of the supertype. That’s not obvious.

                                                                                  1. 3

                                                                                    I think the whole concept of type hierarchy is dubious - it’s an attempt to simplify too much.

                                                                                    What I did not like about the posting, however, was that it tossed around terms from logic and category theory as if they were obviously significant in programming, and yet the use of those terms seemed limited to making some simple stuff appear complicated and perhaps also making some complex stuff appear solved. What do we know more about programming or programs after we invoke a lot of vaguely correlated terms from foundational logic and category theory? I don’t see any additional insight.

                                                                                    1. 2

                                                                                      What I did not like about the posting, however, was that it tossed around terms from logic and category theory as if they were obviously significant in programming…

                                                                                      Type theory (which more or less exists to discuss programming) draws a lot on category theory and logic, not just set theory. That’s the link.

                                                                                      1. 2

                                                                                        So, what do you think of this one from Meyer?

                                                                                        http://se.ethz.ch/~meyer/publications/proofs/top.pdf

                                                                                        I thought it was interesting in that it had simplified, but usable, models of all sorts of things in programming expressed with elementary set theory. It’s clean enough that a non-formal methodist like me can follow a lot of it. I also have a bunch of papers in my collection using FOL or set theory to build CA’s, certifying compilers, automated proving, etc. So, I’d like a logic experts opinion on it whether it’s worth further research or development given how it models foundations of programming easy for both people and computers to get.

                                                                                        1. 3

                                                                                          I don’t get how it is “usable” - and I’m not saying that as a way of saying it is not usable, it’s that I read these things and don’t see how all that apparatus produces any insights or assurance.

                                                                                          1. 1

                                                                                            Appreciate the feedback. :)

                                                                                            1. 3

                                                                                              sorry for being so terse. I get why it’s useful to think of a (um) program as a map or relation from states to states, but once you get further down into that explanation, it seems to just restate programming language concepts in a clumsy special notation.

                                                                                              1. 1

                                                                                                Ok. That’s more helpful. Im just surveying opinions on some of this niche work. More interesting one so far was Hehner’s Formal Methods of Software Design. Quite a few liked that.

                                                                                                The embedded folks are prefering model-driven stuff with code generation to SPARK or statically-checkable C. Rockwell-Collins has a nice toolchain that ties together Simulink, provers, SPARK, and AAMP7G.

                                                                                                So, I just dig up stuff like this to run it by diverse crowds of pro’s to see what they think is worth passing onto specialists in CompSci wondering what to tackle or improve.

                                                                                      2. 2

                                                                                        The Liskov substitution principle is as much of a logical triviality with types as it is with sets. And the following corollary is also a triviality: Absent any laws governing how methods can be overridden (an object-oriented counterpart to Haskell’s type class laws), the real meaning of a non-final method in a non-final class is simply undefined.

                                                                                        Yet most object-oriented programmers still define APIs full of non-final methods without associated laws. This is why we need to restate the Liskov substitution principle over and over.

                                                                                        1. 2

                                                                                          Maybe I miss the point, but the Liskov substitution principle seems to me to indicate that type hierarchies are too simple minded. Squares are obviously a type of rectangle, but operations on rectangles that are closed in the set of rectangles are not necessarily closed on squares. What’s the problem? The problem comes up because there is a desire to allow all methods defined for rectangles to be applied to squares, but that seems like an odd idea. All odd numbers are numbers, but doubling an number produces a number, while doubling an odd number takes us out of the set. So what?

                                                                                          1. 2

                                                                                            Squares are obviously a type of rectangle, but operations on rectangles that are closed in the set of rectangles are not necessarily closed on squares. What’s the problem?

                                                                                            The problem is that object-oriented programmers call Rectangle and Square classes whose instances don’t quite behave like rectangles or squares. Mathematical objects don’t “adjust themselves” in response to method calls. If you perform an operations on a mathematical object, what you get is another mathematical object (unless the given object happens to be a fixed point of the given operation, of course). If you could actually define types of rectangles and squares, rather than pointers to some memory blob whose current state happens to contain the parameters of a rectangle or square, you’d see how beautifully Square is a subtype of Rectangle.

                                                                                            1. 3

                                                                                              This is what I don’t get. If you perform x times 2 on an odd number, you get an even number. That’s why we use groups, rings, fields, etc. to capture the notion of a set with a collection of operations. If you increase the length of a pair of sides on a square, you get a rectangle. These are both mathematical objects, but the operation: increase length of parallel sides is not closed for “squares”. I am undoubtedly missing the point, but to me it seems like the difficulty here is that the abstraction of a type hierarchy is wrong. The reason one might want to inherit rectangle is code reuse. That makes sense. Shouldn’t we really be asking: does subtyping efficiently reuse code, not is the subtype closed under all type methods? In Liskov’s paper, one issue she brings up is aliasing - where an object “square” is also an element of “rectangle” so you could apply a rectangle operation unaware. But that seems like the real problem: if I constrain a type, shouldn’t the language at least complain if I evade the constraints?

                                                                                              1. 2

                                                                                                These are both mathematical objects, but the operation: increase length of parallel sides is not closed for “squares”.

                                                                                                Right, it has type enlarge :: Number -> Rectangle -> Rectangle (where the number specifies by how much the length of parallel sides must grow), but not Number -> Square -> Square. However, if you get your subtypes right, you can pass a Square to enlarge, and while the output isn’t guaranteed to be a Square, it’s guaranteed to be a Rectangle.

                                                                                                I am undoubtedly missing the point, but to me it seems like the difficulty here is that the abstraction of a type hierarchy is wrong.

                                                                                                Type hierarchies are totally fine. The problem is what types you’re putting in the type hierarchy. What an OOPer calls a Rectangle (resp. Square) is actually a mutable cell whose state can be interpreted as the parameters of a rectangle (resp. square). A Haskell programmer would call such things IORef Rectangle (resp. IORef Square). Haskell doesn’t have subtyping, but you can obviously write a function upcast :: Square -> Rectangle. And a very naïve form of the Liskov substitution principle can be expressed: contramap upcast :: Predicate Rectangle -> Predicate Square. However, you can’t lift upcast to another function of type IORef Square -> IORef Rectangle, because IORef isn’t a Functor. This is why logic provides insight about computation.

                                                                                                1. 1

                                                                                                  Well, I’m glad that gives you some insight about computation, but I have no idea what it could be.

                                                                                                  1. 2

                                                                                                    In this particular case: a mutable cell containing a rectangle isn’t the same thing as a rectangle, thus you can’t expect properties of rectangles to apply to mutable cells containing rectangles. Phrased this way, it’s an utter triviality, but apparently most programmers won’t see the obvious.

                                                                                          2. 2

                                                                                            It is logically trivial with types, but to state it one must accept that the notion of subtype isn’t as obvious as it is with sets. If you use set intuition you’ll skip right over the interesting misconception since it’s been so thoroughly hammered out.

                                                                                        2. 2

                                                                                          Half-agree and half-disagree. You correctly note that the Liskov substitution principle is a triviality. It holds in any type safe language with subtyping: Java, OCaml, etc. However, believe it or not, not everyone understands this! For example, many, perhaps most object-oriented programmers think they can somehow “break” the Liskov substitution principle by overriding in a derived class a non-abstract method from a base class. Here’s the classical example:

                                                                                          class Animal {
                                                                                              public void makeNoise() { System.out.println("generic noise"); }
                                                                                          }
                                                                                          

                                                                                          After reading this snippet, many programmers conclude that:

                                                                                          (0) If animal is an Animal, then animal.makeNoise() produces a generic noise.

                                                                                          But then we show them the following snippet:

                                                                                          class Dog extends Animal {
                                                                                              public void makeNoise() { System.out.println("bark"); }
                                                                                          }
                                                                                          

                                                                                          And then they conclude that:

                                                                                          (1) Dog is a subtype of Animal.

                                                                                          (2) If dog is a Dog, then dog.makeNoise() doesn’t produce a generic noise.

                                                                                          After putting the pieces together, the only thing we can conclude is that we just broke the Liskov substitution principle. But, wait, didn’t I just say that the Liskov substitution principle always holds? Where did we go wrong?

                                                                                          1. 1

                                                                                            I thought the classic example was a type hierarchy that has a square as a subclass of a rectangle since it is a “special type of rectangle that happens to have equal sides”. It violates LSP since a square cannot be substituted for a rectangle in some situtations such as when the width and height are being varied independently.

                                                                                            1. 3

                                                                                              The problem is that you’re wrongly relying on names to determine the meaning of your types. Just because your classes are called Rectangle and Square, it doesn’t automatically mean that their instances actually behave like mathematical rectangles and squares.

                                                                                        1. 2

                                                                                          philosophical question, who do you pay back technical debt to? I think this is where the analogy breaks down. Ward Cunningham invented the term to explain what his engineering team was doing to a bunch of finance people. While the analogy may have made sense to said finance people, it makes less sense to me.

                                                                                          I prefer the idea of entropy instead of technical debt.

                                                                                          1. 7

                                                                                            Your (future) self. We often speak of living on borrowed time, even though there’s no time bank from which to borrow time. Possibly alternately phrased as the devil always gets his due.

                                                                                            The financial metaphor is very accurate. It’s all about time value. Having a feature today can be worth much more than the cost of building it twice over the long term.

                                                                                            1. 1

                                                                                              I don’t think it is that simple. What about when you leave the org? Maybe the org owns the debt? Who does it get the debt from? Itself? What about when the org fails, does the debt disappear? Maybe they open source it and the greater society takes on the debt? Does the debt have an interest? Usually you have to conciously acknowledge taking debt. How often do you find engineers decide consciously they are taking on “technical” debt? Debt typically has a schedule for payback, does technical debt have a schedule?

                                                                                              It’s not that simple.

                                                                                              1. 1

                                                                                                The debt is like a lien against the code. As the owner of the code today, you get to make the decision to incur debt. When you leave and give the code to somebody else, they get the debt too.

                                                                                                No, technical debt doesn’t require sitting down with a loan officer and filling out forms in triplicate and waiting for approval.

                                                                                                1. 2

                                                                                                  BRAINWAVE: securitizing technical debt. GET ME A16Z, this bad boy isn’t going to last!

                                                                                                  1. 1

                                                                                                    Now you are getting into some classic religious territory about debt to the universe type stuff. We have a lien against the code which we borrowed from the gods.

                                                                                              2. 4

                                                                                                My favourite metaphor is a comparison to either a legal system or a tax code.

                                                                                                As a society evolves, laws are re-written and supersede (parts of) previous laws, but the old laws aren’t usually retracted explicitly. The legal system becomes more complicated to interpret and reason about in general over time. Each legal document or law often references other clauses elsewhere as exclusions or edge-cases, requiring you to read or be familiar with those other parts in order to make sense of the document you’re interpreting. Anyone who has done taxes in the US knows how difficult it can be to work within complex tax codes.

                                                                                                It is possible to aggregate and “compress” the effective laws or tax code into a simplified and revised set of documents that would bee less ambiguous, easier to interpret/change, and which read mostly linearly. Refactor it, if you will.

                                                                                                1. 2

                                                                                                  Does it really break the analogy? How much does the other party matter? I suppose in theory it’s possible to renegotiate the terms of your real-world debt, but how often is that an actual concern for the business?

                                                                                                  I think entropy is a worse analogy in many respects. It suggests an inevitable law of nature rather than a choice, and that’s to the people to whom it suggests anything at all.

                                                                                                  1. 1

                                                                                                    I think it is more accurate because typically you have to consciously take on more debt. While most developers don’t even acknowledge they are taking any “debt”. Often many decisions are not conscious. It’s more like an inevitable law of nature you are fighting. And if you don’t fight it you die.

                                                                                                  2. 1

                                                                                                    To me, entropy carries the sense of inevitability and so removes the sense of it being worthwhile to oppose it.

                                                                                                    I prefer the debt metaphor since you are borrowing some effort from the future to have something today. If you are lucky you can write it off and have nothing to pay back.

                                                                                                    1. 1

                                                                                                      You are fighting entropy just by being alive. Life IS about fighting entropy. And yes death is inevitable.

                                                                                                  1. 9

                                                                                                    Still need to zoom images on mobile if you want to see any details.

                                                                                                      1. 2

                                                                                                        I have my doubts – some serious concerns, actually – about the value of that password checker.

                                                                                                        I put in five words, randomly chosen from a dictionary, with spaces between them. It generated a very mediocre score: 56%. I was under the (possibly mistaken?) impression that randomly selecting five words from a dictionary would be an excellent password. (Corrections welcome.)

                                                                                                        In addition, I wouldn’t want anyone to be encouraged to enter any of their real passwords on a web site like this, as it could very well use that information maliciously. I’m not saying this particular web site does this, but I don’t think putting passwords into “password checker” web sites is something we generally want to encourage people to do.

                                                                                                        1. 4

                                                                                                          How big was your dictionary? It’s actually fairly easy to compute how many passwords a given generation scheme can produce.

                                                                                                          For example, my /usr/share/dict/words has 99,171 words in it. Picking five at random (without replacement) with cat /usr/share/dict/words|sort -R|head -n 5|tr $'\n' ' ' allows for (99,171 choose 5) different passwords, which is 79,927,903,812,879,014,029,704, or about 76 bits or 13 case-sensitive alphanumeric characters. (Choosing with replacement makes for a significantly easier to calculate but only marginally bigger 83 bits/14 characters.)

                                                                                                          I generated a couple of 13-character alphanumeric passwords and got an average score between 80 and 90, and a couple of five-word passphrases, which mostly got 100, so that seems in line to me. However, it heavily penalizes passphrases that consist entirely of lowercase letters and space, and my dictionary has lots of proper nouns and possessives. Filtering those, the passphrase scores were much worse—50-60-ish. (Interestingly, a 5-word passphrase generated from this shorter dictionary—66,005 words—is still worth a 12-character password. This is why experts advise you to concentrate on length over alphabet/dictionary size.)

                                                                                                          So it’s safe to say this checker isn’t consistent with the actual amount of entropy in a given password. But it looks like it’s trying to penalize the sorts of habits that result in bad passwords, even if that results in a very skewed “good” password space. It’s much more important to it that “password1” get a bad score than that “signals constriction punchy rejoinders titanic” get a good one. I’m not sure it’s biased in the best way (“signals constriction etc.” is far more likely to be remembered and used than the otherwise-equivalent “8inHpcw47jUdD”), and I don’t think I’d recommend it for that reason, but the premise is probably sound.

                                                                                                          1. 4

                                                                                                            Well, let’s do the math. According to a quick search there are about 171,476 words in current usage–that’s about 2^17.387647.

                                                                                                            So, assuming that you pick each word at random and allow duplicates, getting your password is:

                                                                                                            P(5word_pass) = 1/171476 * 1/171476 * 1/171476 * 1/171476 * 1/171476
                                                                                                            P(5word_pass) = ( 2^-17.387647 ) ^ 5
                                                                                                            P(5word_pass) = ( 2^-86.938235 )
                                                                                                            

                                                                                                            So, we’ll setup the same trick using uppercase letters (26), lowecase letters (26), digits (10), and other characters (33). So, at random, we can choose a character from those sets, and that’s a 1/95 chance of any particular character being picked.

                                                                                                            Let’s see how many characters we need to match the 5-word password!

                                                                                                            P(5word_pass) = ( 2^-86.938235 )
                                                                                                            ( 2^-86.938235 ) = (1/95)^N
                                                                                                            ( 2^-86.938235 ) = (2^- 6.569856)^N
                                                                                                            ( 2^-86.938235 ) = 2^(- 6.569856N)
                                                                                                            -86.938235 = -6.569856N
                                                                                                            N = 13.232898
                                                                                                            

                                                                                                            And to double check:

                                                                                                            (1/95) ^ 13.232989 = 6.7422567e-27
                                                                                                            2^(-86.948235) = 6.7422567e-27
                                                                                                            

                                                                                                            So, it looks like you’d have to use about 14 characters from that class defined above to get the same strength as 5 dictionary words.

                                                                                                            1. 1

                                                                                                              Intriguing that 5 random words be roughly equivalent to a 14 character password. The space of 5 word memorable phrases that most people will choose is going to be quite small in practice so for my family I need to reinforce the idea that they should choose random words, e.g. by flipping through a book.

                                                                                                              Of course, the search space become much bigger if they also include proper nouns.

                                                                                                              1. 2

                                                                                                                they should choose random words, e.g. by flipping through a book.

                                                                                                                People are terrible at “choosing” randomly. They’re going to pick words they like and discard words they don’t.

                                                                                                                1. 2

                                                                                                                  That’s why it’s called “diceware” ;) The EFF recently created a list of words to use for creating passwords like this, and then you use dice to pick a word for you.

                                                                                                                  we recommend a generating a six-word passphrase with this list, for a strength of 77 bits of entropy.

                                                                                                                  https://www.eff.org/deeplinks/2016/07/new-wordlists-random-passphrases

                                                                                                        1. 1

                                                                                                          If they’re not going to use a password manager then using lots of words is probably the best you’re going to do. You can mix it up a little by throwing some numbers or symbols in there and varying the capitalization.

                                                                                                          It also helps if they use some non-dictionary words in there. But nothing that’s easy to remember for humans is going to be as good as a bunch of random characters including non-alphanumeric.

                                                                                                          1. 1

                                                                                                            A potential attacker would have to assume that a 30 character password could contain any characters. If that’s true, having 30 lowercase letters is as secure as 30 mixed case or 30 with numbers and symbols?

                                                                                                            1. 2

                                                                                                              I think the concern is dictionary based brute force attacks. People love talking about entropy with regards to password strength, but I think that ignores search space. A long passphrase has very high entropy on a per-character basis, but a memorable series of lowercase words chosen from common vocabulary (not a dictionary) is more likely to be attempted first before a similar length string with special characters. Another thing that I think complicates the discussion is whether you’re protecting against login attempts, hash cracking (from a credential db leak), or a targeted attack that may have already obtained a passphrase you use elsewhere. Different patterns and recommendations tend to focus on addressing one or more of these concerns, but any strategy requiring memorization (no password manager) will compromise on these. All that is to say a long passphrase is good, but a long passphrase with some special characters is even better at guarding against one type of attack.

                                                                                                              1. 1

                                                                                                                You should consider attack vectors. If you have a list of all known usernames like say a forum has a directory of users, then my first attack would be to try every known username against common passwords like password, password1, hunter2, Password, dog, etc.

                                                                                                                Another attack vector is you know the user you want to compromise, so you try potential passwords like names of family, friends, significant things in their life. You can open it up to just all English words, then vary that by special characters trying some leet speak substitutions.

                                                                                                                In summary, I’m just saying that an attacker knows the total solution space is gigantic, but could also assume some basic human nature that were lazy so we make passwords easy and memorable. An attacker might be able to exploit this and reduce their search space enough to have a feasible attack.

                                                                                                                1. 1

                                                                                                                  Why would they have to assume that? Especially knowing that XKCD has made series of words passwords popular. Plus, you don’t know how long a password is based on its hash.

                                                                                                                  Seems like a totally reasonable attack vector nowadays to me to just randomly assemble the most common couple thousand words.