1. 3

    I’m making the static analyzer Stan get applied automatically to every pull request that hits my github repositories. Should be fun.

    1. 1

      Prepping for a launch so….

      • Roll out new production
      • Migrate a database
      • Increase the ceiling to our cloud capacity

      I’m sure there’s twelve things on the list and another 12 I should know about but haven’t considered.

      1. 7

        Kathleen Fisher is sharp as a whip. As expected, this talk is well structured. All in all the talk is heavy on the “what projects have been done using formal methods” and light on the “what formal methods tools and characteristics are out there”.

        She asserts that formal methods can eliminate many exploitable vulnerabilities. First there is an acknowledgement that people are jaded about formal methods promising this and more (really, much more) for 50 years without delivering, but now we have faster CPUs, better SAT/SMT solvers, and more infrastructure (allowing people to focus and specialize on building better solvers).

        As empirical evidence she presents DARPA HACMS project, which was about secure autonomous vehicles. The UAV software at the time was extremely vulnerable and this project rearchitected and replaced most of the stack ending up with FreeRTOS, custom control software writing in Ivory (a Haskell EDSL), Tower EDSL to coordinate concurrent tasks, and a formal method tool to reason about the component interactions. This and similar efforts with the LittleBird and SEL4 resulted in additional funding via the John McCain Defense Authorization Act (some personal pride in achievement is showing here).

        From here we finally get to discussing formal methods which she defines as “application of a broad variety of theoretical computer science fundamentals to problems in software and hardware specification and verification.” Or more specifically 1. Based on math 2. Machine checkable 3. Capable of proving properties in code and models. Examples of formally methods in practice including SEL4 (a kernel with correct accesses controls, compilation, separation), compcert (a C compiler that preserves semantics from C down to assembly), AWS’s TLS efforts.

        Closing lessons:

        • Don’t verify existing code - think more correct by construction.
        • Use SMT if possible to automate the verification.
        • Use code+proof generation

        Disclosure: I’m a Galois employee and worked on HACMS - Galois was mentioned a couple times in this presentation.

        1. 5

          Thanks for your work on applied, formal methods. Far as what theyve done vs how, we actually have a lot more of the latter than the former published. We need as many presentations on practical use as we can get to increase uptake.

          Far as the how and details, you can click on the formalmethods tag to find stuff going back years. It’s mostly PDF’s on specific techniques or problems solved with a mix of common, esoteric, and historical.

        1. 4
          1. Taxes
          2. Install a new washing machine
          3. Deal with changes to the compilation database format where cmake seems to be outputing the command + arguments in a single “command” string where it has previously always included an arguments field with an array of strings.

          Seriously, can we all agree on a canonical compilation database format? I see no command with the command as the first “argument”, I see no arguments with the command line in shell-sytle, I see a command and a list of arguments… this is not a standard but a family of related dialects.

          1. 8

            It’s good to know that 22 years later the libraries/training/popularity (aka - popularity) is still the impediment to… popularity. I’m seriously tempted to summarize a publication to a tautology, but yes the implication goes the other way - a lack of popularity is in part due to libraries and training (and existing, self-propagating, popularity).

            Both F# and Scala try to evade the library issue by borrowing all the work from their respective platforms. Haskell, SML, and OCaml have taken the harder path of building their own community and growing their own libraries. I used to think this was why they failed to achieve as significant a user base but since then GoLang, Rust, and Dart^H^H^H have all gained popularity without borrowing from another community’s success. Both those received major corporate backing (more than F# even, I believe). Is there an example of a language succeeding in the modern age that did not receive such support or build on an existing community like JVM or .Net?

            1. 4

              Maybe Lua? I’m not a fan, but it seems to be popular. I think it fits into the “build on an existing community” niche. It’s used to customize Awesome WM, Wireshark, Nmap, Neovim, games, an internal thing at the company I’m working for… It’s everywhere.

              1. 2

                How “functional” is Lua on a scale from Haskell to JavaScript?

                1. 5

                  Very much on the JavaScript end; Lua and JavaScript are almost like dialects of the same language in some ways.

                  1. 1

                    Lua is a bit different in that its equality semantics are almost exactly egal from Henry Baker’s paper, and it’s use of coroutines can encourage a more lexical approach.

                    Not sure it counts as “modern age” as it predates Ruby and Python.

              2. 3

                I used to think this was why they failed to achieve as significant a user base but since then GoLang, Rust, and Dart^H^H^H have all gained popularity without borrowing from another community’s success.

                Who were all originally backed by entities with the means to prop things up with money and/or people. That I know of, none of those began outside of Google or Mozilla. They are the products of these entities wanting to solve problems that they think they have. As far as adoption, “Nobody Gets Fired For Buying Google” might as well be the new “Nobody Gets Fired For Buying IBM.”

                1. 1

                  Younger me found this “popularity begets popularity” tendency to inspire cynicism. These days I’m a bit more at peace about it.

                  Part of that is Rust, part of that is seeing that there are some impediments to FP languages, part of that is accepting that first impressions color a ton, and people fought tooth and nail against OOP for years, citing its difficulty. It took many years of just being around for people to think it was normal. Change is hard, but I’ve benefited enormously from keeping an open mind and looking for that challenge.

                  1. 1

                    I still find it mind boggling how much money Sun spent marketing Java:

                    https://www.theregister.co.uk/2003/06/09/sun_preps_500m_java_brand/

                  1. 8

                    As someone making a product with a Haskell backend I have a lot of opinions here. There is a tremendous amount of power and safety in a strong, descriptive, type system and modern code generation techniques. I’m deep in the Haskell community and quite happy with Haskell. At the same time users pay for these benefits every step of the way - it’s trailblazing (or more negatively phrased, bushwhacking) with each step and that does hurt.

                    Some examples of bushwhacking: Working with a database other than the top three SQLs will very likely require you to write your own bindings. Same with interacting with other SaaS services like New Relic. Use of a large swath of existing libraries likely means you’ll be the only production user of some of them. Cached build require you to invest in a Shake cloud or Nix build system because neither stack nor cabal do cached builds right (yet).

                    More on the topic - this very old post has it right that getting to a functioning point takes too much effort. Things can and should be easy. Python libraries are made so users can get a complex task done with ease while Haskell libraries are made to be fully generic and keep the most options open to users. This isn’t a language issue but a culture issue and we must learn to change.

                    1. 2

                      Play with kids.

                      Have S’mores at the fire pit.

                      Learn more nix.