1. 1

    Tangential question, but do you think that formal methods will get more traction in the 2020s? Aside from building more robust software, I think semantics can help AI approaches such as program synthesis.

    I did a whole MSc on the topic back a decade ago, and we were using a mix of old references like the one posted and new more polished material. I remember quite fondly using these books, on a language inspired by Z: http://www.imm.dtu.dk/~aeha/RAISEbooks.html

    The literature is much better now. In particular there is some great broad introductory material:

    Plus some classics, most available long ago already:

    And some constructive foundations:

    1. 3

      I have been summoned

      Almost exactly a year ago I wrote a piece called Why Don’t People Use Formal Methods which aimed to cover a lot of the specific difficulties in the space. To summarize:

      1. Proving code is correct is pull-your-hair-out hard
      2. Proving designs correct is easier, but has social barriers.

      Now (1) is getting easier, as the SMT revolution comes into full force, but it’s probably going to be a specialist domain for the near future. I’ve talked with people who do it professionally, and the challenges there are all essential. Proving code correct is just a fundamentally difficult problem. We’re likely to see more advances in partial verification, though, with things like Rust showcasing what we can push into the language.

      Re (2), the biggest challenges there are accidental: formal specification has bad UX and bad PR. I’ve been working really hard on the second one, making things like TLA+ and Alloy easier to learn by providing better education materials and more interesting to learn by providing lots of good examples. But the UX problem is still a pretty big barrier. Fortunately, it’s something that can change, and probably will as more and more people start to learn these things.

      1. 1

        I totally agree SMT solvers, when blended into languages, will make things more usable.

        I really liked Spec# as a student a decade ago. I think their approach of applying theorem proving on contracts yields a very natural user interface. I suspect that when applied on a language with very clean semantics, such as any purely functional one, it’d be even better.

        Do you have any other favorite tools aside from TLA+ or Alloy? What is the domain you are mostly working on?

    1. 7

      I think this will be my first year of using exclusively Windows after like 15 years. All started when I got a small Debian netbook from my father. Used Windows pretty much exclusively for gaming after that. Now I run it both on my laptop and on my PC. Well I do all my work through Msys2, I have bash and basic Linux utilities and a package manager which is basically all I ever needed.

      I got burnt out from fixing things. I got burned out from being tempted to break them. Took me a while to realize I actively don’t want to know how to fix anything pacman related, or WM related, or anything like that.

      Linux is a bad fit for me because I’m a perfectionist. Even when I’d fix something I had this unshakeable feeling that I’ve ‘muddied’ my system, that it still might tacitly be in an invalid state. Yet I never put in enough energy to become truly proficient with stuff, only fragments.

      Here’s a snarky twitter thread in this vein: https://twitter.com/garybernhardt/status/1078389370741186560

      1. 7

        Actually I feel the other way round about Linux vs other systems. I can only achieve simple and fully reproducible setups using Linux.

        The key is cherrypicking appropriate hardware and simple standard components. In my case, I find all-Intel machines plus a simple userland (StumpWM, Emacs, Firefox and XTerm) are incredibly nice to use. For this I employ both NixOS and Archlinux.

        1. 7

          Yup. Brains are different. For you, the shortcomings that are unclimbable mountains for some are barely noticeable.

          I do think that with things like WSL and Powershell, Windows is beginning to approach the same level of customizability, but its interfaces for accomplishing what you want are probably not to your liking.

          That’s the whole point, it’s about finding the interface that feels good to you while appreciating that it isn’t the same way for everyone.

          1. 3

            Thanks, I am interested in learning what makes Windows superior to Linux for your usecase aside from hardware compatibility.

            In my case, I love Linux due to minimal distros (few moving parts) and declarative configurations plus rollbacks (Nix and dotfiles).

            1. 2

              I had switched from Linux to macOS in 2007, because it was so much more polished (it still is) and had so much better applications (still does). But NixOS is what brought me back to the Linux on the desktop fold. Being able to define your machines and development environments declaratively is an enormous win. I can check out a project repository on a new machine and I have exactly the same CUDA, PyTorch, etc. versions.

              (Yes I know that Nix works on Darwin and I use it on my MacBook, but NixOS is more encompassing + Linux is better supported by Nix.)

          2. 1

            I hate simplicity and the best way to achieve reproducibility is to not ever have to reproduce anything:)

          3. 5

            Msys2 is a good solution, WSL is excellent in my experience.

            And it’s only getting better, there’s a HUGE amount of effort being invested in making it a first class development environment from Ubuntu and Microsoft. I’m psyched to see what evolves in that space.

            And I totally agree, I have both installed on my laptop and very much enjoy having Linux around to play with the amazing toys the mad scientists come up with and do crazy experiments on, but when I Need to Get Work Done (and this is gonna make the diehard *NIX folks bristle, sorry folks :) I boot into Windows and stop worrying about it.

            1. 1

              WSL1 has extremely poor IO performance, to the point where it is almost unusable in certain situations. I’ve since switched to using an ‘always-on’ Linux VM using hyper-v that I just SSH into. Much better performance and support for all Linux programs that way. I’m looking forward to WSL2 though, which is just actual Linux running in a VM.

              1. 1

                Yes I’m very much looking forward to WSL2 as well. I now wish I’d bought the Pro version so I could run the preview, but unfortunately their marketing doesn’t mention anything about Pro having expanded Hyper-V container hosting capabilities.

            2. 4

              I got burnt out from fixing things. I got burned out from being tempted to break them. Took me a while to realize I actively don’t want to know how to fix anything pacman related, or WM related, or anything like that.

              Don’t break things then? Linux systems don’t randomly break like Windows systems do. They just work, reliably, the same way, until you change them. People that complain about their Linux systems breaking inevitably are doing stuff like installing dozens of AUR packages. Installing loads of crappy third party software is going to have negative effects on any operating system.

              Here’s a snarky twitter thread in this vein: https://twitter.com/garybernhardt/status/1078389370741186560

              This is the problem with Twitter. We don’t see any of the replies to his tweets, we just see him unfairly and inaccurately paraphrasing what people say and arguing against that. And it’s impossible to argue against his claims anyway.

              His original tweet is about the Linux desktop, and as soon as people point out that the Linux experience on desktop is completely fine today, he pivots to talking about laptops, which aren’t desktops. Someone points out that other platforms also don’t work reliably (no shit! none of them work reliably) and says “Buy a new Mac. Open the lid. The trackpad works. The sound works. The WiFi works. Emoji works. 3D acceleration works. Close the lid. It sleeps. Open the lid again. It wakes from sleep.” Like mate, you can get Linux laptops where all those things work too…

              Every time anyone responds to his point, he shifts the goalposts.

              1. 6

                Linux systems don’t randomly break like Windows systems do.

                In my experience this is very incorrect. I’ve been using Windows 10 for the last couple years with no real issues. Prior to that I was using Ubuntu and had random things break almost once a week. You could say it was my fault for using third party package sources to install current versions of software that was unavailable in the official sources despite having been released for six months, but things like that simply don’t happen on Windows in my experience.

                1. 1

                  In my experience Windows 10 breaks constantly in weird ways and Linux is very reliable. And that’s certainly not my fault!

                  Random things literally cannot break ‘once a week’ on Linux unless you’re changing things once a week. You complain about needing to use third party packages then also complain about stability. Like, the whole point of the official repositories not being the most recent version of packages is stability!

                2. 3

                  Like mate, you can get Linux laptops where all those things work too…

                  I think that’s the thing; he’s comparing Apples to oranges^Wrandom hardware and throwing Linux on it. I am constantly disappointed by stuff not working in Debian on some Thinkpads (my current work machine has a weird issue with the display driver on multi monitor and my home laptop’s microphone doesn’t seem to work at all), but then those weren’t actually designed to run Linux. Try running MacOS on a random janky piece of shit PC hardware “designed for Windows” and see how well you fare. Then complain on Twitter and watch the number of people claiming their Hackintosh works just fine, thankyouverymuch.

                  By the way, what “designed for Linux” laptops can you recommend? I’m slowly starting to think about replacing my x230 and I don’t intend on buying another Lenovo. Ever.

                  1. 2

                    Like mate, you can get Linux laptops where all those things work too…

                    I bought a HP laptop this year and stripped off Windows and put on OpenSUSE. It’s a niche distro, and neraly everything just worked (except codecs, but just add Packman). I haven’t had to configure much since set up either. I know people have gotten themselves into trouble with pacman, and I’ve gotten myself in a world of hurt in both apt and yum before, but zypper seems to do the right thing most of the time. I spent many college nights tinkering to get things to work, but things are 1000x better today.

                    1. 2

                      Don’t break things then?

                      They break by themselves. Constantly. Even if accomplishing basic things didn’t require a level of involvement from the user much higher than that in Windows, even Ubuntu tended to break just from basic updating.

                      Linux systems don’t randomly break like Windows systems do.

                      I genuinely can’t recall Windows ever breaking, except once when I had a hardware issue that was causing BSODs.

                      People that complain about their Linux systems breaking inevitably are doing stuff like installing dozens of AUR packages.

                      Oh man you use Arch and actually have no trouble stating that it doesn’t break literally randomly?? This is a meme even in hardcore Linux enthusiast communities because of how often that happens.

                      1. 4

                        They break by themselves. Constantly.

                        They literally do not. This is not up for debate. Software does not spontaneously break. You change things and it breaks. Its developers change things and it breaks. But it does not spontaneously break.

                        Even if accomplishing basic things didn’t require a level of involvement from the user much higher than that in Windows

                        Like what? Beyond installing it in the first place. That computers almost all still come with Windows is a perfect example of the failure of anti-monopoly laws, not a point against Linux.

                        I genuinely can’t recall Windows ever breaking, except once when I had a hardware issue that was causing BSODs.

                        Windows is notoriously unreliable. I can’t understand how someone could even type the words ‘I genuinely can’t recall Windows ever breaking’. It’s an operating system that’s so unreliable that people have to regularly reinstall it to avoid it becoming slowed down by its own decay!

                        Oh man you use Arch and actually have no trouble stating that it doesn’t break literally randomly?? This is a meme even in hardcore Linux enthusiast communities because of how often that happens.

                        It’s a meme specifically because of the ease with which you can install third party packages. If you don’t do that then it doesn’t break basically ever unless you completely ignore the announcements every year or so that you need do so something beyond updating all your packages for some reason.

                        If Arch did break more than other distros then that would just confirm that the issue is the software breaking and not the operating system, because the only difference between Arch and other distros is that it’s rolling release and doesn’t patch its packages.

                        1. 4

                          They literally do not. This is not up for debate. Software does not spontaneously break. You change things and it breaks. Its developers change things and it breaks. But it does not spontaneously break.

                          Yeah, it can, assuming it’s stateful and you actually use it. I’ve had stock installs of Debian run out of disk space because of too many log files.

                    2. 2

                      I’m sometimes tempted to go Windows only but I always have to dual boot to Windows on a number of machines and the consistent micro lags (30 - 150 ms) on brand new top-of-the-line hardware drives me crazy :-/

                    1. 7

                      This was my home office for most of last year.

                      However, I have now decided to return to a life of living out of a suitcase and slowly travelling the world, writing Haskell on a Macintosh Book Air. I’m looking forward to when Fruit Company releases the new machines with the old keyboards, as I spilled a glass of exquisite Georgian red wine in my current machine and typing has become somewhat less ergonomic.

                      1. 1

                        Living the dream. I’d love to hear more about how you do this, since doing the same thing someday is on my bucket list.

                        1. 8

                          I started working remotely six years ago, and was working partly remotely for about 18 months prior. I always knew I wanted to work from home, and initially it was something I requested as part of the salary negotiation process. Us programmers have plenty of leverage in that regard.

                          All through my freelance/consulting years, I had to convince companies to let me work from home, and would pitch it as them getting more documentation — because communication should be mostly asynchronous, in written form — and also buying my services at a lower rate, since I don’t have to pay the extortionate costs of living in, e.g. London. Everyone wins.

                          I could have happily continued living in Poland by the beach, but visa issues with my partner (Russian) meant we would potentially be separated for a couple of months. Rather than endure the bitter Winter by the Baltic Sea alone, in February and March of 2018 we went and lived in Thailand. I then realised there’s no good reason for us to not continue floating around different countries that are more affordable and have a better climate. We went sailing in Greece in May, lived in Belgrade in June, Warsaw in July (not very original I guess; I’m half Polish), Ukraine for three months, and then a combination of London and Russia towards the holiday end of the year. At the end of 2018 I quit working for other people, and I have been focusing on my own projects since.

                          Travel plans for this year so far include Russia, Thailand, Sri Lanka, Armenia (or perhaps Georgia), and Ukraine. My partner is a junior web developer, and she is now looking for her first remote job. All of my employees also work from wherever they want. If you’re curious about writing Haskell specifically: I don’t think anyone was going to hire me to do this. I had to start my own businesses, get funding, and build my own team of Haskell people.

                          Happy to answer most other questions you might have.

                          1. 1

                            Sounds amazing, your own Haskell business.

                            Care to elaborate more on what application domain you use Haskell for, if possible?

                            1. 4

                              All three businesses are web applications. One is in sales lead generation, one is in price comparison, and my primary focus is a marketplace product for the reinsurance industry. I’m using similar tech in all three: Yesod, PostgreSQL, Redis, NixOS, AWS.

                              1. 2

                                NixOS fits so well with Haskell ethos.

                                Very intereting to hear all this, thanks.