Leaky Delegation: You are not a Commodity 2021-01-25T02:04:55.942Z
Cause Awareness as a Factor against Cause Neutrality 2018-08-13T20:00:49.513Z
The Partial Control Fallacy 2016-12-14T02:57:24.773Z
Raytheon to Develop Rationality-Training Games 2011-11-18T21:07:51.461Z
Meetup : Pittsburgh Meetup 2011-09-30T17:48:10.478Z
Little Johny Bayesian 2009-03-18T21:30:59.049Z


Comment by Darmani on The Nature of Counterfactuals · 2021-06-06T18:18:45.138Z · LW · GW

The underlying thought behind both this and the previous post seems to be the notion that counterfactuals are somehow mysterious or hard to grasp. This looks like a good chance to plug our upcoming ICML paper, w

hich reduces counterfactuals to a programming language feature. It gives a new meaning to "programming Omega."

Comment by Darmani on Taking the outside view on code quality · 2021-05-07T07:47:48.776Z · LW · GW

It's a small upfront cost for gradual long-term benefit. Nothing in that says one necessarily outweighs the other. I don't think there's anything more to be had from this example beyond "hyperbolic discounting."

Comment by Darmani on Taking the outside view on code quality · 2021-05-07T05:09:54.996Z · LW · GW

I think it's simpler than this: renaming it is a small upfront cost for gradual long-term benefit. Hyperbolic discounting kicks in. Carmack talks about this in his QuakeCon 2013, saying "humans are bad at integrating small costs over time":


But, bigger picture, code quality is not about things like local variable naming. This is Mistake #4 of the 7 Mistakes that Cause Fragile Code:

Comment by Darmani on Lean Startup Reading Comprehension Quiz · 2021-02-02T06:28:58.628Z · LW · GW

I read/listened to  Lean Startup back in 2014. Reading it helped me realize many of the mistakes I had made in my previous startup, mistakes I made even though I thought I understood the "Lean startup" philosophy by osmosis.

Indeed, "Lean Startup" is a movement whose terminology has spread much faster than its content, creating a poisoned well that inoculates people against learning 

For example, the term "minimum viable product" has been mutated to have a meaning emphasizing the "minimum" over the "product," making it harder to spread the actual intended idea.  I blogged about this a long time ago:

Anyway, this post was a nice review! I had to guess on some of the questions, which is probably good; if I'm successful, it means I really internalized it. Thanks!

Comment by Darmani on Lean Startup Reading Comprehension Quiz · 2021-02-02T06:23:32.106Z · LW · GW

1. What is the difference between learning and validated learning?

 Validated learning is learning that has been tested empirically against users/the marketplace.

2. True or false: "According to the author, a startup with exponential growth in metrics like revenue and number of customers is doing well." Explain your answer.

 False. This is only true if those metrics imply a path of long-term sustainable profitability. If the startup in question is Github, it probably does. If it's Groupon.....

3. Finish the sentence: "almost every lean startup technique we've discussed so far works its magic in two ways:"

  By reducing inventory and increasing validated learning. 

4. Ries argues that startups should pay more attention to innovation accounting than traditional accounting. Name two ways in which startups can change their financial metrics to accomplish innovation accounting.

 (a) Estimate the value of patents/trade secrets and track on an internal balance sheet. (b) Require VoI calculations and add such numbers to an internal balance sheet. 

5. Describe, concretely, what a car company's supply chain would look like if it used push vs pull inventory.

 Push: Each supplier pumps out parts, which are stockpiled in storerooms and warehouses.  Each factory will regularly, e.g.: be shipped all the stuff it needs for the next month. Pull: Each factory keeps just a few days of parts needed, places frequent orders for the next few day's worth.

6. Ries applies the pull inventory model to startups. But what is the unit that is being pulled, and where does it obtain the "pull signal"?

 The unit is "aspects of the business that deliver value to customers." The initial pull is validated market demand, which then translates to internal demand for features/process.

7. True or false: "Lean manufacturing is meant to give manufacturers an advantage in domains of extreme uncertainty". Explain your answer.

 True. Lean manufacturing allows manufacturers to retool and change their production much faster, greatly cheapening the cost of creating a suboptimal or unwanted product.

8. True or false: "Lean manufacturing is about harnessing the power of economies-of-scale."

 False. Lean manufacturing cheapens the cost of small runs, making the manufacturer more competitive at a lesser scale.

9. Ries discusses an anecdote of a family folding letters. The dad folds, stamps, and seals one letter at a time; whereas the kids begin by folding all letters, then stamping all, etc. Name two reasons Ries' considers the dad's method superior.

 a) Not having to manage the intermediate outputs. b) Can discover issues later in the pipeline earlier.

10. True or false: "A consequence of lean manufacturing is that the performance of each employee as an isolated unit, in terms of output per unit of time, might *decrease*." Explain your answer.

  Lean manufacturing comes with much higher switching costs. An employee's output might shrink, but more of it will go towards useful ends.

11. Give an example of what a “large batch death spiral” might look like in practice. 

 My game team is running behind schedule.  To catch up, I ask the artists to produce assets without waiting for them to be tested.  This then creates a large batch of work for the programmers to implement the graphics, which produces a large back of comments. This gets passed back to the artists, who do a huge number of revisions at once. The cycle continues.

12. According to Ries, the “Five why’s” method is a control system (though he doesn’t say so explicitly). What does it control, and how? 

 It puts a damper on major failures; it creates a mechanism by which a failure is turned into a systematic, mitigating change.

13. Explain the meaning of Toyota proverb “Stop production so that production never stops”

 Do regular maintenance and improvement work to prevent larger future problems.

Comment by Darmani on Limiting Causality by Complexity Class · 2021-01-31T20:31:36.167Z · LW · GW

Causal inference has long been about how to take small assumptions about causality and turn them into big inferences about causality. It's very bad at getting causal knowledge from nothing. This has long been known.

For the first: Well, yep, that's why I said I was only 80% satisfied. 


For the second: I think you'll need to give a concrete example, with edges, probabilities, and functions. I'm not seeing how to apply thinking about complexity to a type causality setting, where it's assumed you have actual probabilities on co-occurrences.

Comment by Darmani on Limiting Causality by Complexity Class · 2021-01-31T00:17:58.074Z · LW · GW

This post is a mixture of two questions: "interventions" from an agent which is part of the world, and restrictions

The first is actually a problem, and is closely related to the problem of how to extract a single causal model which is executed repeatedly from a universe in which everything only happens once. Pearl's answer, from IIRC Chapter 7 of Causality, which I find 80% satisfying, is about using external knowledge about repeatability to consider a system in isolation. The same principle gets applied whenever a researcher tries to shield an experiment from outside interference.

The second is about limiting allowed interventions. This looks like a special case of normality conditions, which are described in Chapter 3 of Halpern's book. Halpern's treatment of normality conditions actually involves a normality ordering on worlds, though  this can easily be massaged to imply a normality ordering on possible interventions. I don't see any special mileage  here out of making the normality ordering dependent on complexity, as opposed to any other arbitrary normality ordering, though someone may be able to find some interesting interaction between normality and complexity.


Speaking more broadly, this is part of the broader problem that our current definitions of actual causation are extremely model-sensitive, which I find a serious problem. I don't see a mechanistic resolution, but I did find this essay extremely thought provoking, which posits considering interventions in all possible containing models:

Comment by Darmani on Leaky Delegation: You are not a Commodity · 2021-01-28T00:11:49.667Z · LW · GW

Thought I'd share an anecdote that didn't make it into the article: on how doing something yourself can make you a better outsourcer.

About 6 months ago, I went shopping for a logo for one of my projects. It helped greatly that I've spent a lot of time studying visual design myself.

I made a document describing what I wanted, including a mood board of other logos. I showed it to a logo design specialist recommended by a friend. He said "That's the best logo recquisition doc I've seen, and I've seen a lot."

I also showed it to the designer I've been working with on other things (like sprucing up Powerpoint slides). She's not a logo specialist, but quoted half the price.

I had the confidence that I'd be able to give good feedback to my designer even if she was less likely to knock it out of the park on her first try than the specialist. I went with her.

Many rounds of feedback later, I had a design. Showed it to some housemates and my advisor. "Dang, that's a good logo."


You can see it live at .

Comment by Darmani on Leaky Delegation: You are not a Commodity · 2021-01-28T00:07:49.840Z · LW · GW

Oh, on the contrary: I think this article misses several things that are quite important (or were brushed under a single sentence like "[main principal/agent problems] are communication and risk." Reason: emphasis on things fewer readers were likely to consider.

So the costs you're describing are indeed real and brushed off to corner. I think both of these fall under transaction costs, and #2 also under centralization and overhead. For #2, I think you mean something other than what "externality" means to me (a cost specifically born by a non-party to a transaction) --- maybe second-order cost?


Comment by Darmani on Leaky Delegation: You are not a Commodity · 2021-01-28T00:01:17.973Z · LW · GW

Thanks! This is good.

It's not a physical good, but I had also been thinking that most of the price of renting a venue on the open market is trust (that you won't mess up their space; whether they can give you the keys vs. needing someone to let you in), followed by coordination. Hence, why having a friend let you use their office's conference room on a weekend to do an event might cost $0, while renting such a space might cost $1000.

Comment by Darmani on Leaky Delegation: You are not a Commodity · 2021-01-27T07:44:21.131Z · LW · GW

To clarify: You're not saying the wedding tax is because of insurance costs, as the article is asking about, right?

Comment by Darmani on Leaky Delegation: You are not a Commodity · 2021-01-26T22:13:57.231Z · LW · GW

Thanks; fixed!

Comment by Darmani on Help your rivals when they are numerous · 2021-01-23T10:07:36.765Z · LW · GW

I have a number of issues with this post.


First, as others have mentioned, opponents are very much not equal. Further, timing is important: certain trades you should be much more or less likely to take near the end of the game, for example.

Second, I don't think it's valid to look at expected values when all you care about is rank.  Expectation is very much a concept for when you care about absolute amounts.

Third, which perhaps sums everything up: I don't see a valid notion of utility / utility maximization for board games, other than perhaps "probability of winning," which makes this circular ("if you're trying to win, you should make moves that increase your probability of winning"). Utility is meant to put a linear scale on satisfaction with a given state of the world. When discussing what to do in a board game, one usually presumes the objective is to win, and satisfaction derives ultimately from winning. The closest thing you usually see to a "utility" number on an intermediate state is a heuristic, as used in e.g.: chess AIs, where you might give yourself 5 points for having a pawn in a center square. If I'm remembering my undergrad correctly, these heuristics are intended to approximate log-likelihoods of victory, but they certainly lack the soundness required to think about expected utility.


Let's switch out of Catan, and to a game that hopefully people here know but is more directly combative: Diplomacy. Pray tell me how you propose to assign a utility score to putting a navy in the Black Sea.

Comment by Darmani on In software engineering, what are the upper limits of Language-Based Security? · 2020-12-28T01:01:12.819Z · LW · GW

Did not know about the answer/comment distinction! Thanks for pointing that out.

Before I dig deeper, I'd like to encourage you to come bring these questions to Formal Methods for the Informal Engineer ( ), a workshop organized by myself and a few other researchers (including one or two more affiliated with LessWrong!) specifically dedicated to helping build collaborations to increase the adoption of formal methods technologies in the industry. Since it's online this year, it might be a bit harder to have these deep open-ended conversations, but you sound exactly like the kind of person we want to attend. (To set expectations, I should add that registrations already exceed capacity; I'm not sure how we plan to allocate spots.)

I'd also like to share this list of formal methods in industry: . In the past decade, there's been a huge (in relative, not absolute terms) increase in the commercial use of formerly Ivory Tower tools.

You may also be interested in the readings from this course:

BTW, I've been trying to think about whom I know that directly works in language-based security.  (defined as a narrow specialty). The main name that comes to mind that I personally know is Stephen Chong, but I think some of the Wyvern developers ( ) may also consider themselves in this category (and be easier to get ahold of than a Harvard professor).

I'm going to briefly hit some of your more narrow questions now. As an aside, be wary about saying "process" to a researcher -- it's used narrowly in ICSE circles to mean "methodology" (e.g.: Agile). I'm trying to mentally replace every use with "language-based security."

the most security-promoting development processes that are currently in wide use.

I think Jim mostly gets it above: memory-safe languages and secure API design; also, implicitly, the type systems that make the latter possible.

There are a number of patterns in secure API design you might not know the names for, such as object capabilities ( ).

In a way, this question is kinda self-answered by the framing, since language-based security primarily refers to language design, which primarily means type systems --- this is in contrast to techniques such as static analysis, testing, model checking, symbolic execution, and sandboxing.

Leaving the realm of Turing-complete programs, I'll point you to PNaCl/RockSalt ( ) and eBPF, both of which have verified sandboxes.

If you're willing to be flexible about the "widely-used" statement, then individual companies have their own quirky languages, some of which have rather interesting restrictions. This language ostensibly used by OutSystems comes to mind ( ), although I'm told by one of the authors that their actual implementation (as of 2013) is a bit simpler.


  • the most security-promoting development processes that are possible with recently developed technology


This is a tough question for me, because recent papers in this area tend to be about solving highly specific problems (the space of security problems is big, yo), and it takes a lot to generalize that to answer such a broad question. Also, I don't follow latest developments that intensely. I'm going to take a pass.


  • processes that could come to exist 10 years away; processes that might exist 30-50 years from now.


Adam Chlipala thinks by that time we'll be generating correct-by-construction code from specs. The Everest and Fiat-Crypto projects, both of which generate correct-by-construction cryptography code, are probably the two current best-known deployments of this.



  • perhaps some impossibility theorems that may bind even the creatures of the singularity.


"If it's nontrivial to prove your program terminates, your program probably doesn't run." --- an undergrad friend.

For common infrastructure software of today, no. Except maybe that I don't know it's been shown  possible to build secure, reliable software atop a realistic model of hardware faults.

For Software 2.0 (i.e.: neural net in the loop), it's a more open question that I don't know much about.

For the kinds of reflective self-improvement software MIRI discusses, that's part of their active research program (and generally outside the cognizance of PL/SE researchers).

Comment by Darmani on In software engineering, what are the upper limits of Language-Based Security? · 2020-12-27T06:52:40.819Z · LW · GW

It is already possible to build an embedded language inside of Coq which requires arbitrary security proofs for all executable code. It's theoretically possible to make those proofs guard against all known side channels, including, theoretically, hardware-based side channels such as Row Hammer.

Are you asking about which kinds of attacks can't be stopped by improving software? Or are you asking about the theoretical limits of PL technology? The latter question is not so interesting without  more constraints: as stated above, they're basically unbounded.

Comment by Darmani on Extortion beats brinksmanship, but the audience matters · 2020-11-21T09:29:43.343Z · LW · GW

Okay. I think you're saying this is extortion because Walmart's goal is to build a reputation for only agreeing to deals absurdly favorable to them.

If the focus on building a reputation is the distinguishing factor, then how does that square with the following statement: "it is not useful for me to have a credible reputation for following up on brinksmanship threats?"

Comment by Darmani on Extortion beats brinksmanship, but the audience matters · 2020-11-20T01:01:03.340Z · LW · GW

I see. In that case, I don't think the Walmart scenario is extortion. It is not to the detriment of Walmart to refuse to buy from a supplier who will not meet their demands, so long as they can find an adequate supplier who will.

Comment by Darmani on Extortion beats brinksmanship, but the audience matters · 2020-11-18T02:53:18.473Z · LW · GW

I'd really appreciate a more rigorous/formal/specific definition of both. I'm not seeing what puts the Walmart example in the "extortion" category, and, without a clear  distinction, this post dissolves.

Comment by Darmani on Extortion beats brinksmanship, but the audience matters · 2020-11-17T04:25:52.461Z · LW · GW

Very interesting post. I was very prepared to praise it with "this draws some useful categories for me," but it began to get less clear as I tried more examples. And I'm still trying to come up with a distinction between brinksmanship and extortion. I've thought about the payoff matrices (they look the same), and whether "unilateral attack vs. not" is a distinguishing factor (I don't think so). I still can't find a clear distinction.



(1) You say that releasing nude photos is in the blackmail category. But who's the audience?

(2) For n=1, m large:  Is  an example of brinkmanship here a monopolistic buyer who will only choose suppliers giving cutrate prices? It seems to have been quite effective for Walmart decades ago, and effective for Hollywood today ( ).

Comment by Darmani on Gems from the Wiki: Paranoid Debating · 2020-09-15T06:26:34.430Z · LW · GW

I tried playing this in 2009 at a math summer program. It scared a lot of people away, but I got a small group to join in. The scoring algorithm was rather questionable, but the game of competitive Fermi estimates was fun.

I can't claim to have improved much at rationality or estimates, but, ever since then, I remember that, to the question "How many liters of water are there in the ocean," the answer "1 mole of liters" is not the mark of a deceiver, but is actually relatively close, being only 1 order of magnitude too low.

If I ever play again, now that I know some measure theory, I'd be tempted to play a distribution that has an arbitrarily high mass at every rational number, and 0 at every irrational number.

Comment by Darmani on When can Fiction Change the World? · 2020-08-25T09:20:07.535Z · LW · GW

Nice post!

Another example for your list: Altneuland catalyzed the Zionist movement that led to the creation of Israel. The city of Tel Aviv is named after the book.

Comment by Darmani on A Hierarchy of Abstraction · 2020-08-11T23:59:57.670Z · LW · GW

Was just reading through my journal, and found that I had copied this quote. I think you'll find it to be of interest re: teaching recursion.


From “Computing Science: Achievements and Challenges” (1999):

“I learned a second lesson in the 60s, when I taught a course on programming to sophomores, and discovered to my surprise that 10% of my audience had the greatest difficulty in coping with the concept of re, cursive procedures. I was surprised because I knew that the concept of recursion was not difficult. Walking with my five-year old son through Eindhoven, he suddenly said "Dad not every boat has a life-boat, has it?" '"'How come?" I said. "Well, the life-boat could have a smaller life-boat, but then that would be without one." It turned out that the students with problems were those who had had prior exposure to FORTRAN, and the source of their difficulties was not that FORTRAN did not permit recursion, but that they had not been taught to distinguish between the definition of a programming language and its implementation and that their only handle on the semantics was trying to visualize what happened during program execution. Their only way of "understanding" recursion was to implement it, something of course they could not do. Their way of thinking was so thoroughly operational that, because they did not see how to implement recursion, they could not understand it. The inability to think about programs in an implementation-independent way still afflicts large sections of the computing community, and FORTRAN played a major role in establishing that regrettable tradition”

Comment by Darmani on Reveal Culture · 2020-08-11T21:43:39.939Z · LW · GW

I've noticed that the Reveal Culture examples / Tell Culture done right resemble greatly the kinds of communication advocated in the many strands of conflict/communication training I've taken. Connecting your requests to needs, looking for interests instead of positions, seeing the listener's perspective, etc.

For instance, the Tell Culture example example "I'm beginning to find this conversation aversive" is quite close to the example from my training "I notice I'm having a reaction," except that it's closer to being judgmental. For comparison, here's a quote I have in Anki, I believe from the book "Difficult Conversations": "When doing active listening, strategies for making the tension explicit include signaling that you're having a reaction, sharing how you're feeling, and postponing the conversation because of emotions."

The people who gave Malcolm's friend the "Crocker's Rules" impression were probably failing to not mix in judgments into their tells. I recently taught a workshop on this, which reminded me just how hard this is for many people.

It's become very apparent to me that one person with high communication skills can go a long way towards making up for deficits in all whom they interact with. If Reveal Culture/Tell Culture as you understand it really is recommending adopting some of the habits recommended by books like NVC and Difficult Conversations, then I do see this as primarily being about skill, not culture, although learning these skills can be quite deep and can entail some personality changes. One possible reconciliation: having a default preference toward sharing your inner world and accepting those of others may make people much more tolerant of unskilled attempts to do so, where people inadvertently give their positions and judgments instead of their observations, feelings, and needs.

Comment by Darmani on Towards a Formalisation of Logical Counterfactuals · 2020-08-09T23:19:02.101Z · LW · GW

Hi Bunthut,

First, I'll encourage you to have a look at material on what I thought this post was going to be about from the title: . I know about this subject primarily from (which is more concrete/mathematical than the Wikipedia article, as it's written by computer scientists rather than philosophers).

Second: If I'm understanding this correctly in my sleep deprived state, you're actually working on the exact same problem that I am in one of my papers, except that we focus on causality/counterfactuals in logic systems which correspond to programming language semantics. I got stuck on similar problemss. I can send you a preprint if you PM me.

Overall, my take is that you're getting stuck in superficial differences of formalisttm, which makes it much harder for sleep-deprived me to find the insight. E.g.: the desire to use graphs to represent proofs; with the proper conceptual toolkit, this "multiple-antecedent problem" is a non-issue. (Two solutions: (1) use hypergraphs [which we do in the current draft of the paper]; (2) join antecedents into one, as is done in proof categories.)

Comment by Darmani on A Hierarchy of Abstraction · 2020-08-09T02:06:58.118Z · LW · GW

I was 12 or so when I first studied pointers. I did not get them at all back then.

Comment by Darmani on A Hierarchy of Abstraction · 2020-08-08T12:16:43.984Z · LW · GW

Thanks for the explanation. I accept your usage of "abstraction" as congruent with the common use among software engineers (although I have other issues with that usage)). Confusingly, your hierarchy is a hierarchy in g required, not a hierarchy in the abstractions themselves.

I am well-read in Joel Spoelsky, and my personal experience matches the anecdotes you share. On the other hand, I have also tutored some struggling programmers to a high level. I still find the claim of a g-floor incredible. This kind of inference feels like claiming the insolubility of the quintic because I solved a couple quintics numerically and the numbers look very weird.

Sidenote: I find your example discussion of human learning funny because I learned arithmetic before writing.

Comment by Darmani on A Hierarchy of Abstraction · 2020-08-08T10:09:00.322Z · LW · GW

You seem to be making a few claims: (1) that these skills require an increasing amount of 1-dimensional intelligence (2) that one cannot do lower-indexed things without doing higher-indexed ones and (3) that there is something fundamental about this.

You obviously do not mean this literally, for there are plenty of people who understand recursion but not pointers (i.e.: intro Python students), and plenty of programmers who have never touched Python.

First, what is an abstraction?

As someone who recently wrote a paper involving Cousot-style abstract interpretation, this is a question that interests me. We in programming-languages research have our answer: that an abstraction is a relation between two spaces such that every behavior in the larger ("concrete") space has a corresponding behavior in the smaller "abstract" space. In this definition, there is a sensible meaning of a hierarchy of abstraction, but it's not what most people think: tracking arbitrary sets of integers is less abstract than tracking intervals of integers, which are in turn less abstract than tracking the possible sign(s) of a number.

I am less familiar with abstraction as it is used by AI researchers; my understanding is that it is similar, but without the strict requirements, e.g.: they'll be willing to analyze poker rounding all bets to multiples of $5, and say that two bets of something that rounds to $5 = 1 bet of something that rounds to $10 bet, rather than "something that rounds to $5, $10, or $15", as would the PL researcher.

Most software engineers seem to use "more abstract" to mean "can be implemented using" or "can be defined using," e.g.: the home screen on my phone is an abstraction built on top of the file system, which is an abstraction built on top of the hardware. This seems to be the closest to what you mean. In that sense, I cannot see what makes these examples a hierarchy, or fundamental in any sense. E.g.: recursion clearly does not require arithmetic. The lambda calculus has recursion but not arithmetic.

The best I can make of this post is that these tasks have something akin to a hard-floor in g-factor required, which is an extraordinary claim in need of extraordinary evidence.

Comment by Darmani on Writing Causal Models Like We Write Programs · 2020-05-14T17:33:18.390Z · LW · GW

John is correct that do() is not imperative assignment. It's a different effect called "lazy dynamic scope."

do() is described fully in our paper on formal semantics for a language with counterfactuals, . The connection with dynamic scope is covered in the appendix, which is not yet online.

Comment by Darmani on Two Alternatives to Logical Counterfactuals · 2020-04-01T18:06:23.061Z · LW · GW
In this possible world, it is the case that "A" returns Y upon being given those same observations. But, the output of "A" when given those observations is a fixed computation, so you now need to reason about a possible world that is logically incoherent, given your knowledge that "A" in fact returns X. This possible world is, then, a logical counterfactual: a "possible world" that is logically incoherent.

Simpler solution: in that world, your code is instead A', which is exactly like A, except that it returns Y in this situation. This is the more general solution derived from Pearl's account of counterfactuals in domains with a finite number of variables (the "twin network construction").

Last year, my colleagues and I published a paper on Turing-complete counterfactual models ("causal probabilistic programming"), which details how to do this, and even gives executable code to play with, as well as a formal semantics. Have a look at our predator-prey example, a fully worked example of how to do this "counterfactual world is same except blah" construction.

Comment by Darmani on Programming Languages For AI · 2019-05-12T03:51:11.432Z · LW · GW

Hi, I'm a Ph. D. student at MIT in programming languages.

Your choice of names suggests that you're familiar with existing tactics languages. I don't see anything stopping you from implementing this as a library in Ltac, the tactics language associated with Coq.

I'm familiar with a lot of DSLs (here's umpteen of them: ). I've never heard of one designed before they had an idea what the engine would be.

E.g.: you can write a language for creating variants of minimax algorithms, or a language for doing feature extraction for writing heuristic functions, but you wouldn't think to write either of those unless you knew how a chess AI worked. Without knowing that those are useful things, what's left? Abstract data types are sufficient for representing chess pieces cleanly. Maybe you'll decide to write concrete syntax for chess positions (e.g.: write a chess move as Nx6 and have the compiler parse it properly), but, putting aside how superficial that would be, you would do that in a language with extensible syntax (e.g.: Wyvern, Coq, Common Lisp), not a special "chess language."

The recent-ish development of probabilistic programming (hey, now there's a family of AI languages) is instructive: first was decades of people developing probabilistic models and inference/sampling algorithms, then came the idea to create a language for probabilistic models backed by an inference engine.

Comment by Darmani on How does OpenAI's language model affect our AI timeline estimates? · 2019-02-15T07:43:00.017Z · LW · GW

Something you learn pretty quickly in academia: don't trust the demos. Systems never work as well when you select the inputs freely (and, if they do, expect thorough proof). So, I wouldn't read too deeply into this yet; we don't know how good it actually is.

Comment by Darmani on 2018 AI Alignment Literature Review and Charity Comparison · 2018-12-27T02:10:25.201Z · LW · GW
The vast majority of discussion in this area seems to consist of people who are annoyed at ML systems are learning based on the data, rather than based on the prejudices/moral views of the writer.

While many writers may take this flawed view, there's also a very serious problem here.

Decision-making question: Let there be two actions A and ~A. Our goal is to obtain outcome G. If P(G | A) > P(G | ~A), should we do A?

The correct answer is “maybe.” All distributions of P(A,G) are consistent with scenarios in which doing A is the right answer, and scenarios in which it’s the wrong answer.

If you adopt a rule “do A, if P(G | A) > P(G | ~A)”, then you get AI systems which tell you never to go to the doctor, because people who go to the doctor are more likely to be sick. You may laugh, but I’ve actually seen an AI paper where a neural net for diagnosing diabetes was found to be checking every other diagnosis of the patient, in part because all diagnoses are correlated with doctor visits.

The moral of the story is that it is in general impossible to make decisions based purely on observational statistics. It comes down to the difference between P(G | A) and P(G | do(A)). The former is defined by counting the co-occurences of A and G; the latter is defined by writing G as a deterministic function of A (and other variables) plus random noise.

This is the real problem of bias: the decisions an AI makes may not actually produce the outcomes predicted by the data, because the data itself was influenced by previous decisions.

The third part of this slide deck explains the problem very well, with lots of references:

Source: I’m involved in a couple of causal inference projects.

Comment by Darmani on Overconfident talking down, humble or hostile talking up · 2018-12-01T05:55:55.137Z · LW · GW

And Paul Graham in Beating the Averages:

Comment by Darmani on Cause Awareness as a Factor against Cause Neutrality · 2018-08-31T02:40:07.586Z · LW · GW

I think you hit the kernel of the argument in the first paragraph: If you have an obscure pet cause, then chances are it's because you do have some special knowledge about the problem. The person visiting a random village might not, but the locals do, and hence this is a reason why local charity can be effective, particularly if you live in a remote area where the problems are not quantified (and are hence probably not reading this).

Comment by Darmani on Learning strategies and the Pokemon league parable · 2018-08-13T19:49:41.648Z · LW · GW

Put that in your post! I got what you're saying way better after reading that.

Comment by Darmani on Learning strategies and the Pokemon league parable · 2018-08-12T17:39:09.538Z · LW · GW

I'm confused about whether you're talking about "learning things specifically to solve a problem" (which I've seen called "pull-based learning"), or "learning things by doing projects" (i.e.: project-based learning). The former differs from the "waterfall method" ("push-based learning") only in the sequence and selection: it's just the difference between doing a Scala tutorial because you want to learn Scala, vs. because you just got put on a project that uses Scala (and hence you can skip parts of the tutorial the project doesn't use).

For actual PBL: I am a PBL skeptic. I've seen so many people consider it self-evident that learning physics by building a catapult is superior to doing textbook problems that I wrote a blog post to highlight some of the major downsides: . I've seen it become a fad, but I've not seen the After I wrote the blog post, I had a lot of people tell me about their negative experiences with PBL. One that stands out is a guy who took a PBL MOOC on driverless cars, and didn't like it because they spent too much time learning about how to use some special pieces of software rather than anything fundamental or transferable.

Quick summary:

Advantages of PBL:

  • More motivating to some
  • Includes all aspects of practice needed in performance (e.g.: does not omit the skill of integrating many smaller skills together)


  • Does not naturally lead to correct sequencing of knowledge
  • Not optimized for rapid learning; does not teach subskills independently
  • May omit skills which are useful for compressing knowledge, but not directly useful in practice (e.g.: learning chord structure makes it easier to memorize songs, but is not directly used in performing music)
  • May include overly-specific, non-reusable knowledge

I don't think PBL works very efficiently. I think it can produce a lot of successful practitioners, but have trouble seeing how it could produce someone able to push the boundaries of a field. I will gladly pay $10 to anyone who can give me an example of someone well-regarded in mathematics (e.g.: multiple publications in top journals in the past decade, where this person was the primary contributor) who acquired their mathematics chiefly by PBL (i.e.: not studying mathematics except for what is needed to work on a specific problem, concurrently with working on the problem).

Comment by Darmani on Apptimize -- rationalist startup hiring engineers · 2015-01-15T22:50:39.257Z · LW · GW

It's more like the Crockford book -- a set of best practices. We use a fairly functional style without a lot of moving parts that makes Java very pleasant to work with. You will not find a SingletonFactoryObserverBridge at this company.

Comment by Darmani on Apptimize -- rationalist startup hiring engineers · 2015-01-12T23:14:35.237Z · LW · GW

Yep. The first thing we do is have a conversation where we look for the 6 company values. Another of them is "commitment," which includes both ownership and grit.

Comment by Darmani on Post ridiculous munchkin ideas! · 2013-05-12T09:43:26.807Z · LW · GW

You mean, a lot of cool mathematicians are eastern European. But Terry Tao and Shinichi Mochizuki are not.

Comment by Darmani on Weekly LW Meetups: Austin, Berlin, Cambridge UK, Champaign IL, Durham NC (2), Washington DC · 2012-11-03T09:11:15.170Z · LW · GW

Chris Olah and I (Jimmy Koppel) are both Thiel Fellows and avid Less Wrongers. We'd be happy to answer any questions about the program.

Comment by Darmani on Does anyone know any kid geniuses? · 2012-03-28T14:25:52.019Z · LW · GW

I know at least four people who started college by age 15. They're not "kid" geniuses anymore though -- the youngest is 16 and slowly going through college part-time, while the oldest is in his 30s and a full math professor at Arizona.

I don't know about the upbringing of the other three, but one attended a program where taking classes mutliple grade-levels ahead is the norm (though no-one else learned calculus in 3rd grade), and attended Canada/USA Mathcamp during the summers of his undergrad.

I second the Olympiads. Terry Tao famously represented Australia at the IMO at age 10, so he's definitely old enough.

Comment by Darmani on Biased Pandemic · 2012-03-13T04:49:29.868Z · LW · GW

With a sufficiently strong player, Arkham Horror is a one player game which seven people play.

Comment by Darmani on Diseased disciplines: the strange case of the inverted chart · 2012-02-05T16:43:04.559Z · LW · GW

There is a very healthy (and mathematical) subdiscipline of software engineering, applied programming languages. My favorite software-engineering paper, Type-Based Access Control in Data-Centric Systems, comes with a verified proof that, in the system it presents, data-access violations (i.e.: privacy bugs) are impossible.

This is my own research area ( ), but my belief that this was a healthy part of a diseased discipline is a large part of the reason I accepted the position.

Comment by Darmani on Completeness, incompleteness, and what it all means: first versus second order logic · 2012-01-27T16:57:08.815Z · LW · GW

Yes, but the point is that we are learning features from empirical observations, not using some magic deduction system that our computers don't have access to. That may only be one bit of information, but it's a very important bit. This skips over the mysterious part in the exact same way that "electrical engineering" doesn't answer "How does a CPU work?" -- it tells you where to look to learn more.

I know far less about empirical mathematics than about logic. The only thing along these lines I'm familiar with is Douglas Lenat's Automated Mathematician (which is only semi-automated). A quick search for "automated mathematician" on Google Scholar gives a lot of more recent work, including a 2002 book called "Automated theory formation in pure mathematics."

Comment by Darmani on Completeness, incompleteness, and what it all means: first versus second order logic · 2012-01-25T02:35:59.558Z · LW · GW

We form beliefs about mathematics the same way we form beliefs about everything else: heuristic-based learning algorithms. We typically accept things based on intuition and inductive inference until trained to rely on proof instead. There is nothing stopping a computer from forming mathematical beliefs based on statistical inference rather than logical inference.

Have a look at experimental mathematics or probabilistic number theory for some related material.

Comment by Darmani on Completeness, incompleteness, and what it all means: first versus second order logic · 2012-01-20T03:18:51.177Z · LW · GW

Computers can prove everything about integers that we can. I don't see a problem here.

Comment by Darmani on Completeness, incompleteness, and what it all means: first versus second order logic · 2012-01-19T23:22:52.110Z · LW · GW

The argument wasn't specific to ZFC or HOL, it was intended to apply to any system that can have a proof checker.

Pointing out the Gödelian limitations of all systems with recursively enumerable axioms doesn't seem like much of criticism of the system of nth-order logic I mentioned. Now I have less of an idea of what you're trying to say.

By the way, I think he's using "full model" to mean "standard model." Presumably, the standard integers are the standard model that satisfies the Peano axioms, while nonstandard integers are any other satisfying model (see ).

Comment by Darmani on Completeness, incompleteness, and what it all means: first versus second order logic · 2012-01-19T16:55:44.786Z · LW · GW

If I understand correctly, you are saying that higher order logic cannot prove all theorems about the integers that ZFC can. That's a very uninteresting statement. Since higher order logic was proven consistent* with ZFC, it is strictly weaker. Second order logic, is, of course, strictly weaker than 4th order logic, which is strictly weaker than 6th order logic, and so on, and is thus much weaker than higher-order logic.

I've never heard it claimed that second-order logic has a unique model of the standard integers. Actually, I've never heard of the standard integers -- do you mean a unique standard model of the integers? I hope not, as we actually can get a unique standard model of the integers in a system with machine-checkable proofs. See "To Truth Through Proof" by Peter Andrews. It's omitted in the Google Books preview, but I believe the proof is on page 327; i lent out my copy and cannot check. (It, naturally, does not have a unique general model, so this not of huge practical significance.)

* I have not actually read that, and should not really say that. However, type theory with an axiom of infinity, which is strictly stronger than type theory without an axiom of infinity, which can express all statements of higher-order logic, has been proven consistent. Also, any proof in higher order logic can be trivially converted into a proof of nth-order logic for some n, which can be shown consistent in (n+2)th-order logic.

Comment by Darmani on Completeness, incompleteness, and what it all means: first versus second order logic · 2012-01-17T03:22:51.112Z · LW · GW

Proofs in second-order logic work the exact same way as proofs in first-order logic: You prove a sentence by beginning with axioms, and construct the sentence using inference rules. In first-order logic, you have individuals, functions (from individuals to individuals), terms, and predicates (loosely speaking, functions from individuals to truth values), but may only quantify over individuals. In second-order logic, you may also quantify over predicates and functions. In third-order logic, you add functions of functions of individuals, and, in fourth-order logic, the ability to quantify over them. This continues all the way up to omega-eth order logic (a.k.a.: higher-order logic), where you may use functions of arbitrary orders. The axioms and inference rules are the same as in first-order logic.

Wait, I said nothing about sets above. Sets are no problem: a set containing certain elements is equivalent to a predicate which only returns true on those elements.

I also lied about it being the same as first-order logic -- a couple are added. One very useful axiom scheme is comprehension, which roughly means that you can find a predicate equivalent to any formula. You can think of this as being an axiom schema of first-order logic, except that, since it cannot be stated until fourth-order logic, it contains no axioms in first-order logic.

(My formal logic training is primarily in Church's theory of types, which is very similar to higher-order logic [though superficially extremely different]. I probably mixed-up terminology somewhere in the above.)

Comment by Darmani on [Link] Duolingo · 2012-01-05T21:41:39.959Z · LW · GW

I used Duolingo for a few hours on its first day. (I used to TA for Luis, which helps for getting private invites, at least by knowing to sign up immediately.)

I've basically just gone through passing out of German lessons. This basically consists of taking a 20 question test, in which I translate sentences like "The woman drinks with her cat." and pray I don't make typos on three questions and have to start over. Except that all too often I give correct translations, but their checker isn't attuned to the flexibilities of German word ordering, or I use a different word for "chair." They said they'd teach it the distinction between "essen" ("to eat" for humans) and "fressen" ("to eat" for animals) so that their quizzes would stop recommending wrong answers, but I'm skeptical. I did another one just now, and it now seems to accept answers off by one character. I noticed this in a listening exercise not because I made a typo, but because the word for "is" is approximately homonymous with the word for "eats."

Oh, apparently Duolingo has something to do with translating the web, rather than just going through a bunch of German 1-level exercises. Maybe I have to repeat the above for the remaining 45 lessons before I see an option to do that.