1. 8

I’m working on two projects in my spare time right now:

-going through Type-Driven Development With Idris, to learn Idris for the dependent-types goodness

-trying to teach myself the nuts and bolts of type theory by implementing Hindley-Milner type checking in the toy programming language interpreter I’ve been working on for a while. I’ve found a few resources about exactly how to go about doing this (most notably, this Haskell conference talk and this section from Stephen Diehl’s incomplete tutorial on implementing a Haskell-like functional programming language. I’ve actually had a bit of trouble translating the code from those resources, which is in Haskell and assumes a particular design for the AST data structures, to my own interpreter, which is in Rust and has a different AST design. If anyone is knowledgeable about actually implementing Hindley-Milner in a real programming language, I’d love to get some advice.

1. 4

I’ve got that book sitting in front of me right now! It’s so cool how you can specify protocols and valid state transitions so nicely in idris! I’m fantasizing about using it as the basis for a smart contract language.

1. 4

I tried going through that book, too, but I was not convinced by the examples it used. I recall one example which added the runtime length of an array to the typesystem. Nice, but you still needed do (runtime) checks for the length…

1. 2

You don’t always need to do runtime checks for the length. For example, if the length of a vector is n you can use a data type Fin n to represent an index. If you ask a user for an input, you’ll have to check it there - but once you have a Fin n you can pass it around your program without checking it. It’s always a valid index.

2. 1

If anyone is knowledgeable about actually implementing Hindley-Milner in a real programming language…

I have experience with doing it in Haskell, but it seems like you’re implying that Haskell is not a real programming language…

1. 1

Haha far from it, I’ve written ostensibly-useful code in Haskell myself. There are a number of impedence mismatches between Haskell-style code and Rust-style code, that have made it hard for me to take the example Haskell code I’ve seen for Hindely-Milner and apply it to my own project.

1. 3

I’ve been working on a toy porgramming language implemention for a while, and I’ve been eagerly awaiting this section of Crafting Interpeters to be published, becuase creating my own bytecode interpreter is one o the many substeps of a PL implemention that I don’t fully grok. Thanks munificent for working on this book (and please try to get Ch 15 out quickly so I can read it too :) )

1. 3

Yes it’s great to see this. What other books cover bytecode interpreters?

Most compiler textbooks don’t appear to cover the subject? As far as I remember the Dragon Book covers a “three address code”, but it’s more of an IR to compile down to assembly, not a stack machine.

I found this article interesting – it has a very compact style:

https://codewords.recurse.com/issues/seven/dragon-taming-with-tailbiter-a-bytecode-compiler

1. 1

Thank you! Hopefully the next chapters won’t take quite as long. The past couple of months had a much greater number of personal life… things… than usual.

1. 2

Maybe another way to think about this is “Can I not do FP in my language?”. Yes for JavaScript and Scala and Rust - you can write procedural code to your heart’s content in these languages, even if JavaScript gives you the tools to use functional abstractions and Scala and Rust actively encourage them. No for Haskell and Elm - there’s no way to write code that looks imperative in these langauges.

1. 9

No for Haskell and Elm - there’s no way to write code that looks imperative in these langauges.

main = do
name <- getStr
putStrLn "Hello, " ++ name  1. 5 No for Haskell and Elm - there’s no way to write code that looks imperative in these langauges. What do you mean by “looks imperative”? Doing everything inside the IO monad is not much different from writing a program in an imperative language. 1. 2 You mean StateT and IO. And then learning how to use both. 2. 3 Writing Haskell at my day job, I’ve seen my fair share of Fortran written in it. The language is expressive enough to host any design pathology you throw at it. No language will save you from yourself. 1. 8 For some reason I’ve picked up Blender and went through a real nice set of tutorials (armed with this awesome cheatsheet). Will try to keep up the pace of just building random things in Blender I’ve gotten a bit burned out on tech-y stuff recently, so opting for drawing and the like for my free time. I’m not good but it’s still relaxing and satisfying. 1. 4 Nice! I’ve played around with Blender some myself, and have been meaning for a while to learn it more thoroughly. I really enjoy Blender Guru’s tutorials. 1. 10 Yeah, it did. And that’s unfortunate, because the ability to interact with a remote computer graphically as easily as you can with ssh would have been very useful. “Most people only ever interact with remote machines with either text mode SSH or a browser talking to a web server on the remote machine.” says the article, and indeed a web browser talking to a server on the remote machine is basically how one interacts with a remote computer graphically nowadays. This is wildly popular, of course, but is it the best possible world? Probably not. 1. 5 If you want to do that, RDP is actually well implemented and works for such purposes, on the Windows side. 1. 6 Unfortunately, there are a lot of “RDP hostile” applications these days – many of them from Microsoft themselves! For example, using Skype for text chat over RDP is quite painful now. 1. 1 Not only on the Windows side. FreeRDP is very good too. 1. 11 It’s a good story, but the headline (just copied from CBC, not av’s fault!) is entirely wrong. Computer code didn’t put people in jail. An oppressive government put people in jail. 1. 1 I think both interpretations could be correct. The laws of the regime are wholly unethical, so I agree blame lies mostly with the government. But the Gülenists who created the link back to bylock did so knowing that innocent (in the eyes of the law) people might be incarcerated under the laws of the regime. The authors are partly culpable. Of course, “Oppressive regime throws innocents in jail” isn’t going to get as many clicks. 1. 1 This is an excellent point. I’m not a Turk myself, but I hate Erdogan and the Islamist political views he represents. If Turkey were within my sphere of immediate political concern (rather than a country I have no particular connection to), I could easily see myself supporting the coup attempt itself, let alone a communications app connected with it. So seeing people legally exonerated for doing something that I think ought to be completely legitimate brings me no joy. For an analogy closer to home, imagine that this article was about people trying desperately to prove that they were being falsely accused of using was Gab, because their jobs were at stake. 1. 3 Great writeup that’s answered some questions I’ve had myself about tokio, since its not a problem domain I have much experience with but gets a lot of discussion in rust-related fora. 1. 9 Harry Potter nad the Methods of Rationality - fiction and the title says it all. Unsong - fiction which is quite hard to describe without spoiling it. Gödel, Escher, Bach: An Eternal Golden Braid - explores how recursion and self reference can create complex behaviour. And I also highly recommended Metamorphosis of prime intellect mentioned by Hobbes. 1. 4 I would also recommend Unsong (United Nations Subcommittee On the Names of God). The premise is that the arcane rules of the Kabbalah system of Jewish mysticism became manifest in the world in 1968, when the members of the Apollo 8 mission read from scripture while orbiting the moon. In the present day, there are various groups seeking to use or abuse Kabbalistic mechanisms as the laws of physics slowly collapse around them. Would recommend to anyone with a programmer’s appreciation of rule systems, or anyone who likes Jewish thought. 1. 2 YAY GEB: The Eternal Golden Braid! I’m 3/4 of the way through it now. What a ride! 1. 1 I spent about a month reading it (I was out of work and did little else for the month). I could split my life experience into the time before, and the time after, reading GEB. 1. 3 I want to know about the people who don’t follow everybody else, like sheep. Who were the most down voted? 1. 5 I don’t actually think this means what you think it means, at least if people are using down votes the way I’d like to see them used. For me, a down vote means “This has no place here”. 1. 3 At least on HN and TrueReddit, which I think share your (and my) preference for how downvotes should be used, downvotes seem to be abused to reflect disagreement maybe 2/3rds of the time. It’s a shame, but seems inevitable. 1. 4 Exactly. Sometimes I also think people view downvoting as their way of saying “feh” to someone whose ideas they somehow disapprove of or deem unworthy. IMO such a disagree/disapprove downvote is a major cop out. Either reply and explain yourself or upvote someone who’s already done so that you disagree with. 1. 4 If people can up-vote without having to post a reason, what is wrong with down-voting without posting a reason? There are lots of reasons for down-voting, including “This has no place here”. 1. 5 Arguably we should have the mechanism to document reason for upvotes. But, downvotes without reasons are a malfeature. That mechanisms encourage the level of discourse one finds at HN and Reddit. We at least attempt to do better. 1. 3 Because in my view, the system here is designed to measure merit. If I think an article is interesting or useful, I upvote it. If I don’t, I simply leave that article alone. No negative action is required. We DO need a mechanism for keeping what’s posted here in line with the kind of thing the community wants to see, and that’s where I see down votes coming in. Think of Lobsters as a bar graph, with the most voted for articles bubbling to the top and generating the longest bar. 2. 1 At least on HN and TrueReddit, which I think share your (and my) pref People can disagree on what things constitute that which has no place here 1. 1 TrueReddit What’s that? 1. 2 https://www.reddit.com/r/TrueReddit/ (Don’t use it myself.) 3. 2 I deliver niche content, thank you! I’d have piles of funding by VC’s and on Kickstarter if I stayed on popular topics in popular places. I imagine some others, too. Most of us are here on this specific forum for stuff better for the brain, though. ;) Far as most downvoted, it’s gotta be that libertarian fellow: I’m often expanding their comments to see exactly what was said. Usually just some ideological repetition but every now and then a good counterpoint. 1. 1 How about having a count of our yearly total up/down votes, with an option to make them public? 1. 1 I’d almost rather limit the number of downvotes that people can cast in a given time period to remind people that a downvote is more censure than disagreement. 1. 1 I think a limit on both up/down would be good. It would certainly make me spend more time considering whether a link really was worth an up-vote. 1. 1 I dunno. I think upvotes should be easy, downvotes should require due consideration. 1. 13 A person I know who was active on Twitter around 2010 said that he felt at home with the geeky culture on twitter then, and regrets the loss of that culture as twitter became more mainstream and politically relevant on an international scale. I suspect that some of the homey feeling of mastodon is this same effect - because of its newness, and lack of backing by an expansion-seeking corporation, it hasn’t attracted enough people the author doesn’t like yet. Just like Twitter in 2010. This doesn’t mean that I’m anti-Mastodon. In fact, I’m strongly in favor of it, and I hope it gains more adoption as a competitor to Twitter. I’m always in favor of open, decentralized platforms that are not controlled by a profit-seeking corporation. But I’d like to see the author revisit this article in 1 or 3 or 5 years, if the same people who he thinks make Twitter a “garbage pile” are on Mastodon as well. Of course one crucial difference between Twitter and Mastodon is that by design Mastodon makes it easy for communities to arise that have the power to systematically block content they don’t want to see. So maybe even in that future, the author would still feel “at home” on Mastodon, and so would the garbage pile people, and everyone would be happier than they are today. 1. 6 if the same people who he thinks make Twitter a “garbage pile” are on Mastodon as well. Some of them are already on the Fediverse, if not using Mastodon. Each instance can control who it federates with, and life goes on. 1. 2 I have heard it is even better: sometimes instance A federates with B, but only for explicit subscriptions and targeted messages (not for global search etc.). In this case, communicating with both sides of the schism of the day becomes feasible even on individual-user level, not just on the instance-level. 2. 3 Of course one crucial difference between Twitter and Mastodon is that by design Mastodon makes it easy for communities to arise that have the power to systematically block content they don’t want to see. So maybe even in that future, the author would still feel “at home” on Mastodon, and so would the garbage pile people, and everyone would be happier than they are today. I’m not familiar enough with Mastodon to know how this works. But if it’s as you describe above, then given the current highly-polarized state of Western democracy, we must recognize the downside of a system that would encourage people to disappear even further into the comfort of their own ideological ingroups. To the extent that Twitter users are confronted with opinions they vehemently disagree with, that’s a good thing for society. (Even though it’s notoriously rare for such a disagreement on Twitter to lead to a productive conversation.) 1. 5 On the one hand it is true; on the other hand, having a global conversation seems to encourage everyone to take a side in every conflict, which drives the polarization even deeper. It is not enough to show people things they disagree with, you have to show mostly the high-quality examples of the opposing views for anything good to happen. Maybe overlapping personal bubbles could provide better diffusion of ideas by avoiding indestructible walls? I am not sure this would work, I just don’t think we have any obviously-better simple options. 1. 8 I donate money on a monthly basis to the Against Malaria foundation, since they are one of GiveWell’s top rated effective charities. 1. 2 You are awesome. Stay awesome. 1. 6 1. 4 I do as well, having a more explicit tag is reasonable. 1. 11 I have to admit, I was very much in agreement with the author while reading the article. I thought the quoted email about the examples being so distracting that nothing could be learned from the book was simply melodramatic. But on finishing the article I realized my politics align with the author’s on every point. Based on the up votes it seems this article was well received. A challenge to readers who responded positively to this article: imagine Feuerstein had picked a different set of targets, say he derided victims of police brutality as criminals deserving what they got or accused unions of massive corruption and suggested they ought to be illegal. Would you still support his choice of examples under the same principle? I don’t find the examples nearly as cute when they don’t affirm my opinions, and would be tempted to say they don’t belong in a technical book. 1. 5 Indeed. I also found the OP’s take on “Americans not wanting to talk politics” to be quite a bit off, at least for me. It’s not really that I don’t want to talk politics. I used to do it a lot. But I got sick of the consequences of voicing my opinions. My own particular views tend to disagree with just about everyone else’s, so it just winds up creating a ton of friction and I end up losing a ton of time to it. One day, I realized that I didn’t want to spend my life that way (I’m certainly not going to change anyone’s mind) so I just mostly shut up about it. Things have been much better. If I had read the OP’s book, I don’t think I would have been so distracted as to be incapable of learning from them. But I certainly would be skeptical of any future work put out by the OP. The views themselves wouldn’t really bother me, even though I probably disagree with many of them in various ways. (If they did, I’d have a really hard time living in Massachusetts and working in Cambridge.) What would bother me is the fact that the author was so confident in their own opinions, that they would use them in a descriptive context as if they were facts. N.B. I use the word “politics” here to loosely mean “the discussion of current events in the context of government behavior” or “a controversial topic that divides political party lines” or something like that. I don’t use in the sense of “literally any action, including inaction.” (The latter interpretation exposes a trivial contradiction in the claim that I “mostly shut up about politics.”) 1. 4 Note that this was written in 2000, before a lot of the trends that have lead people in Anglophone countries to be more vocally political started happening. 2. 5 I don’t like unions and I do like guns and I’m very uninterested in being preached to about these things by tech people via a medium that doesn’t allow discussion. I don’t think I’d literally be unable to learn from reading the examples, I just think I would get a different book after a few of them or avoid this book if I knew about them going into things. I’m inclined to upvote things like this that I think are likely to provoke interesting conversations though for the record. 1. 5 via a medium that doesn’t allow discussion Well put. I don’t object to writing that mixes up politics and technology, as such. But smuggling in factoids without bothering to set up an argument is just poor form. It cheapens or even precludes the debate. I don’t care what the issue is or what side you’re on: if you care enough to write about it, you should care enough to write directly, show evidence, and build an argument. Little potshots crammed into code examples don’t help make a case; it merely shows a casual disrespect for the reader. 2. 1 My politics, too, align with those of the author. imagine Feuerstein had picked a different set of targets, say he derided victims of police brutality as criminals deserving what they got […] Would you still support his choice of examples under the same principle? Same as with when encountering any political speech: support everyone’s freedom to choose their political viewpoints and promote them [1], but only actually support politics that make the world better. Argue and rebut where you think it’s important to and/or effective. A.k.a. don’t ban the book, but that doesn’t mean you have to buy it or like it. AFAICT that’s what most people who disagreed with the actual book did, too. [1] With the usual dishonourable exception for politics intolerant of other viewpoints, or even entire peoples’ rights. I don’t advocate repressing their speech at every turn, simply because that is not the most effective way to suppress the school of thought, but a tolerant society must reserve that right to prevent the intolerant from abusing it and taking over. See the Paradox of tolerance. 1. 5 I’m on GNU Social, the distributed network of which Mastodon is one flavour of instances. @leeg@quitter.se 1. 11 Keep in mind some instances will blanket block GNU Social because: 1. It’s still on OStatus instead of ActivityPub, so privacy controls likely won’t work. 2. Many instances of GNU Social are “free speech zones” of “red fediverse,” which causes “deep blue” fediverse to silence/ban (depends on how strict they are) them. (Matthew Skala’s article on it is interesting; somehow, the fediverse stays together!) 1. 4 Huh. Thank you for that link. I’ve read it, and I don’t understand what Skala considers surprising about these events. It starts off by explaining some major factions, which certainly exist, but then what he describes doesn’t really have anything to do with the red/blue fragmentation. I’d love to see a write-up on the philosophical implications of fragmenting our communication platforms along ideological lines. I think we’re at a point in history where it’s inevitable, not due solely to political divisiveness, but due to the success of state actors who’ve worked to break the Internet’s original idea that we should have open communication regardless of national origin. And I think that’s very saddening. 1. 4 Yes, filter bubbling isn’t good, and federated networks might end up making it even easier to build one. The good news is I think third party nodes can still federate with both parties unless one does something like whitelisting or reprisals for following “the enemy.” My node is in such a situation; and I hope to keep it this way. 1. 1 The last election was the worst Ive ever seen filter bubbling thanks to how easy it is to unfollow or unfriend those that disagree. Im not sure how to counter it at this point since one is also fighting the algorithms and market share of the big compsnies. Temporary solution is just having several ways to support a point or policy that are tied to each of the prevailing audiences. There’s often overlap in interes. Trick is to focus claims on that while avoiding any words or points of your own political philosophy that are triggers for them. They just go into fight or flight mode if they spot one. Thing about this is there aren’t and won’t be enough people doing it. It might work focused on influential people, though. Then, the market or voter side gets pulled in indirectly. 1. 3 My thoughts on this topic probably deserve an essay rather than a comment here, but I tend to procrastinate forever on writing essays, so I’ll answer briefly anyway… I think “filter bubble” is a suboptimal way to conceptualize the problem you’re talking about, as there are significant parts of it that it doesn’t include. I also think that fundamentally that what we see in the US is an urban/rural cultural divide at play, but not in most of the ways that have gotten the most headlines; it’s a lot more complicated than that. That urban/rural tension has always existed (it’s why the US has an electoral college at all), but the Internet made it more obvious to everyone, because people can’t really escape being put into contact with people from the other side of it, in the way that they used to be able to. And that either means being exposed to concerted hatred of everything they are, or to condescension and claims to know everything. (I’ll let you think about which sides are guilty of which of those offenses… It’s a useful thought exercise.) And people are right to want to step away from that, and to want a break. For thousands of years it’s been possible, even if costly, to just leave when you can’t stand somebody or their attitude. It isn’t any more, and humans aren’t built for that. And in that sense it’s not too surprising that we see ways to achieve something similar online, but the degree of fragmentation is still quite shocking to me. But that said, I don’t blame the fragmentation for the election. Quite the opposite - I blame the communication. 2. 2 that’s up to them. If your instance doesn’t let you follow the people you want to follow you can switch to a different instance. 1. 1 I don’t think the answer to the problem of toxic or poorly administrated instances is as simple as “people should just switch instances if their operator does something about other instances’ toxicity” 1. 5 Legislation is the deeper problem. If I run an instance, I must not store illegal images on my server. Another instance in another jurisdiction might like to store images which are illegal for me. How can I keep those images away from my server? This is not about “poorly administrated” or “toxicity”. 1. 3 They’ve already had to deal with that problem on Mastodon - you can set federation on another server to allow everything except media, supress except to followers, that plus no media, and completely defederate. (The case was Japanese servers allowing “lolicon” when that’s illegal in some jurisdictions.) 2. 4 A lot of people are using Mastodon specifically because it allows them to create social networks that censor how they want to rather than how Twitter wants to. I don’t like any kind of censorship, particularly political censorship (and I view “toxicity” as a shibboleth of a specific cluster of political beliefs for speech they wish to make politically unacceptable, rather than as something universally bad), but that’s something that people running their own mastodon instance should feel entitled to do on their own instance. I would encourage people to be aware of the political biases of the people who run mastodon instances (of course, Twitter itself has its own set of political biases), and since my own politics are anti-censorship, I do actually think it would be good if people generally switched instances if the instance operator “does something about other instances’ toxicity”. 1. 1 The whole concept is always weird to me, since I only see things from people I follow. I agree you need a way to block people from mentioning you (or even block all mentions by people you don’t follow) but that’s easy to support and isn’t really censorship 2. 3 There’s a pretty wide range in how different instance admins define “toxicity”, and also a quite large range in how transparent and consistent they are, so if you encounter weird and poorly explained admin actions, switching instances to one that better matches your preferences can be a pretty reasonable course of action. I switched from mastodon.social to icosahedron.website in part for that reason (and in part because I like platonic solids). 1. 2 Neither do I. Somehow, the idea of distributed status servers escalated to “someone on an instance running this software is undesirable, therefore anybody using that software should be blocked”. I understand that some toxic people use computers, and yet here we are on a computer. 3. 1 I remember reading about GNU Social YEARS ago. Do we have any sense of the kind of adoption that network / service has seen as compared with Mastodon? I get the impression it (Mastodon) is taking off in ways that GNU Social and Friendica never did. 1. 1 It apparently (through Gab?) became a sort of haven for people even Twitter thought were too extreme. 1. 1 Gab Oof. Googling gab.ai yields a face full of angry “alt-right” … stuff. (Must… Resist.. Judgemental… Snark…) 2. 1 GNU Social doesn’t have that large of a userbase tho IIRC they are involved in the OStatus protocol and such. You can federate between Mastodon and GNU Social. 1. 2 I mentioned the Getting Things Done system in this comment (https://lobste.rs/s/jkmwer/what_are_you_working_on_this_week#c_ylb3cs). I’ve only just started doing this myself, so I can’t speak for its long-term efficacy, but having one central list that I can consult of everything that I thought I might want to do, that I can go to whenever I want to work on something, has already proven useful at getting me to use my time more efficiently. My specific strategy for keeping track of the Getting Things Done lists right now is just having several text files on a server that I have pretty reliable ssh access to, and writing them with an ordinary text editor. 1. 4 DIdn’t know about Yalp store, that’s handy. I run LineageOS on my phone, but did install google services and the play store because I wanted a few apps that require it. Maybe yalp is a way around the problem. 1. 5 LineageOS for microG (and yalp) seem to be a nice way around, indeed. There’s also this list of awesome FOSS apps on GitHub, as well as https://fossdroid.com. 1. 7 I started using the Getting Things Done system (https://hamberg.no/gtd/) to keep track of the various projects I’d like to work on. So, using the lists that that system encourages me to create, I can report that this week, I am going to spend trying to set up a personal Diaspora instance, to use to proxy messages I send to facebook or any of the other social networks they support. I like the idea of being able to use the externally-controlled social media platforms I am used to, but at a remove, mediated by software I control, and allowing me to ensure that I retain a copy of anything I see or write there. I don’t know how good diaspora will be at this, but that will be something I can judge, once I get a local instance working. 1. 1 I’m not familiar with the studies about type systems, but I feel pretty confident many large projects I’ve worked on would fall apart if they were dynamically typed. So in the spirit of the article, what do those studies actually say? In particular, what do they say about projects of different code sizes? Are there even enough multi-million line dynamic language projects to analyze? 1. 13 The article quite literally links to a review of studies made. I can’t help but notice that you kind of prove their complaint: people not even doing the simplest review of linked sources. https://danluu.com/empirical-pl/ 1. 4 Yes, it’s true, I didn’t review the linked sources. Because they are long and I don’t quite care enough. I’m just curious enough to ask, since it’s likely someone here would already know and have an answer slightly more concise than several pages. :) 1. 3 The problem with comparing static and dynamic languages is that that variable is hard to isolate between all the other differences between individual languages that have a static type system and individual languages that have a dynamic type system. I’ve seen danluu’s analysis before, and not been particularly impressed that any of them were really answering the question of “all else being equal, is static typing better than not?”, as opposed to showing that you can write code with fewer bugs in Haskell specifically than with Python specifically, or that Java’s type system doesn’t gain you all that much, or some result along those lines. Not all type systems are equally powerful or ergonomic in any case. I’m a big fan of strong typing myself, from my own intuitional experience of maintaining large codebases written in dynamically-typed languages and debugging things that a type-checker would’ve caught, but I think that has as much to do with the fact that a specific set of popular strongly-typed languages encourage a different mindset around creating code compared with a specific set of popular dynamically-typed languages, than about the raw fact of having types or not. 1. 2 The fact that it’s hard to analyze is itself evidence that static typing does not play a dominant role. If the type system was the defining feature of the language it would dominate other factors, in practice it clearly does not. 1. 7 That may not be a valid way to look at the problem. See McNamara Fallacy: https://en.wikipedia.org/wiki/McNamara_fallacy But I might not be completely understanding what you’re saying. 1. 3 I’m not talking about disregarding anything. To put it another way, we have to observe a statistical difference for a language or a group of languages compared to others. For example, if projects written in Haskell were statistically of higher quality than those written in other languages, we could make a hypothesis that Haskell type system has a positive impact on quality and test that hypothesis. 1. 4 This is a much different statement than the first one I responded to. Your first statement was that “X being hard to measure is evidence X isn’t a big factor”. But that is clearly wrong. It means you cannot say much about X, not evidence for one particular interpretation of it. 1. 2 That was not my statement. The statement was that X does not appear to play a more significant role than other factors. 1. 1 Does that mean you do know how to measure the factors? 1. 1 I’m saying that you have to show that statistical trends exist before you can start having discussion about different factors and their potential impact. 1. 2 Does that mean you’re changing your original statement? Your original statement was: The fact that it’s hard to analyze is itself evidence that static typing does not play a dominant role. Being hard to analyze is not evidence for a particular interpretation other than the interpretation that it’s hard to analyze. 1. 1 I’m not changing anything. If a particular factor had a significant contribution that would be an invariant in all languages that have this factor. I think at this point you know exactly what I’m saying, and you’re just playing word games with me. 1. 1 But that is only true if what one is measuring is well-defined, which it doesn’t appear to be, right? It feels like you’re saying the absence of evidence is evidence of absence, which is clearly false. I’m not playing word game with you, I’m being precise in order to understand what you are saying. Based on what you’ve said, it seems like one would have to conclude that that one cannot say one way or the other the effect of the type system on a project rather than that it has no effect. Isn’t this like the difference between not-rejecting the null hypothesis vs accepting the null hypothesis? 1. 1 Once again, what I’m saying is that you have to demonstrate that there is a statistical difference before you can discuss the cause of that difference. What part of that statement are you having trouble with? 1. 1 That statement is perfectly reasonable, but that is not the first statement you made where you claimed that the mere fact that something is difficult to measure is evidence of a particular conclusion. Did I misinterpret what you said? The exact quote is: The fact that it’s hard to analyze is itself evidence that static typing does not play a dominant role. 1. 2 That directly follows from the fact that statistical differences have not been demonstrated. If a particular language is shown to be a statistical outlier, then you could reasonably say that some feature or combination of thereof are responsible for that. Since we are not seeing such outliers, that strongly implies that the choice of language is not a dominant factor. It’s entirely possible that things like developer skill, development process, and testing practices eclipse any effect a language might have. 2. 14 I’m not familiar with the studies about type systems, but I feel pretty confident many large projects I’ve worked on would fall apart if they were dynamically typed. Sure. And ancient Greek scholars felt pretty confident that rubbing garlic on a magnet would demagnetize it. We need to start by recognizing that a personal feeling of confidence is an absolutely terrible basis from which to derive objective facts about the world. 1. 3 Fall apart in what sense? I worked for 15 years on a codebase that was maintained by about 500 engineers. 90% of it was written in TCL. You might argue the codebase would have been better if it had been typed, but we continued to make money just fine, and despite competitors (internal and external) trying to rewrite or replace it, they couldn’t. It didn’t ‘fall apart’. 1. 7 I notice that all of these examples have to do with a specific programming problem, namely moving from non-concurrent to concurrent execution models. This is something that most programming languages have been historically bad at because of lack of need, and modern programming languages are being built with specific features to make safely writing concurrent programs easier. So it’s possible that this issue of software rot is really more about the difficulty of managing a specific programming problem, namely introducing concurrency to an environment which previously lacked it. 1. 3 I feel this is a big part of it. I also think nobody currently trying to fix it is pointed in the right direction, with the possible exception of Pony. 1. 4 The big thing I’m confused about with TLA that I haven’t seen any of the commentary about it handle is, how can I use TLA to say something useful about software that I’m currently working on? For instance, right now I’m working on an interpreter for a toy programming language, and I have no idea how I could apply TLA to make that codebase less buggy, or make my toy language design better in some way. 1. 3 I’ve not worked on interpreters, so I can’t think of a good example off the top of my head, but I’ve written and presented on how TLA+ has been useful for adding functionality to a web app. I also like this article on detecting thread deadlocks, and this example of simulating trading algorithms. 1. 3 Just wanna let you know that all your work is appreciated, I’ve got “learn TLA” as my main go-to task over the upcoming Christmas break. Waiting on my copy of LL’s book to arrive before then as well, I hope :) Edit: Me fail english? That’s unpossible! 1. 2 Aww, thank you! If it doesn’t arrive in time, it’s also downloadable free here. 2. 2 Two questions (as I work through this list). I’m just finishing watching your Strangeloop talk, got to the part about “Redacted” where you describe TLA+ finding that your fixes to satisfy the invariant cause another invariant to no longer hold. I was curious if TLA+ is also capable of finding contradictory invariants; specifically non-obvious ones. My second question relates to the first, atwork, I’m responsible for maintaining and designing the infrastructure surrounding one of our main applications. I’m not alone in this task, but I’m significantly more experienced (most of the team is new as of the beginning of this year, I’ve been there for 5 years) than the rest of the team so naturally a lot of things fall to me. The existing architecture we maintain is gnarly and old, having been designed by poorly trained orangutans gentlemen before my time. We are simultaneously planning a port to a new infrastructure with some architectural changes, and I’m curious about applying TLA+ to the design of this new infrastructure. Part of the issue with the old design is the plethora of constraints applied to everything due to old contracts, SLA expectations, etc; a major concern that I have been working through is ensuring that we aren’t painted into an impossible corner, and while my background is in math, doing that much of it by hand is not… y’know… ideal. I was curious if you know of any resources on infrastructural/low-level/devops-y design with TLA+. It seems like it’d be a natural fit (esp. as I try to get us to a newer model, but also for diagnosing systemic errors in the old).

EDIT: Also, just finished the talk as I wrote this, great talk – everyone should go watch it, it’s the one hwayne links above.

1. 2

I’m just finishing watching your Strangeloop talk, got to the part about “Redacted” where you describe TLA+ finding that your fixes to satisfy the invariant cause another invariant to no longer hold. I was curious if TLA+ is also capable of finding contradictory invariants; specifically non-obvious ones.

Ooh, good question. The short answer is “probably”. The long answer is it depends.

Invariants in TLA+ don’t have any special status: they’re just operators that return booleans. When you declare it an invariant, the model checker raises an error if it’s ever false. If you want to find out if two invariants are contradictory, that’s logically equivalent to determining if, in all states, both don’t hold. So you could make your invariant Contradictory == ~(A /\ B). If that doesn’t hold, TLA+ will give you a state where both invariants are true at the same time.

The two caveats are 1) TLA+ only checks finite state spaces, so if the model passes, you aren’t guaranteed it will always be contradictory. It might hold for a larger model. And 2) This is only applies to safety invariants, aka “bad things never happen” invariants. There’s also liveness invariants, which are things like “all messages sent are eventually received” or “the database will eventually reach consistency.” Those can’t be composed in the same way.

I was curious if you know of any resources on infrastructural/low-level/devops-y design with TLA+. It seems like it’d be a natural fit (esp. as I try to get us to a newer model, but also for diagnosing systemic errors in the old).

One of the problems with TLA+ as it currently exists is the community is tiny and most of the specs are private. I did a quick demo of modeling zero-downtime deployments but that’s the only public devops thing I can think of. “Redacted” was a pretty heavy infra project, though, so I guess I can vouch for TLA+’s applicability in those kinds of situations.

1. 1

Invariants in TLA+ don’t have any special status: they’re just operators that return booleans…

Interesting. I suppose once you have the invariants in a reasonably notation, it’s not too hard to put them through some other sort of Satisfier and have it look for contradictions. Half the battle is probably getting to the point of a formal notation for them.

I did a quick demo of modeling zero-downtime deployments… so I guess I can vouch for TLA+’s applicability…

This is good, this is the sort of thing that helps me justify this isn’t a rabbit hole when I tell my boss I’m working on it. :D

1. 2

Half the battle is probably getting to the point of a formal notation for them.

It’s not actually that bad. TLA+ is a first order logic, so it’s pretty easy to do stuff like

  OneTargetPerWorker ==
\A w1 \in Workers, w2 \in Workers:
target[w1] = target[w2] =>
target[w1] = NULL \/ (w1 = w2)


Most of my trouble comes from running into TLA+ footguns, which is why I spend so much time writing about how to avoid TLA+ footguns.

This is good, this is the sort of thing that helps me justify this isn’t a rabbit hole when I tell my boss I’m working on it. :D

Awesome! Feel free to message me if you need any help with anything!

3. 1

It’s kind of the reverse of the “rest of the fucking owl” problem :)

1. 1

If it has concurrency, it’s possible TLA+ could help with ordering problems. Additionally if it was fault-tolerant with several keeping in sync with some protocol. Otherwise, Alloy for data structures or SPARK Ada for correctness would be more appropriate far as lightweight, formal methods go.

http://alloy.mit.edu/alloy/

https://en.wikipedia.org/wiki/SPARK_(programming_language)

1. 2

I’ve started learning Alloy and it’s really, really cool. I want to spend more time improving before I make sweeping statements about it, but I think it might actually beat TLA+ for the case of non-concurrent time modeling. That’s because you can represent a single data structure undergoing mutation as an ordered sequence of structures where each pair is restricted to differ by a mutation. Alloy can then look at the entire “timeline” at once, while TLA+ is restricted to treating the mutations as separate states in a behavior.

The reason TLA+ does that, of course, is to provide first-class temporal support, so adding multiple structures changing over time is trivial, while for Alloy you’d need to add an explicit time variable and then everything gets really messy. I think it’ll be good to know both.

Also the Alloy resources are so much better than the TLA+ resources. I wonder if I would have been willing to learn TLA+ if I started with Alloy. I hope I would have.

1. 1

I only recently came across Alloy, it does indeed seem really interesting and the tutorial I found looks great. Unfortunately for me the UI NPEs the instant it receives a keypress, so I can’t use the tools. At some point I might extract the sources and try to debug it, but I’ve not decided to act on that yet because I fear it’s likely to lead to a lot of work :)

1. 1

Very interesting observation on time modeling. I was hoping you’d learn Alloy. You have a talent for turning this odd tech into stuff people can understand and use. I do encourage you to wait on the writeup so you can apply Alloy to various structures and use-cases first. Definitely skim through the publication list to see the kinds of things they used it on. That was everything from data structures to security policies to component repair from contracts. Think of the things you’ve seen real-world developers deal with that’s similar. Small examples with tricky-to-test flaws or that would require brute-force with time consuming pile of tests are good examples. Attempts at Alloy on such diverse problems will show you its strengths and weaknesses. If you commit to it, I’m sure we’ll enjoy your write-up at least as much as the TLA+ one. :)

I’m glad you learned TLA+ first, though, as I might have never had a chance to learn it if I had to face the documentation and guides you did. They did not look beginner-friendly compared to Alloy. I had seen it first in a high-assurance VPN [1]. Quite a few people used it for configuration verification. Esp networked- or component-based. I bet that still has potential with all the black boxes I see ops people flinging together in submissions.