1. 2

    A lot of comments focus on technical details, many of which I agree with (better IPC/messaging than what we have right now is the big one). But, we use our OS to do things - I’m more interested in the operating environment or shell rather than the low-level details. I recently asked: How might a future OS help us navigate the world?.

    Hopefully it will enhance our abilities to:

    • Process incoming information: ingest, relate
    • Understand information: query, navigate
    • Act in the world: schedule, plan, react

    When I’m using a computer to work (vs idly browsing), I typically have several different applications open and I am running through some workflow between them. These apps don’t usually know much about each other. Somehow my OS doesn’t even know which apps I usually open together and how I place them on the screen! I figure that’s the least it should do for me.

    A new shell should help me organize my tasks and coordinate applications. This requires a supporting ecosystem and incentives for apps to be less black-box, more toolbox - which many of the comments here are addressing. But what does it look like for the less technical end user?

    1. 1

      You might be interested in enso (nee Luna) and/or arcan-fe.

    1. 6

      This is partly what a recent paper & submission to lobste.rs, “Collapsing Towers of Interpreters”, Amin, Rompf, is about. Of course this is recent research so applying it will probably be an exercise.

      This is overkill for your use case as you’re not talking about many languages, just your one. Can you compile your program to C/C++/Go or whatever you’re most comfortable with rather than interpreting it?

      1. 2

        That paper looks like it would be very useful whether I implement it directly or not.

        My ultimate target now is simple bytecode for a unique platform. Compiling to C would mean creating a C-to-bytecode compiler too.

        1. 3

          You could perhaps implement a backend for LLVM or some other C compiler emitting to your custom platform. Then you’ll get the LLVM optimizations. I don’t know what your time/money budget is :)

          1. 4

            Yeah no,

            The paper you originally linked to actually is what I need and not overkill. It happens I am dealing with the “interpreter tower” that the paper references.

        2. 1

          That feel when people don’t have a ton of background on the project, but want to tell you that things don’t fit your use case anyway 🙄

          It’s like “rtfm”, but surprisingly even less valuable.

        1. 7

          This is a chance to get familiar with a newer and exciting language in the compile to Javascript world.

          Why Reason is always marketed as “language that compiles to javascript”? I thought it’s just alternative syntax for Ocaml (i.e. it rather compiles to Ocaml or its internal representation than JS), and that compilation to javascript is performed by Bucklescript, not Reason.

          What js-specific functionality it has, compared to plain Ocaml with Bucklescript? Maybe better integration with npm mentioned on website? Or [% … ] quasi-quotations allowing to embed raw js?

          Even Bucklescript website shows code examples in Reason. I’m confused.

          1. 5

            ReasonML is both a syntax and a default build chain relying on Bucklescript. You can use the syntax rewriter to build normal, binary libraries and executables via ocamlc and your build tool of choice.

            Bucklescript heavily integrates with the Javascript runtime - depending on your needs, you can cast directly between a javascript object and a type safe OCaml value. This is why ReasonML uses Bucklescript as the compiler: it makes it much easier to interop with existing JS. Compare to js_of_ocaml which compiles the OCaml runtime to JS (more or less) and makes no attempt to reconcile the difference.

            The only feature specific to ReasonML is the JSX rewriter (AFAIK) - that only works on ReasonML source, not OCaml.

            OCaml + Bucklescript + npm = (default ReasonML toolchain) - jsx

            1. 2

              Most tooling and libraries seem to build on the nodejs side of the ecosystem, meaning npm packages instead of opam, build scripts which only address javascript output, no native binaries.

              (I only glance over ReasonML documentation from time to time, not an active user)

            1. 5

              dgsh also provides an http server to map requests to commands and files: https://www2.dmst.aueb.gr/dds/sw/dgsh/dgsh-httpval.html

              Specify that a query, such as http://localhost:63001/server-bin/pstatus?id=4892, will run the ps(1) command for the specified process-id.

              dgsh-httpval -b ’server-bin/pstatus?id=%d:ps -p %d’

              Who needs Erlang/OTP when you have an OS to manage your processes? ;)

              1. 7

                I recommend looking for a University that does it to learn or work on one of their projects. I suspect it’s very helpful to have experienced people to help you through your first year or two of verifying anything significant.

                In any case, here’s a write-up from one of best in field with advice and one book reference. The other books people mention are Certified Programming with Dependent Types by Chlipala and Software Foundations. If picking based on tooling, Coq and HOL (esp Isabelle) are used on best projects in software with ACL2 being used most for hardware.

                It also helps to see what lightweight verification is like if you need some motivation, a fallback, or just tell you something aint worth proving. Alloy (see site) or TLA+ (learntla.com) are best for that imho.

                1. 2

                  Thanks Nick. I suspect it would be helpful to have experienced mentorship as well. It’s certainly a challenging - and large - area. Working with a University sounds like a great idea.

                  Thanks for the link! I suppose it’s time to get back to writing algorithms and proving things ;)

                  1. 4

                    Well, it might also help to read them to see what tools you even want to use. As always, I suggest something you will enjoy in a category with practical applications immediately or down the line. There’s more practical stuff now than ever. Formal methods still ain’t at Github’s level, though. Still more to do. :)

                    Here’s a few areas of research to consider for what to verify:

                    1. Obviously, a formal semantics, compiler, or optimization for a specific language worth the time. Rust and Nim come to mind. People also keep building important stuff in C++ which was only partly done. Haskell had one, formal semantics done but no verified compiler. Maybe a useful Scheme like Racket or Chicken.

                    2. Tooling for automated proof of safety, termination, and so on for programs in a language like above with minimal specs a la SPARK or Frama-C. Optionally working on SAT/SMT solvers to get such languages closer to 100% on more problems with less schemes like ghost code. There’s lots of potential there.

                    3. Verifying models used in actual languages for safe/effective concurrency (eg Eiffel SCOOP) and/or parallelism (eg Cray Chapel or Taft’s ParaSail). Possibly a mockup in existing language with macros of such features with verified translator to regular code.

                    4. Verifying client-server or peer-to-peer protocols that have a lot of uptake for various properties. Optionally, making something like Verdi that already does it easier to use for non-experts or increased automation.

                    5. Verifying important data structures and sequential algorithms for correctness. Just make sure there’s a C implementation with x86 and ARM7-9 compatibility. If it performs well, people can wrap it in any language with C FFI.

                    6. GUI’s and graphics stacks. That occasionally gets work but not much of it. Graphics drivers are notorious for crashing. Just automated verification of them for safety like Microsoft’s SLAM and no race conditions might be helpful. Fully verification of an OpenGL stack or something might also be interesting. For GUI’s, something like Nitpicker would be easy whereas for GUI programming a DSL compiling to major toolkit would be the route. Maybe an OpenCL model. Who knows.

                    7. Increasing usability, automation, and performance of any tool people have used to do anything on that the lists above. There’s already lots of people increasing their assurance. Cost of verification is a more important problem right now, though. The lightweight methods need more power. The heavyweight methods need more automation. I did speculate about and find a HOL-to-FOL translator used to do the latter once. That, the use of model-checkers to filter before proving, and results of SAT/SMT tooling in general suggest there’s lots of potential here.

                    So, there’s you some ideas that might have immediate or long-term impact on problems that matter. There should also be something in that list you find fun. Maybe also something you know a lot about already. That can help. Either should have potential for projects worth spending a lot of time on.

                    1. 2

                      Thanks for the list. Programming languages are interesting to me and partly what drives my interest here, especially tools like Disel.

                      I’m guessing #7, automation, will be increasingly interesting the further along I get here.

                    2. 4

                      If you’d like to practice on a juicy target, I invite you to join an effort to eradicate bugs in a database I’m working on in my free time, sled! It has a simple interface, but lots of optimizations that really need to be reliable. Nobody wants to use a database that very quickly deletes their data :P

                      I’ve been working extensively with property testing and a few tricks for shaking out interesting thread interleavings, and these approaches have yielded enough bugs to keep me busy for the last 6 months, but it’s time to really ramp up the rigor.

                      These are the approaches I believe will lead to the discovery of interesting bugs:

                      • formally specify the lock-free algorithms in use for the IO buffer and tree using TLA+, alloy, spin, iris etc… with the goal of identifying concerns that have not been considered in the implementation
                      • reproduce the functionality of quviq’s erlang PULSE scheduler using either ptrace or SCHED_FIFO/SCHED_RR in a test harness for performing parallel property testing as a rust library. Bring some of the awesome features of quviq’s quickcheck into the rust world.
                      • implement a concurrency testing library for rust that utilizes ptrace and z3 to get a nice user-friendly practical implementation of Maximal Causality Reduction to identify a minimal set of relevant interleaving schedules, and then use ptrace to schedule the threads according to the generated schedules to suss out crashes or violations of specified invariants.

                      Future directions include:

                      • building a versioned transactional store on top of sled
                      • building a horizontally scalable linearizable kv store on top of sled
                      • building a location-agnostic (phones, multi-dc, PoP’s) store powered by OT & CRDT’s on top of sled

                      The future focus on distributed systems will involve lots of interesting simulation, as well as an attempt to unify concurrency testing and distributed systems simulation. This is sort of a holy grail for me, and I hope to create tooling that lets people build significantly more reliable distributed systems, even more than the databases themselves.

                      Let me know if any of these directions sound like things you would be interested in collaborating on! You can find my email on github if so. Having this stuff on my github has resulted in a bunch of interesting people reaching out about jobs, and I haven’t been asked to do a single technical interview after referring companies to the project to see my output. This is a 100% non-commercial endeavor at this point, but I see it as earning interesting future job opportunities at the very least. I can’t tell you if commercial formal methods people will appreciate your work on these systems or not, but this is a real system that fills a real pain point (existing embedded db’s either have crappy read perf or crappy write perf, are generally confusing for people to configure, and often have poor consistency guarantees), and applying advanced testing techniques to this should actually save people from facing huge issues.

                      1. 1

                        I may have to dig with this. I find having practical examples to chew on while learning quite valuable. Your work looks great, congrats on your success!

                    3. 2

                      “I recommend looking for a University that does it to learn or work on one of their projects. I suspect it’s very helpful to have experienced people to help you through your first year or two of verifying anything significant.”

                      True, you can found some of the courses and lectures in a list.

                    1. 3

                      Don’t have experience with formal verification specifically, but some general advice:

                      1. Adjacent roles is good. Companies with more obscure technologies are often more willing to train, since they have no choice. And small startups will hire for much broader positions than the actual job posting, e.g. I was hired for backend skills but in practice I’m learning image processing as applied to gene sequencing.
                      2. Learn and blog is a fine thing too… if you have the time. I don’t, so tend to go for adjacent jobs if I’m interested in particular skillset (in this case, I wanted to learn scientific computing).

                      If you don’t have skills upfront, you also want resume that stresses your ability to learn quickly.

                      (Longer writeup here: https://codewithoutrules.com/2018/01/23/job-with-technology-you-dont-know/)

                      1. 1

                        Thanks! The tip for resumes is a good one. Sounds like you’re having fun learning in your new role.

                      1. 4

                        What kind of industrial jobs have you found that are centered on formal methods?

                        I was under the impression that that it would be a small part of any software development job.

                        For example, I read the article about Amazon using TLA+. I’m pretty sure they didn’t hire a bunch of people with formal methods experience. It sounds more like the senior engineers tried it, decided it was a good idea, and then taught/spread formal methods within the existing dev team.

                        Does anyone here use formal methods in their day job? If I had to guess, I would probably guess that less than 1% or even zero people reading this have applied formal methods to a piece of code that ships (I certainly haven’t). It seems like it’s more in the research phase, whereas you are talking about getting an “adjacent role at a company”. I could be wrong though.

                        http://lamport.azurewebsites.net/tla/amazon.html

                        1. 5

                          I have! It was a really powerful tool in shipping code, but just that- a tool. It definitely wasn’t what I was hired to do, and in fact it wasn’t even expected at all: I just wedged it in and found it worked.

                          To my understanding, most of the people whose job is specifically “use formal methods” are mostly in either hardware or academia.

                          1. 7

                            To my understanding, most of the people whose job is specifically “use formal methods” are mostly in either hardware or academia.

                            That’s probably most of them, especially hardware if you want an industry job. Besides hardware companies using formal methods, there’s a little ecosystem of middleware companies selling the formal-methods tools, mainly to hardware companies. I’ve run across a handful elsewhere though. Financial companies occasionally advertise specifically formal-methods jobs (example). I’ve also seen ads on occasion from aerospace companies (no link handy). There’s Microsoft Research as well, which might even employ more people working on formal methods full-time than any single university does, but MSR is kind of an honorary member of academia.

                            1. 3

                              There’s Microsoft Research as well, which might even employ more people working on formal methods full-time than any single university does

                              Maaaaaaaaaaaybe MIT is comparable, but that’s the only candidate I can think of. Outside of academia you also have INRIA, which is a French national research agency that produces a lot of stuff in formal methods too. Coincidentally enough, MSR and INRIA run a joint lab, which IIRC is where all the work in TLA+ happens.

                              1. 5

                                Calling INRIA outside academia is… at least, a slight bit misleading, while technically true. People get PhDs at INRIA (technically they are issued by some other university, but their advisor and research is done at INRIA), and people who are at INRIA sometimes lecture at regular universities (I’m not actually sure how common this is, but talked to someone just a few months ago who was talking about doing this).

                                1. 1

                                  Did not know this. Thanks for the correction!

                            2. 1

                              Awesome! How did you learn about formal methods – through school or self-taught?

                              This kind of confirms what I was thinking. If you want to use formal methods at a software company, it’s unlikely you’ll be “hired in” for that. It’s more like you’re already a developer on a team, and you have to take the initiative to use it and teach your coworkers it and sell management on its utility.

                            3. 4

                              Data61 down here in Australia are often hiring Proof Engineers:

                              https://ts.data61.csiro.au/jobs/proof-engineers2015

                              1. 4

                                In industry I have have used Agda to prove code correct instead of testing it, because the tooling made it quicker to do than using property tests in Haskell.

                                1. 4

                                  Whaaaaat!? You may be first person I’ve seen say it was quicker to prove code correct than use testing approaches. Makes me wonder if the code you were working on was a lot of straight-forward math in a functional style or something. You did mention Haskell. In any case, that sounds like it’s worth a write-up and submission to Lobsters for being practical, efficient, and about Agda in industry.

                              2. 3

                                What kind of industrial jobs have you found that are centered on formal methods?… It seems like it’s more in the research phase, whereas you are talking about getting an “adjacent role at a company”.

                                As you suggest, not many :). Mostly hardware companies as others have pointed out. I was including industrial research without being explicit, so Microsoft Research and some other places, e.g. Galois count in my book. I think, in addition to the other suggestions here, I will start going through conference and journal publications to find some more leads.

                                1. 2

                                  One easy trick is just going through the formal methods submissions in the publications looking at their University or corporate affiliation. I’ve also submitted quite a few tagged with formal methods here that you can just use Lobsters search for. You can also look for tool vendors such as company doing Atlier-B to see who their customers are. ProB is another with Z and TLA+ support. For instance, ProofPower led me to QinetiQ. AbsInt owns CompCert. Rosu’s group is doing Runtime Verification Inc. Smartcard vendors like Infineon or Gemalto use them a lot for higher-security stuff. Kesterel Institute is an old one that many outsourced to.

                                  Just looking at the tools, papers, and reference sections takes you a lot of places. Helps to know the jargon that pops up a lot, too. Examples are Common Criteria EAL7 or DO-178B (recently DO-178C) since they often sold as a tool to aid certification. Or “formal methods industry.”

                              1. 4

                                why not use

                                $ some –command; osascript -e ‘display notification “Done!!” with title “Done!”’

                                on your mac? (there are equivalents for gnome, kde, X etc.)

                                1. 6

                                  This is actually superior because, I’m guessing, aa probably won’t work with things like shell aliases, so simply using the shell to run your alert after the command finishes is a better option.

                                  1. 2

                                    Good point! I forgot about shell aliases. I opened an issue to track adding support for that:

                                    https://github.com/frewsxcv/alert-after/issues/8

                                    1. 1

                                      One option would be to just always run the command through the user’s shell. Yours isn’t the only otherwise-cool utility that doesn’t work on aliases. I recently found https://github.com/chneukirchen/nq and was super stoked until I realized it barfed on aliases. I may submit a PR to support that if I find time.

                                      How do you like Rust? I haven’t found enough time or motivation to wrap my tiny brain around it yet :-(

                                  2. 3

                                    I don’t think alert-after actually does this yet, but one advantage of using a wrapper is that it can check the exit status and automatically give you a success/failure notification. You could do that in shell too, but it’d be much more tedious to write out by hand every time.

                                    1. 5
                                      some --command && osascript -e 'display notification "Success!!"' || osascript -e 'display notification "Failure!!"'
                                      

                                      Not awful.

                                      1. 1

                                        If you simply want to notify with the exit code you can use $? which is bound the exit code of the previous process, e.g.

                                        bash -c "exit 0";  echo Status: $?
                                        
                                        1. 0

                                          A 101-character suffix on a command, versus the OP’s 2-character prefix on a command? Yes, I’d call that “much more tedious”.

                                          (it would be pretty easy to turn your command into a shell-script wrapper with a two-character name, but that’s just an argument about implementation, not about whether a wrapper is a good design)

                                        2. 4

                                          sure, but it could be a 5 line shell script

                                          1. 1

                                            shell has functions and aliases that you can add to your profile.

                                          2. 1

                                            I use zenity on Linux for this exact purpose

                                          1. 2

                                            The tone’s markedly different on this one, given the results (defaults broken by design, only maximalist safety configuration gives you linearizability). Huh.

                                            1. 11

                                              I don’t think that consistency modes other than linearizable consistency are “broken by design,” they just make a different tradeoff. Imagine that you’re lobsters, and decide to build it on top of rethinkdb. Someone writes a post, and publishes it. You check new posts and don’t see your post immediately because you end up talking to a primary that was partitioned away.

                                              This is the absolute worst case scenario that can happen under the default (majority write, single read), and it only happens when a primary is partitioned away and doesn’t realize it yet.

                                              So this is still a pretty strong consistency guarantee. And as soon as the primary realizes it’s not the primary any more, it’ll get the new information.

                                              With that said, I don’t think the takeaway from Aphyr’s blog should be, “Never use anything that doesn’t have strong consistency”. I think it should probably be, “make sure you understand your consistency guarantees, because sometimes it matters–eg folks will end up unhappy if you give two people the same handle”. There are significant latency and throughput disadvantages to requiring linearizable consistency for every single request, so make sure you understand your business requirements and engineer to what you need.

                                              For what it’s worth, I don’t usually look at a persistence problem and think, “Oh yeah, I really need this to be linearizable.” In fact, there are probably a lot of use cases of rethinkdb where I would rather use single write and single read.

                                              1. 1

                                                Sorry, it was a snarky reference to https://aphyr.com/posts/322-jepsen-mongodb-stale-reads. I understand consistency pretty well, was just having a bad day and decided to be an ass.

                                              2. 8

                                                In addition to what moses said, also note that RethinkDB is functioning exactly as documented. They don’t make claims they can’t back up, unlike some previously analyzed systems.

                                                Choosing your guarantee on a per-request basis is fairly common as it puts more power in the user’s hands. For example, DynamoDB’s reads are eventually consistent. You must explicitly ask for a strongly consistent read in your request if that’s what you want.

                                                1. 2

                                                  I always felt the tone differences between the mongodb and cassandra reviews were odd, given that the results seemed very similar.

                                                  1. 2

                                                    He recently announced that he would be writing these articles in exchange for payment. I believe they are his customers.

                                                  1. 7

                                                    Functional programming.. I’d lean towards Maybe on this one, although this is arguably a No. Functional languages are still quite niche, but functional programming ideas are now mainstream, at least for the HN/reddit/twitter crowd.

                                                    Also Java, so I’d call it a yes.

                                                    Model checking is omnipresent in chip design. Microsoft’s driver verification tool has probably had more impact than all chip design tools combined

                                                    I don’t know where the author is coming from here. It’s hard to imagine we would achieve the amazing hardware we have today without tools to harness complexity. What does he mean?

                                                    1. 1

                                                      Sure, tools in general, but probably not for formal methods, which is what’s being discussed in that section. Sorry if that was unclear :).

                                                    1. 4

                                                      There have been a lot of posts questioning GraphQL. Assuming good faith and ability on Facebook’s part (& they have a history of it), all that’s happening is Facebook is having a hard time articulating why they created GraphQL. I think what they’re not communicating is scale.

                                                      I used to work at Amazon. Our team owned an internal service with 50+ business-logic service dependencies (more dependencies for ops tools) and 100+ clients. We didn’t invent GraphQL but we did have our own tools. New teams needed to quickly integrate into existing calculation pipeline and expose new data. Clients needed to consume this data quickly and they don’t really care where it comes from (!!). Interfaces should be uniform and unsurprising. From my perspective, GraphQL is about enabling change as quickly as possible in an environment like this. Without the scale and unique pressures of a big business with many teams both independent and tangled, GraphQL may indeed not be the best tool for the job.

                                                      Facebook doesn’t talk about scale in their docs because it’s not relatable. If I’m right-ish, this is unfortunate because it’s precisely the understanding of scale that makes GraphQL relatable.

                                                      1. 13

                                                        A new and exciting way for devs to donate more free labor to businesses.

                                                        1. 11

                                                          … instead of just contributing to the existing documentation for the projects…

                                                          1. 3

                                                            Yeah - I have a hard time imagining the documentation staying up to date for the projects that actually need it. Popular projects already have documentation. Projects with few users won’t have any incentive to keep the SO docs up to date.

                                                            Examples and walkthroughs are a good middle ground between asking questions on Stackoverflow and the API documentation given as an example in the original post (other posters talk about examples as a possibility).

                                                            Providing a curated, relevant set of examples for a project might be achievable and is actually in SO’s wheelhouse - they already do this, more or less.

                                                            The contribution process and tools can be inhibitive so having a place to contribute outside the project is useful.

                                                            1. 1

                                                              It could work for smaller projects though, eg. if one of my projects ever became popular I could move all the documentation from the source code folder or a website into Stack Overflow and either delete the original documentation or make it a mirror of the Stack Overflow content. If I could get help writing documentation for my projects I would gladly accept it. If I putting on Stack Overflow means more/anyone contributes anything at all then is an improvement on what I have currently :)

                                                            2. 5

                                                              The labor doesn’t just help Stack Overflow. All user-submitted Stack Overflow content is Creative Commons licensed, so anyone can read it, share it, or even create a commercial competitor with the data (as long as attribution is given).

                                                              1. 2

                                                                The attribution required is quite strange, it require a link to Stack Overflow even for a single content from a specific user.

                                                                1. 1

                                                                  I think the primary reason for this is to discourage people taking the Q&A data and creating spammy search hits with it.

                                                                  1. 1

                                                                    I think the primary reason for this is to add incoming link to this for profit website.

                                                                2. 1

                                                                  And I didn’t claim it did.

                                                                3. 1

                                                                  Give it some time to find its place. I don’t think they should try to compete with the likes of readme.io. I think open source solutions like Jekyll (-as a wiki), Sphinx and GitBook are making more important headway in that regard.

                                                                  But the “community powered examples” sounds very appealing. If they build this out in a way that it can neatly accommodate existing documentation as opposed to compete with it, this could work.

                                                                1. 3

                                                                  Facebook OS, coming coon.

                                                                  Seriously, I would welcome some competition. Things are stale.

                                                                  1. 4

                                                                    Indeed. And new blood. I loathe that all the competitors in the software space are mostly the same companies, again and again, just shuffling their order of participation when new fads arrive that needs disruption.

                                                                    EDIT: spelling

                                                                    1. 2

                                                                      Not that I’ve ever used it, but I was hoping ChromeOS would take off and inspire some inovation/fixing/cleaning up in Windows, Mac OS and Linux.

                                                                      1. 2

                                                                        Well, Microsoft indeed got inspired by making Windows 10 phone home.

                                                                    1. 3

                                                                      There is a lot of doc, but is there some textual representation of an eve program ?

                                                                      1. 10

                                                                        There is a version in the repo where we had a textual syntax, though the syntax and semantics at that point weren’t the greatest. It’s an open question to us how we want to expose that in the future, but the current version 0 is visual only. That being said, we’ve actually found it to be more pleasant than writing the equivalent text anyways. Checkout my note on visual programming for more rationale there.

                                                                        1. 4

                                                                          What I love in text it’s there a lot of tools to manipulate it such as (but not only) text editors

                                                                          1. 2

                                                                            It should be fun to write some refactoring tools (I hesitate to say metaprogramming..) for Eve programs in Eve!

                                                                        1. 13

                                                                          Still working on Haskell Programming with my coauthor Julie. Recently finished an initial scaffold of the functor/applicative/monad material, moving on to foldable and traversable now. We’re releasing algebraic datatypes through testing (right before monoids) this 15th. Next month on September 15th the monoid/functor/applicative/monad sequence will be released.

                                                                          Kicking around ideas for a final project, pretty hard to find something that fits all of our specifications. Not easy to find something that’s:

                                                                          1. Tractable for a beginner without much exposure to Haskell libraries. We’re not assuming they know databases and the like, for example. The book is written with the limitations of inexperienced programmers in mind.

                                                                          2. Sufficiently interesting to someone that hasn’t been neck deep in code or distributed systems for awhile. I’d love nothing more than to have them make a Kafka or SaltStack clone in Haskell but it’s going to bore them to tears.

                                                                          Trying to avoid heavy duty web apps that would require a lot of frontend work or learning a whole framework as well. If anyone has any suggestions, please reply here or please tweet or email them to me.

                                                                          We’re also looking for reviewers (of any experience level) so if you have the time and it interests you, please reach out!

                                                                          1. 6

                                                                            For a final project, perhaps a (text based) command-driven discussion / social network? Maybe start out with an in-memory implementation then swap it out for a file-based implementation (reinforcing the abstraction tools you’ve taught)? It could be a lead-in to databases: “manipulating all that text data was kind of a pain and won’t be very fast with hundreds of users. go check out databases!”. You could also generate/serve some simple HTML and say “that’s the basic idea behind webapps”

                                                                            1. 5

                                                                              I really like this idea! I’d have to think about how to avoid the problems with NAT and networking for home-users, but I’m going to kick it around with Julie and see if there’s something workable here.

                                                                              Thank you :)

                                                                              1. 3

                                                                                Maybe could be a LAN-only thing for e.g. conferences or something along the lines of that.

                                                                                1. 3

                                                                                  Pop-up social network?

                                                                                  1. 3

                                                                                    That’d be a good descriptor: you could include your <social-network-du-jour> handle in your profile for longer-term connections, maybe. For a talk, maybe a way to submit questions during the talk and have them queued up at the end.

                                                                                2. 2

                                                                                  Sure thing!

                                                                                  Maybe https://ngrok.com/ will help? (also has a handy request inspector!). I’m not sure if it will be appropriate in complexity/difficulty for your audience, though.

                                                                              2. 2

                                                                                I’d like to review. What do you need?

                                                                                1. 1

                                                                                  Is the email address in your lobsters profile a good way to reach you?

                                                                                  1. 1

                                                                                    Yeah, sure, contact me at jordigh@octave.org

                                                                                2. 2

                                                                                  For review, do you need anything more formal than what I’ve been sending you and Julie on Twitter?

                                                                                  1. 1

                                                                                    It’s more work and structure than that, but what you’ve been doing isn’t wildly different.

                                                                                    1. 2

                                                                                      I wouldn’t mind helping out, since I want good learning materials out there.

                                                                                      Use the email address I used when I mailed you last week if you want to send me more info.

                                                                                  2. 2

                                                                                    Cool, i’m curious what you think of the maybe haskell book that thoughtworks put out recently? I rather liked its approach of introducing functor/applicative/monad as concepts. I wish it had been out a year ago when I was starting to relearn haskell in earnest.

                                                                                    I’ll have a look at the new updates after you update the epub, been following along with interest on this book.

                                                                                    And for a final project, can always punt and do a todo application. >.<

                                                                                    1. 2

                                                                                      It’s hard for me to think about a 94 page book when we’re working on something much longer with very different objectives. You could probably stack it up against how I review books with more similar objectives in this post and see whether it hits the high notes I care about.

                                                                                      It’s very hard to think about a book with wildly different scope like that. We release >100 pages every month and we’re trying to make a book that gets people from zero to, “I can begin to solve my problems with Haskell”.

                                                                                      More fundamentally, I’m skeptical people can just be taken on an isolated tour of functor/applicative/monad, there are foundations that have to be in place for it to be anything but cargo culting.

                                                                                      1. 2

                                                                                        Fair enough, just thought i’d ask is all. Looking forward to the updates regardless! I’ll dig into the link.

                                                                                        1. 2

                                                                                          More specifically about Maybe Haskell: I think it’s worth giving people a teaser of what’s possible. I do this sort of thing too, but usually for in-person demos/tutorials. However, I don’t regard them as being a component of any kind of pedagogical scheme.

                                                                                          1. 2

                                                                                            For sure, i’ll admit maybe haskell is at best a great way to whet someones appetite for haskell. So in that regard I’d place it alongside LYAH. Although even less comprehensive in that it doesn’t cover a whole lot of haskell at all. Then again it doesn’t really bill itself as such either.

                                                                                            I just really liked the approach to the functor/applicative/monad explanation used is all. It helped convince a friend to learn haskell. But they’re hitting the same wall everyone seems to with haskell learning materials. I’m helping but i’m not the best teacher so I’m not sure if I’m hindering more than helping. Haskell isn’t hard either its just difficult to elaborate why doing things a different way is beneficial. In hindsight its 20/20 but from the other direction it just looks like a mirror.

                                                                                            Either way keep it up the lambda calculus links on the first chapter were fun to review and read. I was pleasantly amused that you started out with that.

                                                                                    2. 2

                                                                                      I grabbed a copy of the book last week, so far so good.

                                                                                      1. 2

                                                                                        sure, i’d be glad to help review. email address in profile is valid.

                                                                                        1. 1
                                                                                          1. 2

                                                                                            oops, thought i had :) fixed now

                                                                                        2. 2

                                                                                          Looking over the ToC, I’d noticed that the four final chapters are TBA. I’d love to see at least one on something along the lines of “using Haskell in anger”: some tips for real-world Haskell use. Things like common packages to be aware of, debugging, problem solving with Haskell, and deploying my programs. Are there plans to include something like that?

                                                                                          1. 2

                                                                                            We’re always open to ideas/suggestions, but those chapters are literally TBA. We have topics planned for them.

                                                                                            The “almost guaranteed to happen” chapters are IO, “when things go wrong”, and the final project. The more open slot is DSLs & APIs. Data structures covers a lot of the common packages to be aware of, monad transformers covers some of those as well. Debugging is sort-of part of “when things go wrong” but it’s probably not quite what you’d think.

                                                                                            The way we name our chapters hides practical examples. The upcoming release (15th) has more practical projects and examples than have been seen so far.

                                                                                            1. 2

                                                                                              Fair enough.

                                                                                              1. 2

                                                                                                Your suggestions are very much appreciated as I wasn’t happy with the “DSLs & APIs” chapter and I’m seeing a common theme (which you’ve improved the confidence in) in what practical bits people want.

                                                                                          2. 2

                                                                                            I’d be happy to review; I’m going to university in a couple of months and will be doing a very theoretical CS course, which begins with haskell - I’ve been told to buy the Bird book on Haskell, but a lot of people have told me it’s terrible. I already know the basics of haskell though as I’ve used it for a couple of years.

                                                                                            1. 1

                                                                                              What email should I contact you at?

                                                                                              1. 1

                                                                                                Ah, I sent you a pm, not entirely sure how the privacy settings work on this website but I was under the impression my email was viewable in my profile.

                                                                                                1. 1

                                                                                                  Only what you explicitly put in the “About” box is visible (plus your Gravatar). You can see here what’s visible: https://lobste.rs/u/NickHu

                                                                                                  1. 1

                                                                                                    I just thought there ought to be a “make my email public” checkbox or something like that, and reading https://lobste.rs/privacy implied that that might already be the case, duly noted though.

                                                                                            2. 2

                                                                                              I’d love to help review! I have experience in other languages, and have made a few false starts with Haskell (through LYAH and the cis194 class).

                                                                                              1. 1

                                                                                                A cis194 dropout is a perfect candidate for us! What email should we contact you at?

                                                                                                1. 1

                                                                                                  There’s a link in my profile now. Thanks!

                                                                                              1. 1

                                                                                                There are some points where I just don’t understand you (GC are not partitions in the CAP proof, and it’s not new: see cap faq point 16 http://henryr.github.io/cap-faq/). You can push it into it (for example by putting some deadline constraints in the definition of availability), but it’s not really CAP anymore.

                                                                                                It’s easier to choose an algorithm which is safe in the general case of asynchronous networks,

                                                                                                Yeah this one is interesting. I agree on the algo choice (there is no other choice anyway), but many errors (typically not flushing the writes to the disk) are visible only with kill9 or node failures. You have to test independently. Partition tolerance does not mean fault tolerance.

                                                                                                1. 4

                                                                                                  Partitions in the G&L proof are any pattern of message loss. Any garbage collection period which exceeds the duration an application will wait for a message before considering it lost (e.g. tcp socket timeouts, application-level timeouts) will get you the same behavior.

                                                                                                  1. 1

                                                                                                    Yep, that’s what I call pushing it into it (application cannot wait forever => there are deadlines constraints). CAP applies in this case (i.e. you really have to choose between consistency & availability).

                                                                                                    GC are still a little bit simpler than a true network partition, because the process stops working for everybody. Agreed, there will be some nasty race conditions at the end. But you don’t loose a full rack when there is a GC. It’s a much nicer kind of fault, one node at a time. In a big data system, if you lose a rack you have to replicate the data again for safety. With a GC you do not need that: the node will come back to life before you start to replicate the 2Tb of data it was storing (not to mention the case w/ a rack!).

                                                                                                    I do agree with you on the asynchronous part: the algorithm you need to choose when the network is asynchronous will help a lot with partitions and with GC. But you need to test both.

                                                                                                    1. 4

                                                                                                      It’s a much nicer kind of fault, one node at a time

                                                                                                      GC is a notorious cause of distributed systems data-loss, typically where it allows two nodes to believe they’re the primary at the same time. Take a look at the Elasticsearch mailing lists sometime for all kinds of horror stories around high load, memory pressure, or GC causing inconsistency.

                                                                                                      1. 1

                                                                                                        I’m not sure if the size of the fault is necessarily relevant for this discussion, either.

                                                                                                        1. 1

                                                                                                          Agreed again, but node failures and network partitions will add a few other horror stories.

                                                                                                          I mean, I would expect a software vendor to say

                                                                                                          • We have tested dirty node crashes, no data loss

                                                                                                          • We have tested GC. No dataloss, no performance issue if the GC is contained within 10s.

                                                                                                          • We have not tested network partitions. Per our design it should be fine (we’re aiming at AP: availability during partition), but it’s still an edge case.

                                                                                                          Rather than: “we’re partition tolerant of course.”

                                                                                                          And for a system like ES (for example), the design for availability under network partition could be something with partial results and so on (harvest & yield). Not that easy to do (I don’t know ES).

                                                                                                          1. 4

                                                                                                            Agreed again, but node failures and network partitions will add a few other horror stories.

                                                                                                            Absolutely agreed. The reason I mention GC in this response is because you’ve argued that LANs won’t partition. Even if LAN fabric were totally reliable, I’m trying to remind people that partition tolerance is about message delivery, not just what we traditionally consider “the network”.

                                                                                                            And for a system like ES (for example), the design for availability under network partition could be something with partial results and so on (harvest & yield).

                                                                                                            Gilbert & Lynch, footnote 4: “Brewer originally only required almost all requests to receive a response. As allowing probabilistic availability does not change the result when arbitrary failures occur, for simplicity we are requiring 100% availability.”

                                                                                                            1. 1

                                                                                                              Absolutely agreed. The reason I mention GC in this response is because you’ve argued that LANs won’t partition.

                                                                                                              I doubt I said something like this :-) But yeah, for sure the whole post is only about network partitions. I will update the post to make this clear.

                                                                                                              1. 1

                                                                                                                “CA exists, and is described as acceptable for systems running on LAN” “Stonebraker was considering small systems of high range servers on a LAN” “it is also fine to assume CA on a LAN”

                                                                                                                1. 1

                                                                                                                  None of those are mine (lynch/stonebraker/brewer)

                                                                                                                  Both Stonebraker and Brewer consider (quoting Brewer but Stonebraker said exactly the same thing) “CA should mean that the probability of a partition is far less than that of other systemic failures”, so even if they think that CA is acceptable in some specific cases on a LAN that does not mean they think that LANs won’t partition.

                                                                                                        2. 1

                                                                                                          GC are still a little bit simpler than a true network partition… It’s a much nicer kind of fault, one node at a time

                                                                                                          This is usually the case. However, I’ve also seen the back pressure resulting from a GC cause other nodes to become loaded. The other nodes then started a GC. Now there was a feedback loop and the entire system ended up falling over.

                                                                                                          The system could have been configured better… but that’s kind of the same point about experiencing partitions on a LAN. It’s not cost-effective and you’re still going to miss something.

                                                                                                  1. 1

                                                                                                    Awesome! This is the most interesting thing I’ve seen in a while - I’m also interested in visualizing programs and learning from models from other domains. Current software / programming language models don’t really seem to capture the right problems.

                                                                                                    1. 1

                                                                                                      Thanks :) The best part of the internet is getting to share interesting ideas with other people.

                                                                                                    1. 1

                                                                                                      Looks great! I’ve been searching for my next laptop. Only problem wit this is you can only get 8GB of RAM and it’s soldered to the motherboard..

                                                                                                      1. 3

                                                                                                        Same here, I really need 16GB to support various VMs and such.

                                                                                                        1. 2

                                                                                                          Seems to be fairly uncommon for ultrabooks to support 16gb, though it would be nice: this XPS 13, the Macbook Air, and the Thinkpad X1 Carbon all top out at 8gb. The only good option I know of is the Macbook Pro 13", which you can upgrade to 16gb (comes out to $1500).

                                                                                                        1. 3

                                                                                                          Seems like the idea behind algebraic effects. Glancing at “Programming and Reasoning with Algebraic Effects and Dependent Types” I see the same type in the implementation. Is there any practical difference?

                                                                                                          1. 2

                                                                                                            This is the most interesting thing I’ve seen in a while. I wonder if my time is better invested in learning Coq than Haskell..

                                                                                                            1. 7

                                                                                                              Well, I found learning coq a really big investment (time and mental-wise)… I tried twice and left a bit frustrated, the simpler proofs are really simple, the harder ones are really hard. I wouldn’t dismiss the fact that it may be just too hard for me to grasp though.

                                                                                                              If you want to learn programming-language-theory oriented coq there’s a de facto starting point: http://www.cis.upenn.edu/~bcpierce/sf/current/index.html and you may continue with http://adam.chlipala.net/cpdt/

                                                                                                              However, if you like software verification, but find the proving process boring, there’s always the subject of SMTs (Z3, CVC4), automated theorem provers (ACL2) and such (coq is rather a proof assistant, you need to do the proof manually). You don’t need to learn coq to have fun with software verification!

                                                                                                              [EDIT]

                                                                                                              I forgot to mention Idris, which aims to be a sort of “usable coq”.

                                                                                                              1. 5

                                                                                                                In my limited use of it (mostly limited to a grad course taken some years ago), I found ACL2 more towards the proof-assistant side of things also. It does have some automated theorem proving, but it only succeeds fully automatically for very simple things. For anything non-trivial (not even meaning big Real Software, even simple algorithms-textbook algorithms) you have to hand-hold the prover quite a bit, which requires digging into the details of the proving process. A lot of getting a proof to “go through” consists of strategically giving it rewrite rules, induction schemes, etc. The people who are really good with ACL2 seem to have a lot of black-art type knowledge of it.

                                                                                                                1. 2

                                                                                                                  Fabrice, thanks for the reply - this is the sort of overview I was looking for.

                                                                                                                  I have some experience with Haskell - read a lot of papers & code but have only written toys. I’ve seen Idris around and algebraic effects are definitely intriguing.

                                                                                                                  From the sounds of it, Coq isn’t quite what I’m really looking for. I might try out some of those really simple proofs you’re talking about to get a feel for it and then move onto learning more about SMT and Idris.

                                                                                                                  Software verification is definitely the goal, for me :)

                                                                                                                  1. 4

                                                                                                                    Depending on what you mean by “software verification”, you should also look at TLA+ and Promela/Spin. They aim at a different space from Coq, but in my experience tend to be better at the set of things that many working coders find useful.

                                                                                                                    1. 1

                                                                                                                      Thanks, I’ve toyed around with TLA+ and have started digging into the book. Haven’t heard of Promela/Spin - will take a look.