1. 5

    @bytemyapp can I have your feedback on this? From your book and talks, you seem to have a good experience on Haskell and teaching it. This seem to be relevant to any Haskell leaner.

    1. 5

      Probably meant to ping @bitemyapp.

    1. 6
      1. 2

        Someone on HN linked to the story of JPB meeting his partner, Cynthia Horner: Act Three, When Worlds Collide (Audio version). He wrote about her here, including a eulogy for her.

        Some of the most touching pieces I’ve ever read. Most definitely worth the read.

        Rest in peace John.

        1. 11

          As far as I can tell, this is a revival of dwm’s tags/views model.

          While, apparently, many dwm users use tags as if they are workspaces, that is only a fraction of their potential; and, when used properly, they can offer a workflow identical (from my perspective) to the one mentioned in the post.

          cf. tags are not workspaces.

          This is not to say that the author is wrong or is stealing and should give credit or anything like that. It is only to suggest that this paradigm has been known and is available in some window managers.

          Now, here’s where my knowledge of the subject gets a little thin. Where dwm supports this paradigm, I am unsure as to whether or not its many derivatives do (e.g., awesomewm, xmonad, etc.). I’d be interested in hearing from those users if this type of configuration is possible (presumably, anything is possible in xmonad since it’s really just a WM library and you can have whatever logic you’re willing to program, but I more meant, well-supported and easy to achieve through minor configuration changes).

          1. 4

            Awesome supported this, I believe. I remember having Win+[1-9] set to switch between tags, and when I would accidentally hold control when switching I would get windows from both tags!

            I like the idea of this, but I struggle with the execution when bringing in another tag causes overlaps or forces my current workspace to rearrange. For example, if I had chat and a browser open together taking up most of the screen while dealing with some operational issue, adding the editor group/tag to the screen would either overlap (if things were floating) or rearrange/resize existing windows (if some kind of tiling).

            To those that use the group/tagging feature in the way described in the post, how do you deal with the overlap or resizing issue?

            1. 1

              I fix the areas, so I don’t say «give me also group X», I say «please put group X in this subarea (and — in majority of cases — remove everything else from this subarea) without touching the rest of my screen»

              1. 1

                I have pretty much the exact shortcuts you describe. I use tiling mode almost exclusively, so I expect it when I look at two at once. It seems totally normal. I also have super + J and K for moving windows up and down in the current order.

              2. 3

                I’m not running xmonad at the moment, but it seems like xmonad-contrib has a XMonad.Actions.TagWindows module that does this.

                1. 3

                  dwm’s tags are indeed capable of handling that workflow I describe in this post, and even more IIRC. My first experience with groups came with cwm which lets you add windows to a group. Doing so would automatically remove the window from any other groups. With dwm, a single window can have multiple tags, thus allowing finer control over your task set, and which application to bring back and forth. This might be a little more complex to manage though, as you are responsible from adding AND removing windows from tags. Automatic removal from groups is, to me, the best compromise between workspace and tags.

                1. 1

                  I don’t live in the GTA anymore, but I’d be down to attend whenever I’m around.

                  1. 1

                    Dave also gave a talk on Whiley last year: David Pearce - What does the Future of Programming Look Like? (demo at the 11:25 mark).

                    1. 2

                      Enjoyed watching, thanks for sharing!

                      1. 3

                        Thanks for your great work on Oil!

                        On a somewhat unrelated note, I really like the simplicity of Oil’s website. Is the source code used for generating it open source?

                        1. 3

                          Glad it’s appreciated!

                          I haven’t released the site’s code… it’s a pretty messy mix of shell, Python, Make, markdown, and some of my own tools for generating shell snippets and syntax highlighting (with pygments). And of course there HTML, CSS, and JS which I cobbled together over the years. Copied and pasted from different projects.

                          Ironically it’s a testament to both the power of the Unix philosophy and the messiness. On the one hand, I think it produces a pretty good result with a low amount of development effort. On the other hand, I don’t think anybody could maintain it besides me :-/

                          Hopefully I’ll be able to port most of it to Oil at some point far in the future :) Combining shell, Make, and Python into the same language would be really useful, but it’s of course a lot of work. If nothing else it’s a good use case for taking the Unix philosophy pretty far.

                          1. 1

                            Haha that’s interesting :) And I agree with you on the power and messiness of the Unix philosphy.

                            Thanks for the explanations, and I look forward to whatever may come of it later in the future!

                            1. 1

                              Disagree with the messiness being because of the unix philosophy…

                              You can hack things together in any language. The difference with unix is you end up with ad hoc scripts. It’s possible to make sure your scripts are useful as standalone items and document them.

                              1. 2

                                That’s a fair argument I suppose, but to be honest, personally I haven’t found myself reusing my scripts a ton over the years. Sure, there’s definitely been some cases, but I’ve found that usually my use cases tend to not generalize too well and thus I don’t end up reusing all that much. So, for me, the drawbacks of using typical scripting languages (weird semantics, lack of proper types and a type system) usually outweigh the benefits in the context of the Unix philosophy.

                                That’s with usual scripting languages though. One thing I’ve been trying recently and has turned out to be interesting is using Haskell for scripting as well, and not just for larger programs. It seems to give me a nice balance between composability from the Unix philosophy and maintenance of my sanity by having Haskell’s awesome type system at hand. I’m thinking of forcing myself to exclusively use Haskell along with Turtle as my scripting language for a while and see how far I can push it and how it compares to “traditional” scripting languages.

                                1. 2

                                  To be clearer, my point is somewhat orthogonal to making standalone scripts and documenting them.

                                  It’s more about “language cacophony”. Shell and Python work pretty well together, but shell and make don’t. They awkwardly encroach on each others’ territory, both semantically and syntactically. But I can’t just choose one or the other – I need Make for incremental builds of my blog.

                                  The soup of document formats has a lot of downsides too. But I think it’s the best tool for the job or I wouldn’t use this.

                                  Also, I think reuse is somewhat overrated, although reuse in Unix is different than say reuse in Python or Java.

                                  I quoted Knuth on the subject in this post: http://www.oilshell.org/blog/2016/12/27.html

                                  I would also say that attempting to “reuse” makefiles is mostly folly. Even shell has limited opportunities for use. The way I “reuse code in shell” is to write a standalone Python script that can be called from multiple scripts.

                          1. 1

                            How does this website manage to break back-swipe functionality so badly? If I scroll down past the first section, attempting to swipe back results in some sort of insane JavaScript shit going on and preventing me from actually going back to where I was. Even pop-ups don’t manage to be this annoying. Besides this being an insane choice on the part of the page developers (provided it’s intentional), it also insane that mobilesafari allows this behavior.

                            1. 1

                              It’s a behaviour I’ve seen far too frequently, especially in JS-based slide presentation frameworks.

                              What’s likely happening is that behind the scenes they’re manipulating the browser’s history state when you scroll down to a new section. Upon scrolling to each section, they add the id of that section (e.g. #introduction, or #tutorial) to the tab’s history, probably using history.pushState(). That’s why when you do a ‘back’ operation, instead of coming back here to Lobsters, your browser instead pops one of those additional history items off of the history stack. It’s easier to see this happening with a browser that shows the complete url (including its /#tutorial part). They should’ve instead used history.replaceState() to avoid adding extraneous history items for each of the sections you scroll past.

                            1. 23

                              compsci would be appropriate. If there’s a significant number of people reading about compsci who don’t want to read about plt or vice-versa, speak now or forever hold your whitepapers.

                              1. 3

                                I’d like to see compsci used for something that is theoretically focused but used in conjunction with a “modifier”, like ai, or networking, or plt, or algorithms. But maybe I just think of tags differently than others…

                                1. 3

                                  I, too, would love me a plt tag. It would nicely complement formalmethods.

                                  1. 3

                                    What this tells me is I need to find and post more compsci articles that aren’t also about plt.

                                    1. 3

                                      Yes please.

                                      (I’m a computer scientist by day)

                                      1. 2

                                        I’d love a specific PLT tag.

                                        1. 1

                                          For clarity, do you mean reply to this post to say ‘yes please’ (in which case: ‘yes please’), or do you mean reply and/or upvote the OP?

                                          1. 1

                                            Anything, really.

                                          2. 1

                                            There have been a couple people people asking for this - if you see this, could you expand on why you want a tag that’s specifically separate from compsci?

                                            1. 7

                                              Here are some highly-rated Lobsters posts about compsci but not plt:

                                              Here are some highly rated posts where plt may be a good fit:

                                              The way I see it, practices, programming, and compsci are very broad catch-alls for cases where we don’t have enough density to make a dedicated subtopic. python, networking, and ai are all subtopics of programming. compilers and formalmethods are subtopics of compsci. I think there’s probably more people interested in PLT than Formal Methods here, so plt would be a useful subtopic.

                                              1. 3

                                                I’ve added a plt tag with the description “Programming language theory, types, design”.

                                          1. 2

                                            Great article!

                                            Also, a heads up that the two local links at the beginning of the post are broken.

                                            1. 2

                                              Thanks! I will fix that as soon as I can.

                                            1. 26

                                              I’m planning the hosting migration for Lobsters as the torch passes to me. Huge thanks to @alynpost for providing hosting and helping with the setup.

                                              I finished my first week at Recurse Center. It’s a wonderful community. I’ve worked on my solitaire solver, built a planck keyboard, and paired with folks on rails and git.

                                              This week I’m adding hspec and quickcheck (my nemesis - I can’t quite get how arbitrary, Gen, and property fit together) to the solitaire solver to drive out the four bugs I’ve found in the last few days. I’m also bringing Barnacles up-to-date with the Lobsters codebase as part of a deep dive into the Lobsters codebase to ensure I’m very comfortable with it.

                                              1. 3

                                                First of all, thank you so much for keeping the community running! I think there is no way to be grateful enough to volunteer efforts like this one.

                                                Also, on a more mundane side note, how difficult is to build a Planck? How are you liking it up to now?

                                                1. 5

                                                  It was very easy. It is my third soldering project - the first was a little $10 RadioShack kit that didn’t work and I couldn’t fix. The second was an Ergodox that I think had one or two solders I had to reflow. This had zero soldering errors. There’s several unedited videos of builds on YouTube.

                                                  I was down with the flu after I finished, so today will be my first day using it. I’m adopting a Norman layout, which I previously used on the Ergodox.

                                                  1. 1

                                                    I’ve built one recently as well, they’re really not too hard to solder, bearing in mind I hadn’t soldered in years. Typing on it right now, use it in lectures because it’s quiet - much nicer than a laptop keyboard :D

                                                  2. 3

                                                    First, thanks for stepping up for the community.

                                                    Secondly, about your issue with QuickCheck, Have you seen The Design and Use of QuickCheck tutorial? I found it helpful when I was reading up on QuickCheck a while back.

                                                    1. 3

                                                      Yes, though I failed to follow it in my admittedly sleep-addled state. I plan on giving it another try alongside HPFFP.

                                                  1. 2

                                                    This blog defines the difference between TDD and Design By Contract as a matter of whether errors are returned or thrown/asserted uncaught.

                                                    Where does this end though? At some point you accept user input that may not meet invariants you’ve specified, and your software probably shouldn’t just die every time.

                                                    There is a lot more nuance, but I’m not sure how to make it simple.

                                                    1. 6

                                                      I’d simplify it as “contracts are a property of your code, while TDD is a testing technique.” They’d be orthogonal.

                                                      TDD just boils down to “Write your tests before your code”. While agile gurus think it’s only unit tests, there’s nothing stopping you from TDDing with property tests, fuzzers, etc. Using contracts would actually make TDD more useful, since you can use the contracts to generate your tests!

                                                      At some point you accept user input that may not meet invariants you’ve specified, and your software probably shouldn’t just die every time.

                                                      I’d imagine you’d only pass parsed/validated input to your functions with contracts. You should be isolating user input anyway; contracts just give you an extra sanity check.

                                                      1. 4

                                                        I’d imagine you’d only pass parsed/validated input to your functions with contracts. You should be isolating user input anyway; contracts just give you an extra sanity check.

                                                        Yes, that’s the idea with DbC. Each model class provides adequate queries (non-side-effecting methods that return a value) for checking the validity of the data it needs to work with. Those queries are used in the preconditions of the class’s commands (side-effecting methods that don’t return anything but mutate local state). So, it would be the responsibility of the caller to make sure the precondition is satisfied before calling a command; and in turn, it’s the responsibility of the callee to ensure its postcondition holds given valid input.

                                                        With that in mind, you do DbC in your core model classes, and in your outward facing interfaces you’d do defensive programming (i.e. using if statements or switch statements) to validate user input and only call the models when the input is valid.

                                                      2. 4

                                                        At some point you accept user input that may not meet invariants you’ve specified, and your software probably shouldn’t just die every time.

                                                        For that point (for discussion purposes let’s call that point the function “sanitize”) your precondition assert is the loosest possible “assert(true)”

                                                        ie. You must accept all inputs the world can throw at you.

                                                        The postcondition for “sanitize” must be strict.

                                                        Now anything downstream of “sanitize” can and should have much stricter preconditions…. but those preconditions must be supersets of “sanitize”’s postconditions.

                                                        ie. Sanitizes postconditions imply that the downstream preconditions will hold.

                                                        You then hit sanitize with targeted unit tests and fuzzers and make damn sure it does it’s job.

                                                        Because if it doesn’t, your only real remedy is to deliver a fixed version of the software. So the sooner you discover that, the better.

                                                        Think about it…

                                                        If “sanitize” allows unclean inputs through… all bets are off.

                                                        The result may be a crash, or worse, subtle sporadic unreproducible errors, or worse subtle data corruption, or worse a security breach.

                                                        No matter which of those horrid choices eventuate… the symptoms will only be apparent way downstream of the cause (sanitize failing to do it’s job), and usually out in the field on the customers site.

                                                        If your precondition assert kills the system displaying a stack trace…. you can find and fix the bug before the software leaves the test rack.

                                                        1. 3

                                                          Author here of original post, you hit the nail on the head. I have a much older post describing this though you did an excellent job. I call this writing software in the shape of an egg. I feel this is a simple and highy effective technique that has simply been lost in the commercial development space. It works for any kind of software, from GUI to server.

                                                          1. 3

                                                            Ps: While I disagree with you that DbC replaces TDD…. Please don’t let that tiny disagreement dissuade anybody.

                                                            /u/mempko is entirely correct that DbC is extremely important and his post are adding great value to the conversation.

                                                            PPs: You’re right about the bugs being “between the units”, but the solution isn’t to throw the TDD baby out with that bath water.

                                                            Use DbC to create what JB Rainsberger calls Collaboration Tests.

                                                            Here is a snippet from a talk I give my colleagues… Pay particular attention to the part on services.

                                                            They may all be functions…. but Pure, Stateful, Services and I/O functions are very different sorts of functions requiring very different sort of tests.

                                                            Pure Functions

                                                            • A function that modifies nothing and always returns the same answer given the same parameters is called a pure function.

                                                            Stateful Functions

                                                            • Stateful functions results depend on some hidden internal state, or as a side effect modify some hidden internal state.

                                                            However, unlike a service, if you can set up exactly the same starting state, the stateful function will have exactly the same behaviour every time.

                                                            Services

                                                            • A service function is one whose full effect, and precise result, varies with things like timing and inputs and threads and loads in a too complex a manner to be specified in a simple test.

                                                            Testing PURE functions

                                                            Pure functions have many nice mathematical properties and are the easiest to test, to analyse, to reuse and to optimize.

                                                            Actively move as much code as possible into pure functions!

                                                            “const” is a keyword that always make me relax and feel less stressed. “const” is a remarkable powerful statement. Use it where ever possible.

                                                            Tests of pure functions are all about the results, never about functions they may invoke. ie. Never mock a pure subfunction that a pure function may use for implementation. Use the real one.

                                                            Testing Stateful functions

                                                            Often a stateful function can be refactored into a pure function where ….

                                                            • the state is passed in as a const parameter, and…
                                                            • the result can be assigned to the state.

                                                            The best use for stateful functions is to encapsulate a bundle of related state (into a class). These functions (or methods) should guarantee that required relationships (class invariants) between those items are ensured.

                                                            Where you have a collection of functions (or methods) encapsulating state (or a class) the best unit testing strategy is…

                                                            • Construct the object (possibly via a common test fixture).
                                                            • Propagate the object to the required state via a public method (which has been tested in some other test)
                                                            • Invoke the stateful function under test.
                                                            • Verify the result.
                                                            • Discard the object (possibly via a common tear down function).
                                                            • Keep your tests independent, DO NOT succumb to the temptation to reuse this object in a subsequent test. Fragility and complexity lies that way.

                                                            The best measure of the “Goodness” of the unit test suite is how well does it do at Defect Localization.

                                                            ie. Very few tests should fail if you have introduced a bug, and by just looking at the test case name and stack trace you should be able to tell you exactly where what is broken.

                                                            DO NOT assert on private, hidden state of the implementation, otherwise you couple your test to that particular implementation and representation, rather than the desired behaviour of the class.

                                                            Testing Services

                                                            Testing services is all about testing interface specifications . The services dependencies (unless PURE) must be explicitly cut and controlled by the test harness.

                                                            We have had a strong natural inclination to test whether “client” calls “service(…)” correctly by letting “client” call “service(…)” and seeing if the right thing happened.

                                                            However, this mostly tests whether the compiler can correctly invoke functions (yup, it can) rather than whether “client” and “service(…)” agree on the interface.

                                                            Code grown and tested in this manner is fragile and unreusable as it “grew up together” (Connascent coupling). All kinds of implicit, hidden, undocumented coupling and preconditions may exist.

                                                            We need to explicitly test our conformance to interfaces, and rely on the compiler to be correct.

                                                            When testing the Client….

                                                            • Does the client make valid requests to the service? (Use the exactly the services preconditions to check this! Pull them out as a separate function “service_name_pre()”)
                                                            • Can the client handle every response from the service permitted by the interface?

                                                            When testing the Service….

                                                            • Can the service handle every request permitted by the interface? (Fuzz the inputs, you should either get a precondition failure or a pass, nothing else!)
                                                            • Can the service be induced to make every response listed in the interface specification?

                                                            Think of the services post conditions as a region of the output space. Can you induce the service to generate points scattered over a substantial portion of that space (especially boundaries and corners)? Can your client handle all those points?

                                                      1. 5

                                                        I am writing an MUA with ncurses inspired by mutt. I wanted my first project in Rust to be a dive into the language. My goals for now are:

                                                        • separate the backend and UI as much as possible so that you’re not locked in the TUI
                                                        • a sane configuration UX (unlike mutt)
                                                        • use threads when appropriate

                                                        pipe dreams:

                                                        • should be extensible with plugins if there are any features that fit with the API
                                                        • should have as many features as mutt

                                                        The UI is pretty rudimentary so far; just an index and pager (not shown). ncurses is a pain to work with, I must say. I might look into the panel library since I think it has good platform support.

                                                        I’m still working on the library part, I have implemented mail backends as traits but have only Maildir for now. I believe when I finish the ‘check for new mails on a different thread’ part the library will only have mail composition left unimplemented as far as necessary features go. I wrote my own parsers with nom which I might publish separately later on.

                                                        I still haven’t made my repo public because It is not close to being finished, it’s a lot of work. I don’t think having an unfinished repo public is a good idea, what do you think? (I also use my emails for testing which I think should be replaced with something more public.)

                                                        1. 1

                                                          Nice project! I’d definitely like to take a look at your code base if you make it public :)

                                                          I don’t see why developing in the open would be problematic, especially if the software is to be eventually released as “open source” or free software. Though as you mentioned you should definitely remove your private emails before putting it out there.

                                                          1. 1

                                                            Thanks a lot! It will be GPLv3, but I’d like to release it when it’s ready for an alpha or beta version. For now there’s no basic functionality other than reading e-mails, and since I’m in the design process still I guess it’s not ready for co-operative developing. So publishing it will be only for read-only in-progress code.

                                                            1. 1

                                                              Glad to hear that you’ll GPLv3 it!

                                                              And you have a reasonable point about being in the design process. It’d be great if you could document your design decisions. We need more docs :) Good luck!

                                                        1. 4

                                                          I can’t up vote this based on the color scheme alone.

                                                          1. 3

                                                            It’s already more readable than majority of the websites I see these days:

                                                            • Good contrast
                                                            • Readable font, not thin and not too small
                                                            • Reasonable line-height (not crammed vertically)
                                                            • Reasonable line width
                                                            1. 2

                                                              I was skeptical of your comment, until I clicked the link.

                                                              And the color settings are marked !important so you can’t even override them very easily. Just why?

                                                              1. 1

                                                                Just because…

                                                                main { background-color: #fff !important; opacity: 1; padding: 2rem; box-sizing: border-box; }

                                                              1. 1

                                                                Hokay, so cool, vim has sessions. That’s sounds like a good idea. I wonder what’s in the emacs package archive that does that?

                                                                desktop+           melpa      Handle special buffers when saving & restoring sessions
                                                                elscreen           melpa      Emacs window session manager
                                                                escreen            melpa      emacs window session manager
                                                                minimal-session... melpa      Very lean session saver
                                                                modtime-skip-mode  melpa      Minor mode for disabling modtime and supersession checks on files.
                                                                persistent-scratch melpa      Preserve the scratch buffer across Emacs sessions
                                                                psession           melpa      Persistent save of elisp objects.
                                                                remember-last-t... melpa      Remember the last used theme between sessions.
                                                                save-visited-files melpa      save opened files across sessions
                                                                session            melpa      use variables, registers and buffer places across sessions
                                                                term+mux           melpa      term+ terminal multiplexer and session management
                                                                tramp-term         melpa      Automatic setup of directory tracking in ssh sessions.
                                                                

                                                                Also the builtin desktop.el package does that sort of thing. Some of the above are enhancements of desktop.el

                                                                I wonder which of those are best. I will explore and report back…

                                                                1. 1

                                                                  The builtin desktop.el seems to do what I what. Restores, files and frames.

                                                                  Can do it all the time or on demand.

                                                                  1. 1

                                                                    There’s also persp-mode, which I’ve been using for a while (via doom-emacs), and it’s quite nice.

                                                                  1. 4

                                                                    As a fellow Xfce user, I think this is a nice idea. Have you tried bringing it to the attention of the Xfce community and/or filing a bug report on the issue tracker?

                                                                    Edit: There’s a proposal on the Xfce Design SIG page for merging some of the settings panels a few years back. You may want to reference that as well.

                                                                    1. 3

                                                                      Yes, I have seen the proposal, there is at least some overlap! I think I will do a proper write-up and a real proposal, I’m currently looking for some early feedback from users to add some polish, that’s why I’m publishing these things.

                                                                      1. 1

                                                                        Looks all good to me.

                                                                        My recommendation would be to talk to the devs ASAP. You already have enough ideas, you need to identify potential roadblocks now.

                                                                    1. 17

                                                                      Just to underscore the lesson here: understanding your business requirements can substantially reduce cost of development.

                                                                      Instead of wasting time hunting down leaks in Valgrind and programming defensively and doing all that good stuff, they did some easy calculations estimating leak occurrence and just baked in a factor-of-safety.

                                                                      Oftentimes, these sorts of “shortcuts” are left on the table by developers who prefer to live in theory instead of sullying their hands with the messy but lax world of business requirements.

                                                                      1. 19

                                                                        Of course, being military and a missile… they will no doubt develop a longer range version using the same code after that programmer has left…….

                                                                        …and then wonder why it suddenly deviated from course killing whatever was unfortunate enough to be in the wrong place.

                                                                        1. 8

                                                                          This.

                                                                          In fact, this basically happened: The Explosion of the Ariane 5 back in June 1996. Luckily Ariane 5 was an unmanned rocket and no human lives were lost, but “the destroyed rocket and its cargo were valued at $500 million”.

                                                                          1. 2
                                                                            No. Not this.

                                                                            The internal SRI software exception was caused during execution of a data conversion from 64-bit floating point to 16-bit signed integer value. The floating point number which was converted had a value greater than what could be represented by a 16-bit signed integer.

                                                                            short i6(double x) { return (short)x; }
                                                                            

                                                                            Well, no shit.

                                                                            Indeed doing work you don’t need to (like memory management in a missile) is the exact sort of thing that caused this kind of bug, not the reverse like you’re suggesting.

                                                                            1. 2

                                                                              Did you read the report of the Inquiry Board mentioned in the page I linked? If not, I suggest you do.

                                                                              I was not arguing whether or not it’s safe to convert double to short like that, or whether or not you should do dynamic memory allocation in a safety critical system.

                                                                              The point my parent comment was making (and what I was referring to by This) was: when someone does stupid risky shit like letting everything leak and then trying to justify or compensate for it by doubling the maximum amount of leak possible based on the maximum flight time of a particular device, they’re gonna be in serious trouble if when that code is carelessly reused in a future version of that device with different specs and requirements (e.g. longer flight time, etc).

                                                                              The Ariane 5 incident which I linked is the exact same scenario: they reused arguably badly written code from the previous Ariane 4 rocket, without verifying and making sure that all of the assumptions made about the system in those pieces of code still hold for Ariane 5.

                                                                              I’m not going to quote the entire report, but here are some relevant excerpts:

                                                                              • The alignment function is operative for 50 seconds after starting of the Flight Mode of the SRIs which occurs at H0 - 3 seconds for Ariane 5. Consequently, when lift-off occurs, the function continues for approx. 40 seconds of flight. This time sequence is based on a requirement of Ariane 4 and is not required for Ariane 5.
                                                                              • The value of BH was much higher than expected because the early part of the trajectory of Ariane 5 differs from that of Ariane 4 and results in considerably higher horizontal velocity values.

                                                                              The same requirement does not apply to Ariane 5, which has a different preparation sequence and it was maintained for commonality reasons, presumably based on the view that, unless proven necessary, it was not wise to make changes in software which worked well on Ariane 4.

                                                                              p) Ariane 5 has a high initial acceleration and a trajectory which leads to a build-up of horizontal velocity which is five times more rapid than for Ariane 4. The higher horizontal velocity of Ariane 5 generated, within the 40-second timeframe, the excessive value which caused the inertial system computers to cease operation.

                                                                              1. 1

                                                                                I’m not going to quote the entire report, but here are some relevant excerpts

                                                                                Except they’re not relevant.

                                                                                The relevant bits are the recommendations, which don’t recommend code-reuse as being a factor, but here’s my favourite recommendation:

                                                                                no software function should run during flight unless it is needed.

                                                                                which supports my assertion, and the original assertion: Don’t free memory if you don’t need to reclaim it.

                                                                                1. 1

                                                                                  Except they’re not relevant.

                                                                                  They’re relevant to the point I was making.

                                                                                  I’m not opposed to code reuse; not when it’s done properly. You want to bring over code from the previous rocket into the new one? That’s perfectly fine if you can justify the existence of every function you’re bringing (which is what you’re saying), and if it doesn’t interfere with the spec of your new system. They shouldn’t have brought over that function from Ariane 4 into Ariane 5 where it wasn’t needed; and they failed to make sure that what they’re bringing in is consistent with the specs of the new rocket.

                                                                        2. 5

                                                                          On the other hand, taking these shortcuts without also understanding why the leaks occur can have potentially catastrophic consequences. Feynman links improperly thought out safety factors to the Challenger explosion.

                                                                          1. 2

                                                                            Although a good point, I’ll note that both Ada and C++ have ways to reclaim memory as objects go out of scope. It’s just a declaration with a little effort structuring the program. That would also be a baked-in factor of safety much easier than tons of work in Valgrind. They can combine that with a WCET analysis [which they already do] to make sure things stay within timing bounds.

                                                                            Far as using something like in OP, people do both in bootstrapping without a GC and using certain kinds of formal analyses. In both, they know they can try to run both to see if the tool succeeds or crashes (eg out of memory). If they crash, we’re probably doing it wrong and rewrite it somehow. Or just do smaller pieces at a time with a clean slate between them. Not so different from memory pools Ada can use for the above stuff.

                                                                          1. 12

                                                                            I’ve started learning Lean, working my way through the Introduction to Lean tutorial.

                                                                            Quoting their about page linked above,

                                                                            Lean is a new open source theorem prover being developed at Microsoft Research, and its standard library at Carnegie Mellon University. Lean aims to bridge the gap between interactive and automated theorem proving, by situating automated tools and methods in a framework that supports user interaction and the construction of fully specified axiomatic proofs. The goal is to support both mathematical reasoning and reasoning about complex systems, and to verify claims in both domains.

                                                                            I also recommend watching Leonardo de Moura’s talks, From Z3 to Lean, Efficient Verification and The Lean Theorem Prover, for more about Lean.

                                                                            1. 6

                                                                              I’m interested in seeing a submission of your overall perspective of the Lean experience applied to practical examples after you’ve dug into it long enough. Especially compared to what you think the cost/benefits are versus methods that are lightweight (Alloy or TLA+), heavyweight (Coq or Isabelle), or programming-oriented (SPARK or Frama-C). Every experience report is potentially valuable.

                                                                              Maybe more so with you since your slides on Unit B were interesting. I’ll note that the interface/type-checking argument against TLA+ maybe not warranted. Maybe. TLA+ is often advocated as a supplement to coding something in a safe, programming language that lets you do things like that. As in, people who aren’t going to formally specify everything might use it as an extra tool on something that already checks interfaces. Turning it into a specification language with redundant features would be a drawback. You might be better off comparing to stuff aimed at fuller specifications such as Abstract State Machines, Event-B, VDM, or Z + SPIN/CSP as those were common in CompSci and industrial projects.

                                                                              1. 2

                                                                                I’m definitely thinking about writing up my experience with Lean once I’ve used it long enough.

                                                                                As for your comments on Unit-B, while I see where you’re coming from with your point about TLA+, I don’t think a nice type system is a redundant feature; especially if it’s advanced enough. Granted, I haven’t seriously TLA+ for anything yet; but one of the courses I’m taking at school this Fall uses it. So, I look forward to giving it a fair try and being able to better compare it with Unit-B.

                                                                                What I can say, though, is that TLA+‘s untyped logic seems to be quite nice in that it doesn’t tie your hands like a simple type system would. For instance, in TLA+ you could easily express heterogeneous sets (e.g. {5, {4}} is a set with an \Int and \set [\Int]) but whereas Event-B’s simple type system forbids you from doing that, Unit-B’s allows it via subtyping.

                                                                                Further, having a nice type system is quite beneficial:

                                                                                • Getting immediate feedback on your formulas before they’re even discharged to a solver or model checker. This speed would be invaluable if the method is to be integrated in everyday workflows.
                                                                                • Type-checking a specification can prevent you from spending time implementing an inconsistent spec. It is even more important considering that type-checking the implementation won’t reveal the same information. So, being able to quickly get feedback on your spec before going off spending time implementing it is really useful.

                                                                                Lastly, I’ve thought about writing up a detailed comparison of Unit-B with a few other methods of different shapes and sizes (Event-B, TLA+, Lean) by working through one or more examples in each. Hopefully I’ll be able to do that after Fall.

                                                                            1. 2

                                                                              I’ve used fastmail before and was generally quite happy. These days I run my own mail server. There are lots of resources around on how to setup a mail server on a VPS, if you like to go that path. You should check out Mailu too.