Threads for hcs

  1. 1

    Here’s a link to the ACM DL page for the paper instead of directly to PDF: https://dl.acm.org/doi/10.1145/51607.51614

    1. 5

      Reading through some e-graph papers, most excited I’ve been about CS in a while (just learned about them yesterday). Progressing through Crafting Interpreters, going to also start re-reading ZACH-LIKE.

      1. 2

        I’ve somehow not heard of e-graphs, interesting! The end of the POPL 2021 presentation mentioned projects using egg that involved “Java testing” and “educational problems”, does anyone know what these are?

        1. 4

          Author here: those projects are a little old, I should update the list. The java testing was a course project and the education problems was a project that I don’t think went anywhere ultimately (I was not involved in either directly).

          1. 1

            Is anybody using this to implement the optimizer for a more-or-less general purpose programming language? (Instead of the standard approach of multiple different passes that must be ordered by hand.)

            1. 4

              The cranelift folks are exploring using an e-graph (based on egg) in their compiler: https://github.com/bytecodealliance/rfcs/pull/27

              1. 1

                Thanks for that reference. I’m looking forward to finding out how well this works in practice, for both code simplicity, and for performance.

                1. 1

                  I hadn’t seen that; very exciting!

                2. 3

                  I use egg in my implementation of Cammy. It is a short single-file optimizer with little magic.

                  The library and approach are fine, but the language needs to be intentionally designed for it.

                  1. 2

                    Thanks, I’ll take a look. In what sense does the language need to be intentionally designed for it?

                    1. 2

                      Cammy has trivial alpha- and eta-equivalence, and no lambda-abstractions. In fact, my jelly optimizer doesn’t know whether an atom refers to a builtin function or a composite. This was essential to getting equational reasoning which doesn’t need to manage scopes or shadowing. Also, Cammy is total and pure, so optimizations don’t have to speculate or otherwise be conditional on a context. Finally, Cammy’s textual syntax is a flavor of S-expressions which is parseable by Scheme, OCaml, and egg’s builtin SymbolLang, so I did not have to write a new AST type in Rust.

            1. 8

              Under the “Object Oriented Programming” heading

              Luckily the industry doesn’t really use this term any more so we can ignore the changed meaning. The small club of people who still care can use it correctly, everybody else can carry on not using it. Just be aware when diving through the history books that it might mean “extreme late binding of all things” or it might mean “modules, but using the word class” depending on the age of the text.

              I’m not sure if this is a joke or not, but people still use OOP all the time and there’s no consensus whatsoever as to its meaning (although curiously just about everyone who uses one of the meaning seems to insist that everyone agrees with their definition, even though in a given thread multiple definitions will be espoused). Moreover, I’ve very rarely heard people define it in terms of binding time, but usually it’s one of “sending messages”, “encapsulation”, “inheritance/classes”, or so on. There are still plenty of outspoken OOP devotees, and the only thing they seem to agree on is an affinity for the name. The lack of clear consensus about the name makes for some incredibly unproductive conversations.

              1. 2

                I’m sure it’s a joke, but with some truth to it, in that we’re past peak OOP hype. Nonscientific but the ol’ ngram search matches my intuition pretty well that it was nigh-inescapable in the 90s, when it nearly always just meant “like C++ “ (and later Java into the 00s).

                (Final edit: granted this may be related to my own immaturity and poor book selection as I was learning programming from the mid 90s to mid 00s.)

                1. 1

                  “sending messages” is late binding, because the object will do whatever it does when I send the message, and so whatever you get passed at runtime determines what you call instead of some compile time or link time thing.

                1. 4

                  I’m reading through Crafting Interpreters on paper, currently Chapter 13 at the end of the first half’s treewalk interpreter. Partly because I like the writing, and find the material and form interesting, but mostly to build up some kind of intellectual momentum to get out of a mindless rut.

                  1. 1

                    In case you’re wondering, Bridgetown is a progressive site generator. You add content written in an author-friendly markup language like Markdown, alongside layouts and components using template syntax such as Liquid or ERB, and Bridgetown will then compile HTML, CSS, and JavaScript to an output website folder.

                    1. 1

                      The plan was to work on a submission for the GMTK game jam, but the theme this year – Roll of the Dice – hasn’t led me anywhere yet, 7 hours in (of 50).

                      1. 2

                        I firmly believe Formal Method advocates should aim for a more pragmatic approach and “play nice” with compilers and optimizers and Design by Contract and Unit Testing.

                        Let’s face it, writing a full postcondition is just plain a lot harder than writing the code itself.

                        However, writing a perhaps partial postcondition for a few compelling concrete test cases is usually pretty easy.

                        Instead of aiming for “proving” the programmer right or wrong, if they aimed instead for assisting the programmer as much as they can.

                        If formal methods acted like warnings on steroids (but with no false positives) and a boost for optimizers and a power up boost for internal precondition checks….

                        I can see a lot more adoption.

                        1. 3

                          Let’s face it, writing a full postcondition is just plain a lot harder than writing the code itself.

                          That’s not at all obviously true! We have many examples where it is false, and it’s probably false in general.

                          An example of this is are problems in NP. Problems that can be verified in polynomial time but whose solutions cannot be generated in polynomial time (assuming P!=NP, but in any case, even if P=NP the verification is still likely to be far easier).

                          Problems to do with concurrency are another example. There are models that are very simple to specify, but they result in thousands of tricky edge cases that need to be handled perfectly and that humans just don’t come up with on their own.

                          The real problem is that current tooling makes specifying models far too difficult. And even worse, they make knowing if you’ve specified the right mode quite tricky. This is probably a combination of having immature tools and having chosen the wrong formalism for expressing these models. A lot of logics look great at first but their semantics, particularly when it comes to reasoning across time, turn to be really tricky. We have some glimpses of how this can work with languages like Haskell or Isabelle in domains that can be modeled well and it’s beautiful. But there’s a long road from here to a point where we can express these postconditions in a more natural way and still reason about them automatically.

                          1. 6

                            You’re kinda illustrating @JohnCarter’s point here.

                            I’m not working over in CSAIL, but here in startupcanistan even having basic tooling around post-conditions in design-by-contract for things like “this function will never go negative when calculating a sum of credits”, “this function will always return a smaller value towards zero than its inputs”, “this function will return a URL that doesn’t have a query string with such-and-such values in it” would still be super helpful.

                            We’re trying to make a cup of tea, not boil the ocean. Until formal methods folks realize this, their entire field is of limited utility to practical, real-world software engineering outside of a handful of cases (say, writing a database engine).

                            1. 2

                              I’m going to recommend this great post about combining property based testing with contracts. If you can add the assertions for your pre and post conditions, through something like an assert statement in your language or some library support, you can use property based testing to at least generate a lot of inputs. And that’s more likely to find assertion failures than hand-writing test cases.

                              That’s one of the lightest-weight approaches for adding formal methods concepts to a real word project.

                              1. 1

                                Yes, actually from pre/post-conditions you can get 3 things:

                                • Support for generating random tests, similar to QuickCheck
                                • Verification at compile-time, like Dafny
                                • Fail-fast behavior at runtime, like Eiffel

                                The third item is really pragmatic and underappreciated. At runtime, a failed precondition should prevent a function/method from running. A failed postcondition should prevent the function from returning or writing its side effects. A huge class of software errors would disappear if software was written like this.

                                Probably, you can also get a fourth one, better static analyses (without going into full verification) and a fifth one (more efficient code, as discussed elsewhere in this thread).

                                It is unsurprising design-by-contract is so thorough as it is actually refinement types under disguise.

                                1. 2

                                  It is unsurprising design-by-contract is so thorough as it is actually refinement types under disguise.

                                  And refinement types are Hoare logic in disguise :)

                                  1. 1

                                    True! :)

                            2. 2

                              An example of this is are problems in NP. Problems that can be verified in polynomial time but whose solutions cannot be generated in polynomial time

                              Assuming P!=NP says nothing about the relative difficulty of writing the solver vs verifier, though. Or are you speaking metaphorically?

                              1. 1

                                Practically, most solvers for such problems include the verifier as part of the solver. So the solver tends to be (much) more complex. But yes, that’s just a rough example.

                              2. 2

                                We have many examples where it is false, and it’s probably false in general.

                                Really? Can I see those examples? I’d be really curious to some for something like https://github.com/seL4/seL4/blob/master/src/string.c

                                But I couldn’t see them from a quick dig around the repo.

                              3. 3

                                I totally agree. My personal interest is in how to bring formal methods to work, in whatever package is the most useful. There’s a term called “lightweight formal methods” which is similar in philosophy to what you’re talking about. Basically, take the ideas from formal methods, like invariants / properties / formal logic, but use them in a way that doesn’t require full math proof.

                                I think Amazon’s approach here is really promising. They took the theorems that would be proven in a verification effort, like refinement of a model, and instead used property-based testing to check for it. So the property isn’t proven, but they have some amount of confidence in it. They also found 16 bugs this way, before shipping. And isn’t that the end goal?

                                So yea. I think coming up with the right package of a lightweight, practical way to bring formal methods thinking to work is something that there’s demand for.

                                1. 2

                                  This is an interesting point. Do we need mathematical proof? Or can we use scientific proof? Mathematical proof’s epistemology for this domain is fairly straightforward (classical logic for constructive proofs over finite problems). Scientific proof is epistemologically far more fraught…but often a lot easier to produce since it is subject to further refutation.

                                  1. 2

                                    Yes definitely - tests are really a scientific / empirical activity. They are about observing what really happens, not just what the logical model says should happen. I would say the main difference between testing in software and actual scientific experiments though is that we don’t know how to talk about the statistical significance of individual test cases. At least I don’t. I’ve heard that the Cleanroom approach has some notion of statistics, but I’m honestly not familiar with it in detail.

                                    As far as which one is appropriate for software development. It could be contextual, but I pretty much solely focus on “business software,” or “regular” software, and for that I would say math proof is almost never necessary. It could be desired in certain cases, but even then I would only prove things about a model or a broad algorithm in general. Proofs at the implementation level are just extremely time consuming, even with things like proof assistants.

                                    So as a broad strategy, I think we (as an industry) have to get better at elevating testing to a point where we statistically know how effective a test suite is. And no, branch coverage is not what I’m talking about, since input data is really the coverage that we should really care about.

                                    1. 1

                                      I would say the main difference between testing in software and actual scientific experiments though is that we don’t know how to talk about the statistical significance of individual test cases.

                                      Statistical significance isn’t really the issue in most software tests because we set them up to be deterministic. Hypothesis testing is a means of working with randomness in observations. The issue is the selection of observations and test cases. This is true in biology or in software testing. Hypothesis testing is a tool for doing an individual observation, but the aggregate set of observations to run (the research program, more or less) doesn’t depend on that. I’ve written some stuff about this.

                                      I would say math proof is almost never necessary.

                                      I disagree. We depend on proofs heavily on a regular basis. Type systems are the most common example. But setting up a system where you control the flow of information to make certain states impossible is another. These aren’t comprehensive proofs, and they are often implicit, but they are properties we prove mathematically.

                                      branch coverage is not what I’m talking about, since input data is really the coverage that we should really care about.

                                      Mutation testing is the most defensible approach to coverage that I’ve seen: if you change the program, does the test suite start throwing errors. I also like property based testing because it gets humans out of the business of selecting test data individually.

                                      1. 1

                                        I also like property based testing because it gets humans out of the business of selecting test data individually.

                                        Unfortunately in practice I’ve found you have to spend a lot of time getting the data generator just right to cover an interesting enough set of inputs.

                                        1. 1

                                          You have probably used it far more in-depth than I have. I was mostly using it to generate fairly straightforward things like lists of a type.

                                        2. 1

                                          Re math proofs and necessity - I was moreso talking about a full proof for the functional correctness of an entire application. I think that is overkill in most cases. Not proofs in general, especially about smaller algorithms.

                                1. 7

                                  I wish there was also a Programming Languages Gym: a set of well-specified small languages with exhaustive test suites that anybody can implement as an exercise (e.g. in that language itself).

                                  1. 2

                                    I would love this. mal is the only one I’ve seen.

                                    1. 1

                                      There are some puzzle games that require making a recognizer for a language. Manufactoria comes to mind, it comes with a suite of tests, called in-game the “Malevolence Engine”, and it was recently remade. This gets bogged down in assuming the player isn’t already a programmer, and keeping things simple enough to work visually. I thought about trying to make a game with player-authored interpreters (old blog post), but haven’t yet cracked it. How to present the player with a specification that will not be boring or overwhelming to read through, but without having “figure out the spec” take away from the more interesting “implement the language”.

                                    1. 3

                                      I’m going to get some practice with the Godot game engine in preparation for the GMTK Game Jam this weekend. I finally forced myself through some tutorials last week, now I plan to reimplement an earlier puzzle, PrograMaze. That should be a simple starting point, and since 2017 I’ve come up with a few new mechanics to try.

                                      I’ve got heightened hopes after Speleomorph did well in the jam rankings (#1/75 for Design], 4 for Enjoyment, 11 overall). But that was a month long, and it took a lot of that month just to code and recode in raw JavaScript. I’m not going to have enough time to do anything worthwhile in a weekend for GMTK (and future jams) if I don’t pick up some more powerful tools. And it’ll be a huge help towards completing something hopefully salable down the road, it should especially help for collaboration (though Unity might have been a better choice for that).

                                      1. 1

                                        I tracked down this book because it was in the same series as Dahl, Dijkstra & Hoare Structured Programming but there was nearly no information about it online. It turns out to be a reference for translating between Algol 60 and Fortran II/IV, with details about the compilers for and capacity of different machines circa 1966. The main body is the “dictionary”, mapping syntax between the two languages.

                                        1. 1

                                          I’ll be putting the finishing touches on Speleomorph, my submission for the Metroidvania Month 16 game jam, which ends June 15th. I had hoped to get audio in there but a) I need more time to learn and debug Web Audio, b) I don’t think the loops I’ve written will hold up for a full play session.

                                          1. 2

                                            Continuing work on a game jam submission, due June 15. I’m getting to the point where there’s little more that’s essential to gameplay, mostly the tutorial, but also camera management and some infelicities in the control scheme. I need to take another crack at graphics (currently just solid squares everywhere) and try my hand at some music. It’s been a decade since I last wrote a song for a game jam, as a big game music fan I’m tentatively excited, but I’m inexperienced and it’s miserable to struggle with low skill. Same for graphics, I might resort to taking photos and processing them into 2D textures if I get too frustrated with drawing.

                                            1. 1

                                              Yet we do often subject ourselves to more frustration than is necessary. From the article:

                                              You solve a problem by taking a break, by letting something ruminate in your backbrain, by confabbing with someone else, by rubber-ducking it. Minds are weird and nonlinear, and so coding can be weird and nonlinear.

                                              I often manage to forget this in the heat of a work session. The transition from focused progress to unfocused rumination is necessary, but recognizing that is itself a change in approach. I might eventually figure it out after repeated hammering, but usually I’d have had the same insight with less frustration by stepping away earlier.

                                              On the other side, when I find myself unable to reengage with a project, sometimes this is because I’m subconsciously working through problems. One day I’ll suddenly know how all the pieces fit together, and then it’ll be hard to stop. I’d be less frustrated by the lack of progress if I treated this as a formal work mode, but it’s hard to distinguish from low motivation, burnout, or suppressed concrete problems.

                                              1. 1

                                                Working on a small game for the Metroidvania Month 16 jam. I think I have a fun puzzle-y mechanic in mind for the “shapeshifting” theme, just now getting the world design and progression together on index cards before I start coding a prototype.

                                                1. 1

                                                  I’ll be collecting more feedback on a little puzzle game I’ve been working on the last few weeks, got some family and friends trying it out.

                                                  Also I’m “scanning” a book via an extremely makeshift setup involving a pane of glass and a stack of cardboard boxes. The book is “Dictionary for Computer Languages” by Hans Breuer, it’s a 1966 reference for translating between Algol 60 and Fortran II and IV.

                                                  1. 1

                                                    Trying to get feedback on a short puzzle game I’ve been working on over the last two weeks. I’m pleased with the design, but I might be fooling myself that it’s comprehensible. (I’d post it here but I don’t want to burn too many first impressions just yet on this version, if anyone wants to try feel free to get in touch.)

                                                    1. 3

                                                      This reminds me of the Williams tube, one of the earliest computer memories, which used a CRT to store the bits: https://en.wikipedia.org/wiki/Williams_tube

                                                      1. 1

                                                        Indeed, the underlying physics is the same, although the timescales differ: https://en.m.wikipedia.org/wiki/Phosphorescence

                                                      1. 1

                                                        Prior art I had heard of: the five teaching languages created for the 2003 book How to Design Programs. Those five languages, which are subsets of Scheme, range from the “Beginning Student” language to the “Advanced Student” language.

                                                        According to section 2.4 of Hedy’s research paper, Hedy’s main innovation compared to How to Design Programs’s teaching languages is that across language levels, Hedy’s “syntax gradually changes, rather than being extended”.

                                                        1. 1

                                                          I worry that changing the language, instead of extending it, might lead to confusion when the student misremembers what level they’re working at, especially if they’d worked at a lower level for a while. That said, I really like this idea of motivating syntax, I’ll check out the paper (so far I only watched the introductory video on the site).

                                                        1. 2

                                                          with_addr (…) It lets us reconstitute provenance for the purposes of memory models / alias analysis

                                                          This makes my head hurt a bit, but… how does this work with custom allocators? For example what’s the provenance of a pointer to an arena-allocated object? Let’s say an arena allocated object was passed to some FFI and another function received that address back from FFI.

                                                          What is it supposed to do? arena_base.ptr.with_addr(the_object) ? Does that mess up any chance of optimising access to it?

                                                          Edit: I’m getting this wrong, aren’t I? When receiving a pointer from FFI, I’d get the full thing, not just the address…

                                                          1. 1

                                                            Yeah, FFI should be using full pointers that are in the form of (provenance, addr). The bare integer addresses are meant to exist only temporarily while you do pointer arithmetic.

                                                            The arena case is probably even trickier, because I’d expect it to use split_at_mut() when “allocating” a new object, and this gives two independent un-aliased pointers. These would be two independent objects from perspective of aliasing analysis. I don’t know if they’d be separate from CHERI perspective.

                                                            1. 2

                                                              These would be two independent objects from perspective of aliasing analysis. I don’t know if they’d be separate from CHERI perspective.

                                                              CHERI doesn’t provide a mechanism combining two capabilities. If you take a capability that covers a large range, you can subdivide it into two sub-ranges but if you want to be able to access the entire range then you must do so from a capability derived from the original, not from either of the sub-ranges.

                                                              1. 1

                                                                (I just learned about CHERI from this article and reading bits of this introduction (PDF) and the CHERI Rust dissertation (PDF).) I think you can always derive a valid pointer covering a smaller range from a valid larger one, so when the split is done (and the parent slice no longer exists) those slices could be constructed with pointers such that no aliasing between them could be possible. The dissertation mentions this in section 5.4.3.