1. 99
  1. 9

    Might be a good use of the show tag, since this is a lobster’s content–not just product spam.

    1. 25

      I misread this the first time as “lobsters’ content” and now I’m feeling all sappy because lobsters was the first place that really enjoyed all my technical writing, which encouraged me to keep pushing forward with it. Y’all are the best <3

      1. 7

        V.v.V

        1. 1

          Awesome! Looking forward to getting to read this.

      2. 5

        Awesome! I bought the ebook right away.

        1. 2

          Same here.

        2. 5

          Great job! This is only the beginning for you, buddy!

          Just bought it to send some royalties your way. :)

          1. 5

            Congrats on finishing the book!

            Has anyone tried to model anything involving Unix signals with TLA+? Does it make sense for those types of problems?

            There are several edge cases with Unix signals that applications should handle according to POSIX, but that they often don’t handle in practice. Most programs that deal with signals are littered with special cases that accumulate over time.

            One issue is coalescing of signals, and another is EINTR, although I’m not sure that is the kind of problem that can be modelled (maybe it’s more of a linter problem).

            Right now the signal handling of Oil is somewhat naive, and when I look at real shells, I don’t see anything other than a mess of special cases. I would like to do something more principled.

            At the very least there are these two cases:

            • you receive a signal and you’re in the shell interpreter itself, and
            • you receive a signal and you’re waiting on a child process.

            Also handling exits with SIGCHLD vs. wait() is an interesting problem.

            There’s more to it than that (i.e. including the kernel state of the process and subprocesses), and I wonder if TLA+ can help express those kinds of things.


            Thinking about this a bit more, is it possible to have a TLA+ “library” desecribing POSIX kernel behaves with respect to signals? And then you could somehow describe different applications on top, and the invariants you want – e.g. Ctrl-C doesn’t cause memory to become corrupt.

            And it could tell you some sequence of signals that would break those invariants? Not sure if that makes sense.

            1. 3

              I don’t know of any models of Unix signals; the closest thing I’m aware of is OpenComRTOS, an OS that was fully specified in TLA+. That implies it’s doable but doesn’t necessarily mean it’s the right tool for the job. Unfortunately I don’t know enough about operating systems or POSIX to be able to give you a better answer than that.

            2. 3

              Kick ass @hwayne

              1. 3

                @hwayne is there a simple way to get the physical book with the ebook besides purchasing both separately, maybe I missed it?

                And which method of purchasing Amazon/Apress/something else, gives you the biggest kickback?

                1. 4

                  Currently talking with the publisher about a package deal; seems unlikely but I’ll keep pushing.

                  Re kickbacks: they’re all about the same so I wouldn’t worry to much about it. All that matters to me is that people enjoy reading it :)

                  1. 1

                    The publisher has a way to make books eligible for Amazon Kindle MatchBook, so you can get a Kindle ebook for cheap or free after buying the print book. Most publishers don’t opt for this :(

                  2. 3

                    Congratulations!

                    1. 3

                      Congrats @hwayne!

                      1. 2

                        Congrats on the release. Looking forward to reading!

                        1. 2

                          Great work mate! It’s been fun reading along the past few months (?) on your blog.

                          1. 2

                            Super excited. All of my free cycles these days have been going to formal methods - reading the Way of Z, working on my own ‘formal methods lite’ system. TLA+ has been on my list for a long time and I ran through the first chapters of Lamport’s tutorial but it never stuck. Pumped to pick up a resource that first and foremost tries to make things practical and adoptable.

                            1. 2

                              Oh yeah, that reminds me: would it be alright if I messaged you some questions about Pantagruel? Thanks!

                              1. 2

                                Dude, it would be fucking awesome.

                            2. 2

                              Congratulations! Writing a book is a ton of work.

                              1. 1

                                Would the book read well on a Kindle? I don’t want to buy an ebook only to find I can’t really see the charts or graph or pics or whatever that would require lots of awkward zooming on eink.

                                1. 1

                                  Placed an order.

                                  Question: does it have pictures of you with silly hats for every subsection like in the TLA+ video course? If not, why?

                                  1. 1

                                    SOLD! Can’t wait to get my copy!

                                    1. 1

                                      Congratulations, looking forward to reading it, and always glad at more texts on formal methods coming out

                                      1. 1

                                        Excellent - copy bought.

                                        1. 1

                                          Excellent! Congratulations, @hwayne!

                                          I too have the same question that @msingle asked.

                                          1. 1

                                            Congrats @hwayne!!! Just ordered a copy :)

                                            1. 1

                                              @hwayne I just discovered your 2017 talk at StrangeLoop about TLA+ and really enjoyed it! The talk sparked my interest so much that I decided to buy your book Practical TLA+ right away.

                                              The examples you presented in the talk were mostly about the verification of models before their implementation, which is without a question a proper use case, but would it be practical to specify e.g. methods in legacy software which don’t have tests in order to refactor them safely?

                                              Update: added a question

                                              1. 2

                                                Glad you enjoyed! I know a lot of people have successfully used it for refactoring legacy systems; I don’t know if anyone who’s used it at the method level, which might be a little bit too low, but it’s worth a shot IMO.

                                              2. 1

                                                Congrats! Writing a technical book is a raftload of work and takes a lot of persistence to get to the end.