1. 1

    I did stop reading when I reached the common mis-attribution of who did the bulk of the work on the Apollo code.

    1. 4

      What’s the misattribution in question?

      1. 3

        Author here: would love to hear more on this? Fact-checking always appreciated. If you’re referring to Margaret Hamilton’s contribution, the article states her position as leading the team, which does not directly mean that she wrote the code in question. Fair enough, I’ll make note to add the actual author of the critical pieces as well.

        1. 1

          I have to get a good book on the Apollo Code (I bet someone here has a recommendation) but I recall that Hamilton was elevated to leadership position at a more mature stage of the project. Once you put a name to a project, you are making it about a personality (rather than the code) and the question of fair attribution comes up.

          1. 3

            I think “mis-attribution” is an overstatement. But it’s true that Hamilton did not singlehandedly write the AGC code (nor did anyone; it was a team effort). The single person who probably most deserves credit for the fault tolerance feature is probably MIT’s Hal Laning. He designed the executive and waitlist systems. Hamilton deserves as much credit as anyone, but I wish it was expressed that she was a member of a team rather than a one-person effort.

            1. 1

              @craigstuntz thanks for that reference! Is there a good book on the Apollo automation engineering efforts? I’m interested in both the hardware and software and not just the AGC but the whole of it.

              1. 2

                I can tell you about some books I’ve actually read; these might not be the best for your specific interests. “How Apollo Flew to the Moon,” by David Woods. But it doesn’t go into the AGC in minute detail. “The Saturn V F-1 Engine: Powering Apollo into History,” by Anthony Young, is good, but doesn’t cover controls at all. There are a couple of books specifically about the AGC which I haven’t read.

        2. 3

          You could just give him the specifics. Then he can update the article. I’m curious what yours are since I’ve read several different versions of the story.

          1. 2

            This story and the story of Rosalind Franklin are both curious to me. We could start a project - ideally primary sources - to do some archaeology. For DNA all I can think of papers. For the Apollo code it has to be early documentation - all US Gov docs have lists of contributors and responsible people.

            1. 5

              I was asking because I did it before to address the possibility that a bunch of people did work and she just put her name on it. She seems to have for her team. So, I started saying Hamilton’s team. The problem occurs enough that I started doing that in general.

              Now, as to Apollo, I did have some kind of paper that was specific. I faintly recall it saying they were responsible for one or two key modules but they did all the verification. They were the best at making robust software. So, if I’m remembering right, the paper talked like they were handed the code other people wrote to find and fix the errors on top of their own modules. That’s impressive. So is the stacks of spec and code in assembly in the picture. The “Lessons from Apollo” article here has a description of the environment and mindset that led to that as well. Later, she and another woman spent whole career developing CASE tools (HOS and 001 Toolkit) for designing systems with no interface errors that generated code for you. It was like binary trees, Prolog, and Occam combined which is why usability and performance sucked despite it succeeding on robustness and generality.

              So, that’s what I learned when I dug into it. If I get the papers again, I’ll send you the one with the attributions. No promises that I’m going to do another deep dive into that soon, though.

              1. 3

                That would be a very interesting project indeed! Part of the beauty and definitely one of the main reasons the Apollo program was so successful IMHO is specifically the way the work and communication was organized. To this day the project stands as a testament to how such a large-scale project should be carried out effectively. While I’m not privy to the inner working of NASA, there seems to be evidence that some of the organizational systems were lost later and this led to sever inefficiencies. It’s a pity, but luckily it offers us a wealth of learning opportunities.

                1. 2

                  On Hamilton’s side, it seemed like they mostly just let people do their work their own way. The work was also highly-valued and interesting. So, they came up with innovative solutions to their problems. This doesn’t usually happen in process-heavy or micro-managing environments.

        1. 8

          Turn off JS then? Isn’t this what a modern browser is by definition? A tool that executes arbitrary code from URLs I throw at it?

          1. 7

            I am one of those developers whom surfs the web with “javascript.options.wasm = false” and NoScript to block just about 99% of all websites from running any Javascript on my home-machine unless I explicitly turn it on. I’ve also worked on various networks where Javascript is just plain turned off and can’t be turned on by regular users. I’ve heard some, sadly confidential, war-stories that have led to these policies. They are similar in nature to what the author states in his Medium-post.

            If you want to run something, run it on your servers and get off my laptop, phone, tv or even production-machines. Those are mine and if your website can’t handle it, then your website is simply terrible from a user experience viewpoint, dreadfully inefficient and doomed to come back hunting you when you are already in a bind because of an entirely different customer or issue. As a consequence of this way of thinking, a few web-driven systems I wrote more than a decade ago, are still live and going strong without a single security incident and without any performance issues while at the same time reaping the benefits of the better hardware they’ve been migrated to over the years.

            Therefore it is still my firm belief that a browser is primarily a tool to display content from random URLs I throw at it and not an application platform which executes code from the URLs thrown at it.

            1. 3

              That’s a fine and valid viewpoint to have, and you are more than welcome to disable JS. But as a person who wants to use the web as an application platform, are you suggesting that browsers should neglect people like myself? I don’t really understand what your complaint is.

              1. 2

                But as a person who wants to use the web as an application platform, are you suggesting that browsers should neglect people like myself?

                I don’t think so. But using Web Applications should be opt-in, not opt-out.

                1. 3

                  Exactly.

                  There are just to many issues with JavaScript-based web-applications. For example: Performance (technical and non-technical). Accessibility (blind people perceive your site through a 1x40 or 2x80 Braille-character-display matrix, so essentially 1/2 or 2 lines on a terminal). Usability (see gmail’s pop-out feature which misses from by far most modern web-applications and you get it almost for free if you just see the web as a fancy document-delivery/viewing system). Our social status as developers as perceived by the masses: They think that everything is broken, slow and unstable, not because they can make a logical argument, but because they “feel” (in multiple ways) that it is so. And many more.

                  However the author’s focus is on security. I totally get where the author is coming from with his “The web is still a weapon”-posts. If I put off my developer-goggles and look through a user’s eyes it sure feels like it is all designed to be used as one. He can definitely state his case in a better way, although I think that showing that you can interact with an intranet through a third-party javascript makes the underlying problems, and therefore the message too, very clear.

                  It also aligns with the CIA’s Timeless tips for sabotage which you can read on that link.

                  We should think about this very carefully, despite the emotionally inflammatory speech which often accompanies these types of discussions.

                  1. 1

                    He can definitely state his case in a better way

                    I sincerely welcome suggestions.

              2. 1

                by the same stretch of logic you could claim any limited subset of functionality is the only things computers should do in the name of varying forms of “security.”

                perhaps something like: “The computer is a tool for doing computation not displaying things to me and potentially warping my view of reality with incorrect information or emotionally inflammatory speech. This is why I have removed any form of internet connectivity.”

              3. 7

                This is not a bug and it’s not RCE. JavaScript and headers are red herrings here. If you request some URL from a server, you’re going to receive what that server chooses to send you, with or without a browser. There’s a risk in that to be sure, but it’s true by design.

                1. 3

                  Turn off your network and you should eliminate the threat. Turn your computer off completely for a safer mitigation.

                1. 2

                  Here’s another intro from Adam Langley which helped me a lot.

                  1. 1

                    Shoot, I really had my hopes up, here. Thought it was going to be about my favorite VAX editor.

                    1. 6

                      My favorite approach to this problem is in TLA+, and it always finds the solution.

                      1. 4

                        And here’s the Alloy way of doing it!

                        1. 2

                          Both of these are awesome! :) Thanks for the links!

                      1. 3

                        The single best advice I got from this talk is that I should watch this talk:

                        Matt Might - Winning the War on Error Solving the Halting Problem and Curing Cancer

                        Which was worth it, actually.

                        1. 8

                          I didn’t post this, but since it’s my talk I’d be happy to chat about it here.

                          1. 3

                            The “correct” pronunciation of SQLite (source: I attended a lecture by Dr. Richard Hipp) is S-Q-L-ite”

                            1. 2

                              “Type theory is a theory of computation that classifies programs according to their behavior, rather than their structure. Types are themselves programs whose values stand for specifications of program equivalence.”

                              I had to stop right there. Most of us in imperative languages using types use them or structure. Especially in terms of structs or objects. This says types have nothing to do with structure. Makes me wonder if that’s inaccurate or type theory doesn’t cover what imperative/OOP programmers normally call types. Or do they have another definition of structure outside the mainstream definition. I have a feeling a certain amount of confusion that happens in type theory discussions might have started right there.

                              Regarding the RedPRL prover, one person on it is the person who wrote Practical Foundations for Programming Languages. People might find those interesting by themselves.

                              1. 8

                                An example of something that structural interpretations of types have trouble with is equality of functions. Many programming languages have a very limited or outright broken notion of function equality, but it’s important if you want to prove a program conforms to a specification. It’s also important to have a language for what function equality means. Are a quicksort and a merge sort equal functions?

                                Bob Harper is both the author of this blog post and PFPL.

                                1. 3

                                  Type theory is a theory of computation that classifies programs according to their behavior, rather than their structure. Types are themselves programs whose values stand for specifications of program equivalence.

                                  I took “behaviour” to mean the ‘externally visible’ aspects of a value/program. For example, that something with function type Foo -> Bar can be called with a Foo value to produce a Bar value; that something with product type Foo * Bar can be projected to give both a Foo value and a Bar value; that something with sum type Foo + Bar can be projected to give either a Foo value or a Bar value but not both; etc.

                                  I took “structure” to mean the ‘internal’ aspects of a value/program. For example, the different parts it may be made out of, any functions/computations that it uses (delayed or already completed), the syntax it was written as, etc.

                                  In this sense:

                                  • We can make these “behaviours” as complex and precise as we like, by making the types more complex and precise. For example, with dependent pairs and functions we can encode arbitrarily complicated mathematical relationships between values, inputs/outputs, etc.

                                  • We can’t use types to classify the “structure” of a value/program.

                                  As a provocative example, we can think about a value of product type Foo * Bar. We might think that the type tells us some ‘structural’ properties about the value, like “it contains a Foo” and “it contains a Bar”, but that’s not quite right. All we know is the “behaviour”, that we can project the value to get a Foo and a Bar, but we don’t know what will happen during that process. For all we know, the value might be an integer plumbed into an ‘unpairing’ function, like with Cantor pairing or Goedel numbering. Should we say that such a value “contains” a Foo and a Bar? What if that same integer is also used elsewhere to generate a boolean, a list of bitmaps, etc.? We’d at least have to weaken what we think of as “containing” or “structure”.

                                  One example which I’ve heard discussed about type theory as opposed to set theory, is that in set theory we can (and very often do) ask whether a value is contained in a set, e.g. foo ∈ {foo, bar} and foo ∈ {high, low} are propositions which may be true or false. In type theory we can’t ask whether a value has a particular type, e.g. foo : (Foo * Bar) and foo : (High * Low) aren’t true/false propositions; they’re logical statements, which may be well-typed (valid) or ill-typed (invalid).

                                  This is important for the “behaviour” vs “structure” distinction, since in set theory we can distinguish between isomorphic sets, e.g. {foo, bar} and {high, low} are isomorphic (they “behave the same”), but the foo ∈ x predicate is true for one and false for the other (they’re structured differently). Since type theory doesn’t let us do this, isomorphic types are indistinguishable (within the theory), so we can only reason about “behaviour”. This has connotations for modularity, reusability, optimisations, etc.

                                  1. 3

                                    You’re right that the types discussed in here are not being used in the same way that types in many c likes primarily use them. The goal is essentially different in scope. C types mostly capture the size of memory required for allocation of something. Types in the type theory sense can capture this idea, but can also contain much richer and complicated concepts in the types themselves.

                                    also aside from PFPL Bob Harper is known for his work on SML and LF

                                    1. 2

                                      Yeah I don’t think you can do type theoretic proofs in say C# without a lot of work with interfaces and tuples. After all you don’t even have “Product and Sum types”. Heck it’s even hard right now in F# due to the fact that you have to explicitly name everything.

                                      So for example say you have a function which takes a tuple of an int and (bool or string) and returns either a tuple of an int and a bool or and int an a string. int * (bool | string) -> (int * bool) | (int * string) //this would be the function signature. More amusingly

                                      Old * (dumb | fat) -> (Old * dumb) | (Old | fat) // if I’m old and (dumb or fat) this implies I’m either old and dumb or old and fat

                                      This is equivalent to A ^ (B v C) = (A ^ B) v (A ^ C). in logical propositions.

                                      we can the write a function which takes an int and either a bool or a string, and return an int and bool, or an int and string and we know we have covered all possible return combinations.

                                      In this way the function signature, the “Type” represents the lemma and then function itself exists as proof.

                                      This as I understand it is merely the beginning of the whole thing. There’s a good computerphile video on the subject.

                                    1. 12

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

                                              I was thinking “Huh?” then saw you posted most of it a year or two ago. I’d say keep them coming but stay on practical papers or examples where possible. Shows relevance for readers who are curious about stuff or waiting until it’s practical to their needs. That’s been my strategy except occasional research result that was pretty interesting. Most of those get low reads/votes. So, I say stick with stuff where even the abstract tells you something practical and neat.

                                            1. 2

                                              This is awesome

                                              One solution is to guard the value (second m) with a dynamic check. Another is to apply type tailoring to regexp-match!

                                              If I understand this correctly, the type tailored code does exactly that, but is syntactically elided at each use of the macro. Right? Could this be extended to statically enforce constraints without run-time checks?

                                              1. 3

                                                I don’t think that’s right. As I understand it, the type errors are statically checked. The dynamic check is necessary in Typed Racket today due to designed-in limitations of the type checker, similar to how you must check for null in Java (although Racket does better than Java, IMHO, in that it conservatively rejects the unsafe code). The type tailored solution statically shows that the code rejected by Typed Racket is safe at compile time.

                                                1. 3

                                                  The type errors are checked statically, but only because the macro call expands to code that rebuilds the match function’s result. That checking has runtime overhead, including the list constructor and the if/error checks. What I’m asking is whether that cost can be eliminated.

                                                  Surely some of it can: The occurrence typing could learn more about composites, so that you could traverse the list, asserting things along the way, without recreating the list.

                                                  But some of it is less clear: Could you avoid the if/error checks completely with more knowledge of the relationship between the pattern and the return value? Could you do that only with a call-site macro, or do you need co-operation from the called code?

                                                  1. 2

                                                    I am admittedly hitting the bounds of my Racket knowledge here (I’ve written one or two macros in my life, so the bounds aren’t very big!), but as I understand the article and the macro it does statically use the value of the regex in the call, e.g.:

                                                    smart-match rejects some programs that Typed Racket would accept, yet evaluate to runtime errors — for instance, (second (regexp-match "r" "racket")).

                                                    So I think the answer is yes, you do have enough knowledge to do what you ask with a less trivial macro, but I’ll repeat that I’m out of my depth here!

                                                    The return of their function is always a list, so I don’t see how you avoid that constructor as written. It would be neat if you could say, “Well, the only thing done with that list is to call second, so….” but that seems to be outside of the scope of the macro, if I understand correctly? I guess if all this concerned you then you could change the macro definition to say you wanted a specific group as an argument and then it might work?

                                                    1. 3

                                                      I don’t see how you avoid that constructor as written.

                                                      There are two calls to the list constructor. One inside the match function that produces the result. And the other is in the macro expansion that takes that result and recreates it (exactly as is!) but throws a runtime-error if it violates some static assumption.

                                                      I’m proposing replacing this:

                                                      (list
                                                        (car m)
                                                        #,@(for/list ([i (in-range num-groups)])
                                                             #`(or (list-ref m (+ 1 #,i))
                                                                   (error 'smart-match))))
                                                      

                                                      with this:

                                                      #,@(for ([i (in-range num-groups)])
                                                           #`(or (list-ref m (+ 1 #,i))
                                                                 (error 'smart-match))))
                                                      

                                                      Note the outer list constructor is gone, but more importantly the functional ‘for/list’ is replaced by an imperative ‘for’ that returns void.

                                                      For an even simpler example of the sort of thing I’m interested in, consider this:

                                                      (if (pair? x) (car x))
                                                      

                                                      vs this:

                                                      (if (pair? x) (unsafe-car x))
                                                      

                                                      The first will check pair? twice. The second won’t.

                                                      Presumably you could macro expand to unsafe calls, or the compiler could use constant propagation or global value numbering to eliminate the duplicate check. So my question (to the authors I guess): How can this “type tailoring” technique eliminate any check at all? Not just N -> 1, but 1 -> 0 checks.

                                                      1. 3

                                                        We want to convince Typed Racket’s type checker that the result of regexp-match has a second element.

                                                        smart-match does this by unrolling the result into a list so that the number of results is syntactically apparent. For the given example, here is the actual program that runs after the smart-match macro expands:

                                                        (let ([m
                                                               (let ([m (regexp-match "(a*)b" "aaabbb")])
                                                                 (if m
                                                                     (list ; list constructor called with two arguments
                                                                      (car m)
                                                                      (or (list-ref m (+ 1 0))
                                                                          (error 'smart-match)))
                                                                     m))])
                                                          (when m
                                                            (string-length (second m))))
                                                        

                                                        Typed Racket knows that it is for sure safe to call second because it sees the list constructor called with two arguments.

                                                        Your suggestion won’t quite work because for returns void, so the macro would try to splice void into the outer syntax object (#,@ is shorthand for unquote splicing), resulting in an error. (You can try it out, the post contains all the code needed to run the example).

                                                        The actual implementation probably does use unsafe operators as you suggested though. (Actually, Typed Racket might automatically apply that optimization itself.)

                                                        1. 1

                                                          Thanks for posting this! I searched both your blog post and your paper for the expanded macro and I failed to find it. It would be a nice thing to put in the appendix of the post. Thanks for writing it; I enjoyed the paper!

                                              1. 2

                                                Intentional is Charles Simonyi’s company. They make very powerful DSL tools.If one wanted to say, “What will be the next Microsoft Excel in terms of bringing programming to the masses?” it would be a good place to look.

                                                1. 3

                                                  Note the first paragraph, which I’m paraphrasing here:

                                                  “UPDATE: The story which follows was rushed to press before the facts were known and is wrong. The headline was clickbait speculation from the outset.”

                                                  1. 2

                                                    Dammit. Thanks for the clarification!

                                                  1. 3

                                                    COBOL will outlive us all. In ten-thousand years, when humanity has been replaced by gengineered simuloids, there will still be agents dedicated to maintaining their ancient COBOL subsystems.

                                                    1. 6

                                                      There was a joke in the Y2K era about a programmer who was terrified about the Y2K bug and had himself cryogenically frozen to wait out the tech apocalypse. 8000 years later he was revived into a techno-utopian future society. The first thing they said to him was, “We understand you know COBOL…”

                                                      1. 1

                                                        Good thing his cryopod wasn’t affected! Or maybe it was, and that’s why he required manual revival…

                                                    1. 1

                                                      Is using Orleans as a .NET Core cache a good idea? It has totally different architecture and durability goals than Redis (the default cache).

                                                      1. 3

                                                        Pretty good article which I mostly agree with aside from his assertions about most of curl’s bugs not being C-centric.

                                                        1. 1

                                                          …but a disproportionate share of the CVE bugs are, FWIW.

                                                          1. 6

                                                            My favorite two-short-article introduction to machine learning is A Few Useful Things to Know about Machine Learning [PDF] on the more positive side, and the paper you link on the more cautionary side.

                                                            1. 5

                                                              Probably the best title for any paper I have ever seen.

                                                              In one brief phrase you understand what he is going to say, and with brief reflection, you know in your gut he is right.

                                                              1. 2

                                                                Oh that’s one I haven’t seen before.

                                                                § 2.2 is a huge thing I’ve seen a lot of programmers get into the trap of simply because they forgot about what their model actually means.

                                                                Thanks for that!

                                                              1. 1

                                                                There may be a line somewhere between “free for all” and “ban these sites”. What if there were a feature which would flag a site as “suspicious” and encourage submitters to verify stories elsewhere or look for a better source when submitting?