Threads for nickpsecurity

  1. 4

    Wrote 2000 words of thoughts on this! Here

    1. 2

      OP here. Thanks for writing such a detailed reply so quickly. It’s impressive!

      I generally agree with most of your points but I have some comments about a few items:

      My reference to a winter was a bit provocative to catch reader attention. But I think it was quite appropriate. Before the AI winter, all we had were brittle expert systems. I don’t think there was a huge industry interest, it was mostly academic and government funding. FM were pretty close by the mid 90s, just before Tony Hoare’s speech.

      The Vienna Development Method was popular in some scandinavian and germanic CS departments. I have met Bjørner, one of the developers, and refinements of this method were taught and used well into the late 2000s. I am familiar with some current railway systems developed using VDM derivatives. I actually worked on one. Interestingly, Bjørner’s son is behind Z3, together with De Moura.

      I like your point about Z3. In this regard, we should think about FM in a broader way. Type systems should be certainly included. Refinement (liquid) types are possible thanks to fancy SMT solvers. And refinement types are in many ways static DbC. In fact, some refinement types implementations push checks to runtime when they fail to prove something.

      Static analysis is often ignored when talking about FM, but it scales to massive codebases and it has had huge successes. Galois connections are a great conceptual framework, and fast Datalog implementations help a lot in reducing the complexity of implementations. I think static analysis is gaining a lot of momentum, and we will see many more static analyzers by the end of the decade.

      The last thing is that I wouldn’t discount major advances in theorem proving that automate many proofs using DL, augmenting the capabilities of things like Isabelle’s Sledgehammer. There are already promising publications in this avenue.

      1. 2

        Static analysis is often ignored when talking about FM, but it scales to massive codebases and it has had huge successes.

        Facebook’s Infer is a perfect example of that. It’s used on both C++ and Java codebases. There were concurrency checkers that looked at various orders code could execute to spot likely problems. Non-FM experts use Rust’s borrow checker to solve such problems with effectiveness that used to take separation logic that Infer uses internally. Runtime Verification Inc built a tool used in industry on a formal semantics of C that leads to low or no false positives. A Google tool and ForAllSecure’s Mayhem automatically try to fix the problems. On impact, Microsoft’s driver verifier probably deserves higher mention given both deployment numbers and nearly eliminating the blue screens.

        In academia or for hobbyists, many teams whose tools are entering competitions have been converging to use the same underlying codebase (CPA-Checker?). That they do means that a combo of them could be polished and packaged into an industrial tool. Other projects could generate automatic patches for whatever is found. Test generators could show equivalence on top of the benefits they already provide. If equivalent, automatically include the patch without even bothering to further analyze it. Lower and lower developer involvement with higher payoff (esp development velocity) = more adoption.

    1. 4

      This brings back fond memories of when I rescued an old AlphaStation from a customer’s recycling bin and installed OpenBSD on it.

      I do agree about the noise however, the thing was like a jet engine.

      1. 4

        At 266MHz, it’s a pretty slow Alpha - the later ones were even louder. There are lots of things I like about the Alpha but it was very much a system designed by hardware architects who didn’t ever talk to software people. The memory model was very exciting. One of the things that I hate the most about working with Linux is that the kernel memory model is defined in terms of the barriers that Alpha needs, not in terms of release / acquire semantics on objects (as C[++]11 did and the FreeBSD kernel adopted). Most operating systems have given up supporting SMP on Alpha because the memory model imposes a huge maintenance burden on everything else. When WG21 was working on atomics for C++11, compatibility with Alpha was an explicit non-goal.

        Floating point on the Alpha was very fast, at the expense of basically no synchronisation between integer and floating point pipelines. This made a bunch of things interesting, the most significant one was floating point exceptions. If you wanted to avoid paying around a 10x performance penalty, you needed to put floating point exceptions in imprecise mode and you’d then end up with an exception happening at a point in your program that was completely unrelated to the instruction that actually caused the fault. Floating point exceptions were basically a program-terminating event.

        Alpha also took RISC a bit beyond its logical conclusion. I suspect Alpha is the reason for things like int_fast8_t in C99. The Alpha had only 32- and 64-bit loads and stores. If you wanted to do a narrower load, you had to do a load and a shift / mask. A narrower store ended up being a read-modify-write.

        Everything was designed so that the hardware could retire insane numbers of instructions per second but the Alpha needed to be able to do this to compensate for the comparatively high dynamic instruction count compared to other architectures.

        1. 3

          “but it was very much a system designed by hardware architects who didn’t ever talk to software people. “

          I can’t speak to that. I do think the PALcode mechanism on Alpha’s was great for software people. Many things people want to do in OS’s, VM’s, transactions, etc could benefit from that today.

          One of the things I wanted someone to do with RISC-V CPU was to either implement PALcode-like feature or microcode one with HLL-to-microcode compiler (example pdf). If RaspPi-like board existed, hobbyists could build all kinds of experimental kernels and language runtimes on it with few to zero issues from abstraction gaps. A commercial, embedded offering might allow customization for competitive differentiation in performance, determinism, debuggability, or security of various platforms. A server version might do the same. Embedded providers customize more, though, with server-side adoption likely limited by the performance gap with existing, full-custom designs.

          1. 2

            I can’t speak to that. I do think the PALcode mechanism on Alpha’s was great for software people. Many things people want to do in OS’s, VM’s, transactions, etc could benefit from that today.

            I’m a huge fan of PALcode, though it was more useful on single-core systems than with SMP. You could do things like atomic append to queue in PALcode trivially on a single processor because the PALcode ran with interrupts disabled. On an SMP machine, you needed to acquire locks or build a lock-free data structure (very hard with Alpha’s memory model) and at that point you may as well implement it in userspace / kernelspace.

            One of the things I wanted someone to do with RISC-V CPU was to either implement PALcode-like feature or microcode one with HLL-to-microcode compiler

            PALcode on RISC-V is called ‘Machine Mode (M-Mode)’. On Arm it’s called Exception Level 3. Good ideas never completely die.

            That said, I would be interested in playing with a RISC-V version of Alto microcode, where each ‘instruction’ is just a byte that indexes into a table of microcode instructions so that you effectively have hardware assist for writing jump-threaded interpreters. You could probably make that quite fast today and I’d be really curious whether it would outperform an optimised bytecode interpreter.

          2. 2

            I honestly had no idea about any of this. I rescued it from the dumpster, hauled it to work(!), stuck it in a closet with a network connection and SSHd into it.

            It was mostly, “hey, free hardware!” with the added frisson of |D|E|C| hardware quality (I found a service manual which had hand-draughted illustrations) and exotic stuff like ECC memory. I didn’t know what I was doing, I wedged the entire system trying to do a make world and getting Perl dependencies wrong.

            1. 2

              I remember buying Computer Shopper in the ’90s and seeing adverts for 266MHz Alphas from a PC manufacturer in the inside cover. At the time, the fastest Pentium you could buy was 100MHz (and that seemed insanely fast). The Pentium Pro line at up to 200MHz came out at about that time, but then the Alpha workstations were at 500MHz. Even running emulated 32-bit x86 code, the Alphas with Windows NT were about as fast as the fastest Intel CPUs and running native code they were insanely fast. I really wanted one.

              This was pretty much the peak for the Alpha. As SMP and multithreading became more important, it struggled a bit. SMP with multiple single-threaded processes was more-or-less fine, the incredibly weak memory model wasn’t a problem when you had no shared memory between CPUs but it was a problem with multithreaded programs: things written for x86 (or even something like SPARC, which had a slightly less weak memory model) often didn’t work correctly on Alpha.

              Digital largely discontinued Alpha development to focus on Itanium and by the time the Pentium III passed 1GHz the Alphas weren’t really performance kings anymore. Itanium didn’t live up to its promise and there’s been a lot of speculation about what would have happened if Digital had pushed ahead with the EV8 Alphas instead. My guess is that Alpha would still be a dead architecture today, just one that died a few years later, but it’s also possible that they’d have extended the instruction set to support narrower loads and stores and made the memory model a bit stronger. It’s not clear whether it would have remained competitive. Around 2000 there was a shift back towards richer instructions sets: even Arm now tries not to describe itself as a RISC architecture, preferring the term ‘load-store architecture’. There’s a lot of benefit (in terms of store buffer / register rename complexity) in separating loads and stores from other operations but the amount of work you can do in a single pipelined instruction became much greater. I have no idea what an Alpha competitor to Arm’s Scalable Vector Extensions would have looked like and that’s the kind of thing that gives impressive performance wins today.

        1. 9

          So, I’m having a hard time following what the core of the critique here? It seems like the author:

          • Has beef with Clojure, because it models changes over time differently than CL does
          • Thinks that the core appeal of Lisp is the whole system being in one language, rather than trying to Layer Lisp Atop Other things
          • And then thinks that syntax matters a lot less than the environment (which I kinda follow?)

          I feel like I’m missing a lot of context here

          1. 4

            My understanding is that this is the core of the argument:

            In a similar fashion, I have attempted to illustrate a style of Common Lisp, in which the “language” is in fact an interactive programming system, features subsume multiple programming paradigms, occasionally “beating them at their own game”, and provides excellent efficiency for high-level, readable programs. Such a style is why one sticks around with a language; there is not another language with the described design strategies.

            And the rest is beating down every other model of Lisp for taking only bits of Lisp and still calling it Lisp (“selling Lisp by the pound”), which the author believes defeats the purpose of the whole interactive system thing.

            1. 4

              If that’s the core of their argument, then Factor and Smalltalk would also effectively be LISPs to, no?

              1. 2

                “subsume multiple programming paradigms”

                Can’t speak to Factor. Smalltalk might have it on image-based, readable, and maybe fast. Lisp can then add new paradigms by just adding a library. The language itself morphs to better express the solution, maybe multiple times in a program. People did it for OOP and AOP. Everything in a Rails-like framework might be DSL’s in the same ultra-fast, base language. Like with Rayon in Rust, the macros might make similar or the same constructs automagically handle goals like parallelism. Lots of flexibility aiming for lots of potential uses.

                If all Smalltalks have that, then they’d be comparable enough minus the syntax advantages. If not, it’s a tremendous advantage of Lisp if that’s an advantage. Detractors would think Smalltalk would be better the second the codebase was in maintenance mode. “No macros = easier-to-understand code,” they say. They’ll argue most uses of macros can be done with library calls easy enough in dynamic, generic, or whatever language. There’s counterpoints.

                Note: Quick look at Factor page says it’s stack-based. Might cancel multi-paradigm for it, too, if it’s more constrained than Lisp from whatever constraints being stack-based forced onto it.

                1. 2

                  Factor can have a large amount of DSLs in it, though, which is why I bring it up.

              2. 3

                Which is part of why I don’t describe Clojure as a LISP.

            1. 0

              Scriptural Context

              Let’s look more closely. They were given two, simple goals: love God and put Him first; love your neighbor as yourself. The Torah says God was pleased with His faithful, loving servants (eg Enoch, Abraham) before the Law of Moses existed. Being about a relationship, He looked at their hearts more than anything. He describes His commitment to Israel like a faithful marriage to an unfaithful partner He keeps salvaging per their Psalms and historical Scriptures. The Jews might have easily fulfilled their requirements by just focusing on the actual goals: faithfulness to God, love for others. What happened?

              Two things: rebellion and ego. Like everyone, their Scripture says all people rebel against God and good to varying degrees. Israel’s rebellion was constant. They’d also get technical with or corrupt His Law to try to skirt, not follow, moral responsibility. If you doubt that, note the people God had just miraculously saved in Egypt were building a false god while Moses was talking to the real one on their behalf. Shows both their loyalty and mentality.

              On ego, their leaders later ignored the lens of “How to love God and others in humane way?” to pile on endless technicalities that were totally inhumane and which God never commanded. Their elites lorded it over others in a self-righteous way. Jesus repeatedly called out the Pharisees as fake people with no love in their hearts who laid impossible burdens on people they were supposed to care for. Then, delivered His Gospel, much simpler, that they were supposed to have been looking for per their own prophecies.

              Worldly Context: Lessons Learned

              Let’s look at it from a secular, technological lens. The above differences argue strongly for goal-based, not rule-driven, development. You start with the hopefully-clear goals. If hard rules exist, you follow those since you have to. Where there’s not a rule, you pause to look at the goal, come up with potential responses, and consider the human cost. That the Law was meant for their own good means what you add should be necessary and good. One cost is people just can’t track so many rules in their head. Only add what you have to. Also, don’t equate people’s slip-ups on rules for edge cases with willful disobedience of clear orders. Also, patiently, kindly disciple your students regardless of their background. These are practical lessons from Jesus’ goal-focused ministry that contrast nicely with the rule-heavy regime of His opponents.

              “Turning that into “a programming exercise” is a pretty egregious case of cultural appropriation.”

              Well, they were told to be inclusive and impartial to foreigners. That’s how foreigners in enemy lands were saved. Then, their Messiah that their Scriptures told them to watch for (example) said it’s all over with (fulfilled). He’d take that heavy burden (yoke) off of them so they could just walk with their God as they were meant to. He ordered His servants to share the old and new stuff with the Gentiles (non-Jews). The Jewish God intended to include the world in His salvation out of incredible love for every, lost child.

              At this point, it’s something that was more God’s than theirs, got corrupted as they missed the point, became the human-made mess you described, and even the correct stuff they were supposed to let go of to obtain what they were promised which is now available. Feel free to talk about it. In the USA at least.

              1. 6

                I would have liked to tag this article with datastructures but there is no such tag.

                1. 6

                  compsci tends to be the correct goto for that stuff. :)

                  1. 1

                    On top of it, using CompSci neans that clicking the tag will teach them data structures, algorithms, optimizations, and more!

                1. 6

                  One potential limitation is that compute shaders are a relatively new feature, and are only available in GPUs made in the last five-or-so years.

                  Something to watch out for with GPU-based 2D rendering in general is that it might unnecessarily make the application unusable on older hardware. I’m reminded of a sad case involving WPF about a decade ago: a Bible study application where the choice of video card actually mattered. I know about this particular case because it affected my brother when he tried to run that program on an older laptop. I find it sad that, as shown by the linked forum thread, people had to take time away from their real work to discuss video cards. And bear in mind that the application in question was basically a specialized text viewer and editor.

                  1. 2

                    Interesting to see that even in a forum of people that probably care a lot about ethics, you’ll see this comment:

                    Intel graphics are the worst!

                    I thought at least these people would care more about freedom than about performance. But I guess not.

                    1. 1

                      Well, it’s a Christian forum rather than one on ethics in general. Many Christians aren’t concerned much about those things due to the sovereignty if God. As in, how He exerts His will on all things to accomplish His purposes regardless of the schemes of men. From the past (eg Ninevah in Nahum or reforming Israel) to future (eg Revelation), He’s not stopped by much worse oppression and corruption than software licensing. Ex: The number of believers growing massively in China despite the Chinese regularly jailing them. Similary, but smaller numbers, in North Korea. His Word and Will are unstoppable.

                      We’re also to be judged for how much we loved/served God and other people. The love others is things like feeding them, equipping them, being kind, listening, etc. Obviously, bringing them to Christ as well for redemption, peace, and purpose. I’ve personally found I can’t do those things while simultaneously spending lots of time tinkering with FOSS. I’ve cut way, way back on tech to invest in both God’s Word and other people with Him moving consistently.

                      Finally, there’s the fact that believers in Christ get the Holy Spirit to transform us but we’re still human. Our human nature remains till death. Centering on Christ supernaturally transforms in gradual way us to give more of His traits if we stay on it. Jesus says His people will bear His fruits (i.e. character). 1 John 3 has stronger words. If they don’t or are casual about it, human traits dominate with a group of them acting like any other. For instance, not caring about software freedom and griping about electronics is extremely normal. We are to call out evil, though. Grey area on graphics cards. ;)

                  1. 25

                    How has AGPL failed? Quoting the introduction to Google’s own policies, which are the top hit for “agpl google” on DuckDuckGo:

                    WARNING: Code licensed under the GNU Affero General Public License (AGPL) MUST NOT be used at Google. The license places restrictions on software used over a network which are extremely difficult for Google to comply with.

                    This seems like a resounding success of AGPL.

                    Proprietary distributed systems frequently incorporate AGPL software to provide services.

                    Who, and which software packages? This isn’t just about naming and shaming, but ensuring that those software authors are informed and get the chance to exercise their legal rights. Similarly, please don’t talk about “the legal world” without specific references to legal opinions or cases.

                    I feel like this goes hand-in-hand with the fact that you use “open source” fourteen times and “Free Software” zero times. (The submitted title doesn’t line up with the headline of the page as currently written.) This shows an interest in the continued commercialization of software and exploitation of the commons, rather than in protecting Free Software from that exploitation.

                    1. 8

                      How has AGPL failed?

                      I said how in the article:

                      The AGPL was intended, in part, to guarantee this freedom to users, but it has failed. Proprietary distributed systems frequently incorporate AGPL software to provide services. The organizations implementing such systems believe that as long as the individual process that provides the service complies with the AGPL, the rest of the distributed system does not need to comply; and it appears that the legal world agrees.

                      The purpose of the AGPL is not to stop commercial users of the software, it’s to preserve the four freedoms. It doesn’t preserve those freedoms in practice when it’s been used, so it’s a failure.

                      But really AGPL doesn’t have anything to do with this. No-one claims AGPL is a license like the one I describe in the article.

                      Proprietary distributed systems frequently incorporate AGPL software to provide services.

                      Who, and which software packages?

                      mongodb is a high-profile example, used by Amazon.

                      1. 10

                        I’m fairly certain that the version of mongodb that Amazon based DocumentDB off of was Apache licensed, so I don’t think that applies here. From what I’m seeing, they also explicitly don’t offer hosted instances of the AGPL licensed versions of Mongo.

                        1. 5

                          But really AGPL doesn’t have anything to do with this. No-one claims AGPL is a license like the one I describe in the article.

                          Then your article headline is misleading, is it not?

                          1. 2

                            This is true. MongoDB changed their license, in response to Amazon using forks of their own software to compete with them.

                            1. 1

                              That’s fair, you’re probably right. There are lots of other hosted instances of MongoDB that used the AGPL version though, so MongoDB is still the highest-profile example of this. That was the motivation for MongoDB’s move to SSPL.

                            2. 2

                              I don’t see a laundry list here. I appreciate that you checked your examples beforehand and removed those which were wrong, but now there’s only one example left. The reason that I push back on this so heavily is not just because I have evidence that companies shun AGPL, but because I personally have been instructed by every employer I’ve had in the industry that AGPL code is unacceptable in their corporate environment, sometimes including AGPL developer tools! It would have been grounds for termination at three different employers, including my oldest and my most recent employments.

                              Regarding MongoDB, I have no evidence that AWS violated the terms of the AGPL, and they appear to have put effort into respecting it somewhat. It seems that MongoDB’s owners were unhappy that their own in-house SaaS offering was not competing enough with others, and they chose licensing as their way to fight. Neither of these companies are good, but none of them appear to be disrespecting the AGPL.

                            3. 4

                              the agpl says

                              Notwithstanding any other provision of this License, if you modify the Program, your modified version must prominently offer all users interacting with it remotely through a computer network (if your version supports such interaction) an opportunity to receive the Corresponding Source of your version by providing access to the Corresponding Source from a network server at no charge, through some standard or customary means of facilitating copying of software.

                              in other words, you cannot run your own proprietary fork of an agpl program; you have to offer users the modified sources. it says nothing about the sources of the other programs that that program communicates with, or the network infrastructure and configuration that comprises your distributed system.

                              1. 3

                                Yes. This is how we define distributed systems, in some security contexts: A distributed system consists of a patchwork network with multiple administrators, and many machines which are under the control of many different mutually-untrusting people. Running AGPL-licensed daemons on one machine under one’s control does not entitle one to any control over any other machines in the network, including control over what they execute or transmit.

                                Copyright cannot help here, so copyleft cannot help here. Moreover, this problematic layout seems to be required by typical asynchronous constructions; it’s good engineering practice to only assume partial control over a distributed system.

                                1. 1

                                  So, that seems fine then? What’s the problem with that?

                                  1. 1

                                    the problem, as the article says, is that we have no copyleft license that applies to entire distributed systems, and it would be nice to. not so much a problem with the agpl as an explanation of why it is not the license the OP was wishing for.

                                    1. 4

                                      I explain more upthread, but such licenses aren’t possible in typical distributed systems. Therefore we should not be so quick to shun AGPL in the hopes that some hypothetical better license is around the corner. (Without analyzing the author too much, I note that their popular work on GitHub is either MIT-licensed or using the GH default license, instead of licenses like AGPL which are known to repel corporate interests and preserve Free Software from exploitation.)

                                      1. 2

                                        We have Parity as a start. Its author says:

                                        “Parity notably strengthens copyleft for development tools: you can’t use a Parity-licensed tool to build closed software. “

                                        Its terms are copyleft for other software you “develop, operate, or analyze” with licensed software. That’s reads broad enough that anything an operator of distributed systems both owns and integrates should be open sourced.

                                1. 3

                                  My cognitive dissonance is off the charts these days with Microsoft. Are they the goodies?

                                  1. 24

                                    They are a big company doing many different things. It saves a lot of heartache to ditch the goodie/baddie scale and consider each activity on its merits. And in this case I think they’re onto something good. I for one would sacrifice 10-50% JS speed to rule out an entire class of common security bugs.

                                    1. 2

                                      ditch the goodie/baddie scale and consider each activity on its merits.

                                      I gradually changed to this thinking approach after I crossed 33-34, however I struggle to communicate this thinking approach to people. Is there a name for this mental model?

                                      1. 5

                                        People are complex, organizations change over time. Initial impressions matter a large amount, but people who are interested update their opinions on the basis of new information, while retaining history.

                                        One way to do this is bayesian estimation. The two primary problems with bayesian estimation are that people are no good at keeping track of their priors and are no good at estimating new probabilities.

                                        It is reasonable to assume that Microsoft, at any time, is doing something clever, something stupid, and a lot of things that they think will make them money in a medium-term future.

                                        1. 1

                                          Right tool for the job. It almost always redirects the conversation to the technical merits than moral policing. That does not mean moral and ethical considerations are useless, it just helps better calibrate the discussion.

                                    2. 17

                                      They are:

                                      • Giving schools free copies of their office package in order to maintain their OS and productivity software dominance on the desktop.
                                      • Lobbying public sector heavily to get locked into Azure.
                                      • Using their dominant position to get the whole public sector as well as kids and students onto Teams and O365 with a recurring subscription.
                                      • Cross selling One Drive heavily on their non-enterprise Windows editions.
                                      • Showing ads and install bloatware in their non-enterprise Windows editions.

                                      They want nothing else than total platform dominance and they don’t care about the little people, obviously. The question is, do you consider total dependence of our administrations and of the less-well-off on them a goodie?

                                      1. 4
                                        • Microsoft fights to get big Pentagon contracts. GitHub can’t even drop a small ICE contract, because Microsoft doesn’t want to offend the military-industrial complex.
                                        1. 3

                                          Thank you.

                                          1. 6

                                            No problem.

                                            They also care about developers and fund some important research, so it’s not all black & white. Just to be fair.

                                          2. 1

                                            Google, Amazon, Apple, etc do things too, it’s not like MS is alone in their, MY PLATFORM ONLY perspective.

                                            1. 1

                                              True, but I have yet to see GAA employees to write local laws.

                                              I am pretty sure their lobbyist are real busy in Brussels and Washington, though.

                                          3. 8

                                            I think, very approximately, corporations which sell platforms tend to act like arseholes when they have the upper hand (in terms of network effects and lock-in) and saintly when they don’t.

                                            e.g. 10-14 years ago, with win32 being the juggernaut of “we already sunk cost into desktop apps on this platform” and the iPhone only just being released, Microsoft were barely even bothering to disguise their efforts to extinguish open protocols. Meanwhile Apple were pushing html5 hard as the big thing that would allow software to work beautifully on all platforms.

                                            Whereas now we have Microsoft very much less dominant and Apple have a near monopoly on phones purchased by the subset of users who spend money on their phones. So Microsoft are promoting open everything, and Apple are doing things like strategically dragging their feet on html5 features, adding horrendous bugs to iOS Safari and not fixing them for months to years.

                                            1. 5

                                              Nope. I think they’re doing a great job of “embrace” though.


                                              1. 5

                                                No such thing–these companies look out for themselves, period. But you are better off with more than one company duking it out, because to compete they will (sometimes) do things that are pro-consumer or pro-developer or whatever.

                                                Microsoft on top of the world tried to keep the Web stagnant once they’d killed Netscape, and undermined the growth of Linux and GPL software every way they could. Microsoft as a bit more of an underdog likes Web standards, runs GitHub, and builds the favorite open-source dev environment of a bunch of new coders.

                                                Same with, for example, AMD and Intel. AMD got competitive and prices of high-core-count chips plummeted–great! Now with a chip shortage and a solid follow-up product, AMD is in a position to start raising prices, and they are. Intel getting its manufacturing improvements on track would probably give us more of a price war in certain segments, not less!

                                                I’m old enough to remember when AWS was exciting to smaller devs because you didn’t have to shell out upfront for servers or provision far in advance for spiky loads. 🤣 Now it’s a huge profit center for Amazon and there are plenty of justifiable complaints about pricing (notably for egress) and undermining open-source-centric companies by using their market position to compete with the product developer’s own managed offerings.

                                                Tactically, I guess I want underdogs to reach competitiveness, and for companies to see some benefit to doing good things (e.g. open sourcing things) and cost to bad ones (e.g. pushing out little companies) even when the immediate economic incentives point the wrong way. But in the long run all these companies respond to their economic situation and none of them are your friend.

                                                1. 4

                                                  It doesn’t really make much sense to blame the moral character of individual actors when there’s a system of incentives and punishments driving things. If a big company were all saints and angels, they’d be out competed by another company that was willing to play the cutthroat game to maximum advantage. (And sometimes it is worth noting playing the cutthroat game to maximum advantage means doing good things, and sometimes good things come out of bad actions too, but if the market+political winds shift, they’ll (eventually) shift with it or go out of business.)

                                                  They’re doing what they think will make them money without getting another nasty visit from the government regulators. So is Google and Apple and Mozilla. None are good or bad per se, they’re all just navigating the same sea.

                                                  1. 3

                                                    I’ll add to mordae that they were using legal muscle to extract billions in patent royalties from Android. I saw one article claim that stopped. I haven’t followed it in a while. You could check to see if they still patent troll others in general. I mean, that’s clearly evil.

                                                    On showing ads, the traditional logic for desktop software, games, etc is that people who pay don’t see ads. Microsoft started putting ads in paid products, including the Xbox. After gamers protested, they expanded how many were on the screen instead of reduced it.

                                                    One might also count the integration between single-player games with Xbox Live. I shouldn’t have to login to an online service to play an offline game. If I am offline, I shouldn’t lose access to my progress, items, etc. I recall having to deal with stuff like that on Xbox. The nature of online service is they eventually discontinue it for some products and services. Then, they’ll stop working at all or not work as well. All of this is done to maximize sales of new products using Microsoft’s and their suppliers’ platforms.

                                                  1. 5

                                                    I always think of security of software massive companies are using as more a labor problem. It’s in their nature to keep billions in profit. They’ll spare only a slice. Can they spare enough of a slice to hire the developers to fix Linux? And, since it’s Google, Android as well?

                                                    Three figures helped me understand this a while back:

                                                    1. The cost of Solaris 10. It was a rewrite project to modernize a commercial UNIX. Fans of the open-source projects derived from it say it paid off. This gives an idea what their own high-quality, more-secure, clean-slate option might cost.

                                                    2. The cost, in size and/or funding, of groups such as PaX Team, OK Labs, and GrapheneOS. Add in academic teams who did things like add memory safety to FreeBSD kernel or Linux apps. Maybe ExpressOS. These give an idea how much it might cost to make one or more dramatic improvements to Linux, Android, etc.

                                                    3. Google makes billions in revenue on Android. Others making massive fortunes on Linux or Linux-based tech include IBM, Amazon, and defense contractors.

                                                    Yeah, they could do it by themselves if they wanted. That confirms the damage is an externality to them. They’ll put in some kind of effort, leave most of the job undone, and do that even when the cost is almost nothing to them.

                                                    1. 3

                                                      You need to think about opportunity cost. $1 invested in security is $1 not invested in something else. The security investment is competing with things that customers are demanding. How many people will buy an Android phone instead of an iOS phone if Android ships with security feature X? How does this compare with the number of people that will buy an Android phone instead of an iOS phone if Android supports 200 new emoji? Even a big company like Google has a finite number of engineers and needs to prioritise their work. New features sell products, security improvements don’t (outside of a few markets).

                                                      This would probably change a lot if regulation increased liability for vulnerabilities, but it’s not clear how that would work with open source projects. Some random person accidentally introduces a vulnerability into Linux, Google packages it up in AOSP, Samsung ships a phone with Samsung’s Android version built on top of AOSP, who should be liable if an end-user’s phone is compromised?

                                                      1. 1

                                                        The opportunity cost-based accounting only works if there is no liability for shipping shitty/insecure software. If only we could put an end to that…

                                                        1. 1

                                                          You need to think about opportunity cost. $1 invested in security is $1 not invested in something else.

                                                          It’s true that businesses consider this. It might even be what Google was doing. You’ll know that if Google is, like Amazon, steadily building things that might become products, keeping an eye out for what customers love, and turning those into long-term, supported products with revenue. Instead, we see a trend at Google where they consistently create excellent tech with lots of users, sometimes taking over a niche, before canceling that tech. It’s like they don’t even try to make their investment pay off in any way. Looking at their cloud vs Amazons, it’s clear Amazon’s customer focus is whats causing them to pound away at Google. What we see can’t possibly be Google being clever about what customers want.

                                                          On security side, we see a demand for security. Google pushed Chrome on both performance and security via Native Client. They promote projects like BeyondTrust and Titan. Back on demand side, we see damaging stories in the media comparing malware rates on iOS vs Android. It’s a differentiator for iOS you’d think they’d want to eliminate. Further, there’s always been a demand for a private, at least enterprise and government, variant of Android. There’s a hard-to-estimate niche for people that pay to turn off ads. That means it’s a wise move for these companies to make a more secure version with all tracking and ads turned off priced at whatever tracking/ads bring plus some profit. Privacy-conscious customers often pay a premium for it. So, they could increase the profit margin on that. It’s telling that they haven’t even tried despite both FOSS projects and small businesses showing how low cost it would be for Google to set that up.

                                                          Saying they’re handling priorities really well is too charitable after all their missed opportunities, canceled products, and wasteful projects. Best explanation is a combination of (a) they don’t care about security for many reasons (including harder-to-sell ROI) and (b) marketing ineptitude.

                                                          “This would probably change a lot if regulation increased liability for vulnerabilities”

                                                          I agree. I go further wanting both regulation and liability. I’ve promoted regulation since the TCSEC (pdf) and DO-178B proved corporations will respond to it. Whole ecosystems, from reusable components to tools for building them, emerged from both sets of regulations. That makes regulations the only thing that’s proven to work. From there, I just looked to how to do it better: goal-based vs prescriptive, lower costs, more automation, etc.

                                                          Liability is a different issue. We’ve seen the class actions in other industries achieve risk reduction. From there, it becomes some kind of game of what profitable evil they might get away with, what the lawsuits will cost, and if one is higher than the other. We need to make sure whatever they’re getting hit for is actionable. We also need to set the fines or damages at many times higher than whatever preventing them cost. Then, if that’s consistently enforced, those doing it will clearly have just acted unreasonable under reasonable, professional standard.

                                                          So, a mix of regulation and liability.

                                                        2. 2

                                                          They probably would rather put their efforts into Fuscia. The Linux kernel is a bit of a commodity these days, with every tech company maintaining some level of contribution and aptitude for it. The result is less control for any individual company, which we love, but they can’t stand (see browser wars)

                                                          1. 2

                                                            That’s a good theory. Lots of them like control and GPL elimination. It seems like it’s why router vendors go proprietary when better stuff is available under BSD. Let’s not forget long-term, lock-in opportunities. Google seems to be in that camp looking how Google Apps/Play agreements with Android manufacturers.

                                                        1. 1

                                                          Far as runtime, author could test it again mature CL’s or Schemes. That might give an idea.

                                                          1. 6

                                                            My favorite part of it was its security technology (pdf) that Secure64 built a DNS product on. That PDF is an advertisement but describes its mechanisms. With all the papers I’ve submitted, I imagine we could’ve seen a lot of interesting stuff if some of those designs built on Itanium’s hardware support. Esp to hardware-accelerate or further isolate specific parts of them. To get readers thinking, an example would be how Code-Pointer Integrity cleverly used segments to do an important part of its design at high speed and isolation.

                                                            Another benefit of RISCy architectures is that they’re not inherently tied to how C’s abstract machine works. In theory, you have enough registers to keep a large pile of internal state for alternative designs. Most x86 alternatives weren’t as fast and cheap as x86, though. Whereas, Itanium was at least really fast with more memory addressing. There was a lot of potential for alternative paradigms to take off by targeting it so long as enterprises could buy them (esp as appliances). That Secure64 did a good job trying to do that is why I mention them in Itanium discussions.

                                                            One immediate use it had was in NUMA machines. SGI’s Altix used them. Its Prism variant was the system gamers dreamed about having (Onyx2 on MIPS before that). You can scale up critical workloads without the programming headaches of using a cluster. It was just multithreading with some consideration applied to data locality.

                                                            One more benefit was reliability technology. Quite a few failures in mission-critical systems come from hardware issues developers can’t see. Even in clusters, making the individual chips more reliable reduces odds of failures in them taking down the whole thing. Especially when they use the same CPU. The Itanium had improvements in this area, I think NUMA/mainframe vendors (eg Clearpath) took advantage of that, and eventually Xeons got most or all of those features. For a while, Itanium-based designs might have crashed less.

                                                            Unfortunately, most potential adopters just asked, “Can I compile my existing code on my existing system to get it to go much faster with 64-bit support?” Answer was no. Then, AMD won by focusing on and accelerating legacy code on an ISA compiler writers already optimized their stuff for, too.

                                                            This was Intel’s third attempt, after i432 and i960 (awesome), to get people off legacy. They lost billions of dollars in ambitious attempts. Today, people gripe that Intel architecture has all kinds of security issues. They should’ve rewritten or patched the architecture. If anything, Intel took more risks than everyone with losses so high I’d be surprised if they take any more.

                                                            1. 2

                                                              Unfortunately, most potential adopters just asked, “Can I compile my existing code on my existing system to get it to go much faster with 64-bit support?” Answer was no. Then, AMD won by focusing on and accelerating legacy code on an ISA compiler writers already optimized their stuff for, too.

                                                              Similar story with HTM.

                                                              1. 1

                                                                Azul was great, too! Seemed like they were beating the averages. Then, they ditched IIRC the hardware product. I might watch that.

                                                            1. 17

                                                              This article has everything: databases, rad, different visions of computing as a human field of endeavor, criticism of capitalism. I commend it to everyone.

                                                              1. 13

                                                                Criticism of capitalism is, in theory, my main thesis, but I find it difficult to convey in a way that doesn’t get me a lot of angry emails with valid complaints, because the issue is complex and I can’t fully articulate it in a few paragraphs. But it is perhaps my core theory that capitalism has fundamentally diminished the potential of computing, and I hope to express that more in the future.

                                                                1. 3

                                                                  But it is perhaps my core theory that capitalism has fundamentally diminished the potential of computing, and I hope to express that more in the future

                                                                  I am on a team that is making a documentary about the history of personal computing. One of the themes that has come out is how the kind of computing that went out to consumers in the early 80s on was fundamentally influenced by wider socioeconomic shifts that took place beginning in the 70s (what some call a “neoliberal turn”). These shifts included, but were not limited to, the elevation of shareholder primacy and therefore increased concentration on quarterly reports and short-termism.

                                                                  These properties were antithetical to those that led to what we would say were the disproportionate advances in computing (and proto-personal computing) from the 50s, 60s, and 70s. Up until the 80s, the most influential developments in computing research relied on long-term, low-interference funding – starting with ARPA and ultimately ending with orgs like PARC and Bell Labs. The structures of government and business today, and for the past few decades, are the opposite of this and therefore constitutionally incapable of leading to huge new paradigms.

                                                                  One more note about my interviews. The other related theme that has come out is that what today we call “end user programming” systems were actually the goal of a good chunk of that research community. Alan Kay in particular has said that his group wanted to make sure that personal computing “didn’t become like television” (ie, passive consumption). There were hints of the other route personal computing could have gone throughout the 80s and 90s, some of which are discussed in the article. I’d add things like Hypercard and Applescript into the mix. Both were allowed to more or less die on the vine and the reasons why seem obvious to me.

                                                                  1. 1

                                                                    These properties were antithetical to those that led to what we would say were the disproportionate advances in computing (and proto-personal computing) from the 50s, 60s, and 70s. Up until the 80s, the most influential developments in computing research relied on long-term, low-interference funding – starting with ARPA and ultimately ending with orgs like PARC and Bell Labs. The structures of government and business today, and for the past few decades, are the opposite of this and therefore constitutionally incapable of leading to huge new paradigms.

                                                                    This is something I’ve been thinking about a while - most companies are incapable of R&D nowadays; venture capital funded startups have taken a lot of that role. But they can only R&D what they can launch rapidly and likely turn into a success story quickly (where success is a monopoly or liquidity event).

                                                                  2. 3

                                                                    As with so many things. But I think mass computing + networking and our profession have been instrumental in perfecting capitalism.

                                                                    Given the values that were already dominating society, I think this was inevitable. This follows from my view that the way out is a society that lives by different values. I think that this links up with our regularly scheduled fights over open source licenses and commercial exploitation, because at least for some people these fights are at core about how to live and practice our craft in the world as it is, while living according to values and systems that are different from our surrounding capitalist system. In other words, how do we live without being exploited employees or exploiting others, and make the world a marginally better place?

                                                                    1. 2

                                                                      Complaints about the use of the word, and maybe calling you a socialist, or something?

                                                                      I wouldn’t do that to you, but I do have to “mental-autocorrect” capitalism into “We may agree software developers need salary and some SaaS stuff is useful, but social-media-attention-rent-seekers gain power, which sucks, so he means that kind of ‘capitalism’”.

                                                                      There should be a word, like cronyism is the right word for what some call capitalism, or a modifier like surveillance capitalism.

                                                                      1. 3

                                                                        But I am a socialist. The problem is this: the sincere conviction that capitalist organization of global economies has diminished human potential requires that I make particularly strong and persuasive arguments to that end. It’s not at all easy, and the inherent complexity of economics (and thus of any detailed proposal to change the economic system) is such that it’s very difficult to express these ideas in a way that won’t lead to criticism around points not addressed, or of historic socialist regimes. So is it possible to make these arguments about the history of technology without first presenting a thorough summary of the works of Varoufakis and Wolff or something? I don’t know! That’s why I write a blog about computers and not campaign speeches or something. Maybe I’m just too burned out on the comments I get on the orange website.

                                                                        1. 1

                                                                          Sure, I appreciate that, though it would maybe attract bad actors less if there was some thread of synopsis that you could pull on instead of “capitalism”.

                                                                          I think the problem is broad terms, because they present a large attack surface, though I do realize people will also attack outside the given area.

                                                                          I’m also saddened by a lot of what’s going on in ICT, but I wouldn’t attribute it blindly to “capitalism”, but I don’t have all the vocabulary and summaries, if you will, to defend that position.

                                                                          One’s capitalism is anyway different from another’s, so the definitions must be laid out. Maybe all of Varoufakis isn’t needed every time?

                                                                          Nor am I convinced we’ll reach anything better with socialist or other governmental interventions. An occasional good law may be passed, or money handouts that lead to goodness, but each of those will lose in the balance to detrimental handouts/malfeasance, corruption, unintended consequences, and bad laws.

                                                                          Maybe some kind of libertarian-leaning world where people have a healthy dose of socialist values but are enlightened enough to practice them voluntarily?

                                                                      2. 1

                                                                        I would love to see the hoops you jump through to express that. Honestly. It seems so alien to my worldview that anyone making that claim (beyond the silly mindless chants of children which I’m assuming is not the case here) would be worth reading.

                                                                        1. 8

                                                                          I’ve made a related argument before, which I think is still reasonably strong, and I’ll repeat the core of here.

                                                                          In my experience, software tends to become lower quality the more things you add to it. With extremely careful design, you can add a new thing without making it worse (‘orthogonal features’), but it’s rare that it pans out that way.

                                                                          The profit motive drives substantial design flaws via two key mechanisms.

                                                                          “Preventing someone from benefiting without paying for it” (usually means DRM or keeping the interesting bits behind a network RPC), and “Preventing someone from churning to another provider” (usually means keeping your data in an undocumented or even obfuscated format, in the event it’s accessible at all).

                                                                          DRM is an example of “adding a new thing and lowering quality”. It usually introduces at least one bug (sony rootkit fiasco?).

                                                                          Network-RPC means that when your network connection is unreliable, your software is also unreliable. Although I currently have a reliable connection, I use software that doesn’t rely on it wherever feasible.

                                                                          Anti-churn (deliberately restricting how users use their own data) is why e.g. you can’t back up your data from google photos. There used to be an API, but they got rid of it after people started using it.

                                                                          I’m not attempting to make the argument that a particular other system would be better. However, every human system has tradeoffs - the idea that capitalism has no negative ones seems ridiculous on the face of it.

                                                                          1. 1

                                                                            Those are shitty aspects to a lot of things, and those aspects are usually driven by profits, although not always the way people think. I’ll bet dollars to donuts that all the export features Google removes are done simply because they don’t want to have to support them. Google wants nothing less than they want to talk to customers.

                                                                            But without the profit motive in the first place, none of these things would exist at all. The alternatives we’ve thought up and tried so far don’t lead to a world without DRM, they lead to a world where media is split into that the state approves and nobody wants to copy, and that where possession of it gets you a firing squad, whether you paid or not.

                                                                            1. 6

                                                                              But without the profit motive in the first place, none of these things would exist at all.

                                                                              It’s nonsensical to imagine a world lacking the profit motive without having any alternative system of allocation and governance. Nothing stable could exist in such a world. Some of the alternative systems clearly can’t produce software, but we’ve hardly been building software globally for long enough to have a good idea of which ones can, what kinds they can, or how well they can do it (which is a strong argument for the status quo).

                                                                              As far as “made without the profit motive” go, sci-hub and the internet archive are both pretty neat and useful (occupying different points on the legal-in-most-jurisdictions spectrum). I quite like firefox, too.

                                                                          2. 3

                                                                            “Capitalism” is a big thing which makes it difficult to talk about sensibly, and it’s not clear what the alternatives are. That said, many of the important aspects of the internet were developed outside of commercial considerations:

                                                                            • DARPA was the US military

                                                                            • Unix was a budget sink because AT&T wasn’t allowed to go into computing, so they just shunted extra money there and let the nerds play while they made real money from the phone lines

                                                                            • WWW was created at CERN by a guy with grant money

                                                                            • Linux is OSS etc.

                                                                            A lot of people got rich from the internet, but the internet per se wasn’t really a capitalist success story. At best, it’s about the success of the mixed economy with the government sponsoring R&D.

                                                                            On the hardware side, capitalism does much better (although the transistor was another AT&T thing and NASA probably helped jumpstart integrated circuits). I think the first major breakthrough in software that you can really peg to capitalism is the post-AlphaGo AI boom, which was waiting for the GPU revolution, so it’s kind of a hardware thing at a certain level.

                                                                            1. 2

                                                                              I still disagree, but man it’s nice to just discuss this sort of thing without the name-calling and/or brigading (or worse) you see on most of the toobs. This sort of thing is pretty rare.

                                                                            2. 2

                                                                              Obviously not op, but observe the difference between the growth in the scale and distribution of computing power, and what has been enabled, over the last 40 years.

                                                                              Business processes have been computerized and streamlined, entertainment has been computerized, and computerized communications especially group communications like lobsters or other social media have arrived. That’s not nothing, but it’s also nothing that wasn’t imaginable at the start of that 40 year period. We haven’t expanded the computer as a bicycle of the mind - consider simply the lack of widespread use of the power of the computer in your hand to create art. I put that lack of ambition down to the need to intermediate, monetize, and control everything.

                                                                              1. 1

                                                                                And additionally the drive to drive down costs means we have much less blue sky research and ambition; but also means that things are done to the level that they’re barely acceptable. We are that right now with the security situation: everything is about playing whackamole quicker than hackers, rather than investing in either comprehensive ahead of time security practices or in software that is secure by construction (whatever that would look like).

                                                                            3. 1

                                                                              What I used to tell them is it’s basically a theory that says each person should be as selfish as possible always trying to squeeze more out of others (almost always money/power), give less to others (minimize costs), and put as many problems on them as possible (externalities).

                                                                              The first directly leads to all kinds of evil, damaging behavior. There’s any number of schemes like rip-offs, overcharging, lockin, cartels, disposable over repairable, etc. These are normal, rather than the exception.

                                                                              The second does every time cost-cutting pressure forces the company to damage others. I cite examples with food, medicine, safety, false career promises, etc. They also give less to stakeholders where fewer people get rewarded and get rewarded less for work put in. Also, can contrast to utilitarian companies like Publix that gives employees benefits and private stock but owners still got rich. Or companies that didn’t immediately lay off workers during recessions. An easy one is most can relate to is bosses, esp executives, paid a fortune to do almost nothing for the company vs workers.

                                                                              Externalities affect us daily. They’re often a side effect of the other two. Toxic byproducts of industrial processes is a well known one. Pervasive insecurity of computers, from data loss to crippling DDOS’s to infrastructure at risk, is almost always an externality since the damage is someone else’ problem but preventing it would be supplier’s. You see how apathy is built-in when the solution is permissible, open-source, well-maintained software and they still don’t replace vulnerable software with it.

                                                                              Note: Another angle, using game of Monopoly, was how first movers or just lucky folks got an irreversible, predatory advantage over others. Arguing to break that up is a little harder, though.

                                                                              So, I used to focus on those points, illustrate alternative corporate/government models that do better, and suggest using/tweaking everything that already worked. Meanwhile, counter the abuse at consumer level by voting with wallet, sensible regulations anywhere capitalist incentives keep causing damage, and hit them in court with bigger damages that preventing it would cost. Also, if going to court, I recommend showing where it was true how easy or inexpensive prevention was asking the court basically orders it. Ask them to define reasonable, professional standard as not harming stakeholders in as many cases as possible.

                                                                              Note: Before anyone asks, I don’t have the lists of examples anymore or just inaccessible. Side effect of damaged memory is I gotta stay using it or I lose it.

                                                                          1. 3

                                                                            I wonder if the team considered writing the data store backend as a library in Rust, with Ruby bindings. That way it could run in-process, without the overhead of IPC or network round-trips. Rust provides strong static typing like Haskell, so the team would still have gotten the benefits of that.

                                                                            1. 15

                                                                              We didn’t consider Rust, but we did, as documented, build a sidecar app at first which brought latency down low enough. I’d be excited to adopt some Rust at NoRedInk though!

                                                                              Our experience with Haskell has been great, and the learning curve is particularly shallow when all of our developers already write Elm.

                                                                              The reason to pull out to a new service (as well as the reason to avoid different technologies) often has to do with decision fatigue rather than optimal architecture: We’ve built a nice template for an HTTP service in Haskell with, for instance, nice monitoring, deployments, etc.

                                                                              Moving to a new language takes time to make all of the right decisions. The same is true for service shape. How do we monitor, set up permissions, deploy secrets, etc to our sidecar app? Do we want to build & maintain that deployment tooling? In our case: we decided it was worth the latency hit to be able to share tooling.

                                                                              1. 8

                                                                                Our fearless leader is extensively using Rust (and Zig) in the programming language he’s developing, Roc.

                                                                                1. 4

                                                                                  Oh, that language looks very interesting. I think a “friendly” functional programming language that compiles to binaries would be a great addition.

                                                                                  If they haven’t seen it, this paper might be relevant to their work:

                                                                                  Perceus: Garbage Free Reference Counting with Reuse

                                                                                2. 4

                                                                                  Although I use neither, Haskell and Rust look like a good fit since they both focus on safety with support for FP and easier concurrency. If you use Rust, your main obstacle will be borrow checker. Data-driven design helps there. If needed, you can cheat by using refcounting in Rust on what you can’t borrow check. You still get benefits of both its compiler and any 3rd-party code that does borrow check.

                                                                                  So, Rust can be gradually learned and adopted as an accelerator for Haskell projects. If not accelerator, just a way to leverage the good things in its ecosystem (esp networking and data stores).

                                                                                  1. 17

                                                                                    Haskell, when written with care, can often be roughly as fast as rust. It’s a natively compiled language that uses llvm for optimization. With stream fusion and other high level optimizations, you can end up with tight, vectorized asm loops over primitive, unboxed types.

                                                                                    It’s likely more productive to add appropriate strictness hints, awkward structure, and ugly code to make the optimizer happy than to glue two languages together via an ffi, especially since the ffi is likely to act as an optimization barrier, suppressing inlining and making alias analysis hard.

                                                                                    So, while idiomatic rust is likely to be faster than idiomatic haskell, warty optimized haskell in hotspots likely to be more productive than gluing things together by an ffi.

                                                                              1. 4

                                                                                Let me chime in on this. I enjoyed your article as I always do. Minor comments first:

                                                                                re formal methods making it cheaper. I’d scratch this claim since it might give a wrong impression of the field. Maybe you’ve seen a ton of papers claiming this in your research. It could be popular these days. In most of mine (ranging four decades min.), they usually just said formal methods either reduced or (false claim here) totally eliminated defects in software. They focus on how the software will have stunning quality, maybe even perfection. If they mention cost, it’s all over the place: built barely anything with massive labor; cost a lot more to make something better; imply savings in long-term since it needed no maintenance. The lighterweight methods, like Cleanroom, sometimes said it’s cheaper due to (other claim) prevention being cheaper. They didn’t always, though.

                                                                                re common knowledge is wrong. I got bit by a lot of that. Thanks for digging into it, cutting through the nonsense, and helping us think straight!

                                                                                Now for the big stuff.

                                                                                re stuff we can agree on. That’s what I’m going to focus on. The examples you’re using all support your point that nobody can figure anything out. You’re not using examples we’ve discussed in the past that have more weight with high, practical value. I’ll also note that some of these are logical in nature: eliminating the root causes means we don’t need a study to prove their benefit except that they correctly eliminate the root causes. Unless I skimmed past it, it looks like you don’t bring up those at all. Maybe you found problems in them, too. Maybe just forgot. So, I’ll list them in case any of you find them relevant.

                                                                                Memory safety. Most studies a massive number of bugs are memory safety. Languages that block them by default and tools that catch most of them will, if they work (prevent/catch), block a massive number of bugs. Lesser claims: many exploits (a) also use those kinds of bugs and (b) more easily use them. That lets us extrapolate the first claim to reduction of exploits and/or their severity. An easy test would be to compare (minus web apps) both the number of memory-safety errors and code injections found in C/C++ apps vs Java, C#, and Rust. If Java or C#, in the safe parts rather than unsafe parts. I predict a serious drop since their root cause is logically impossible most of the time. I believe field evidence already supports this.

                                                                                Garbage collection (temporal safety, single-threaded). The industry largely switched to languages using GC, esp Java and .NET, from C/C++. That’s because temporal errors are more difficult to prevent, were harder to find at one point (maybe today), and might cost more to fix (action at a distance). These kinds of errors turn up even in high-quality codebases like OpenBSD. I predict a huge drop by garbage collection making them impossible or less-probable. If it’s not performance-prohibitive, a GC-by-default approach reduces development time, totally eliminates cost of fixing these, and reduces crashes they cause. What I don’t have proof of is that I used to see more app crashes before managed languages due to a combo of spatial and temporal memory errors. Might warrant a study.

                                                                                Concurrency (temporal safety, multi-threaded). Like what GC’s address, concurrency errors are more difficult to prevent and can be extremely hard to debug. One Lobster was even hired for a long period of time specifically to fix one. There’s both safe methods for concurrency (eg SCOOP, Rust) and tools that detect the errors (esp in Java). If the methods work, what we’d actually be studying is if not introducing concurrency errors led to less QA issues than introducing and fixing concurrency errors. No brainer. :)

                                                                                Static analysis. They push the button, the bugs appear, and they fix the ones that are real. Every good tool had this effect on real-world, OSS codebases. That proves using them will help you get rid of more bugs than not using them. If no false positives (eg RV-Match, Astree), your argument is basically done. If false positives (eg PVS-Check, Coverity), then one has to study if the cost to go through the false positives is worth it vs methods without them. I’d initially compare to no-false-positive methods. Then, maybe to methods that are alternatives to static analysis.

                                                                                Test generators. Path-based, combinatorial, fuzzing… many methods. Like static analysis, they each find errors. The argument one is good is easy. If many are available (esp free), then other empirical data says each will spot things others miss. That has a quality benefit without a study necessary if the administrative and hardware cost of using them is low enough.

                                                                                My persistent claim on Lobsters for code-level quality: use a combination of FOSS languages and tools with memory-safety, GC-by-default, safe concurrency, static analysis, and test generation. To take the claim down, you just need empirical evidence against one or more of the above since my claim just straight-forward builds on them. Alternatively, show that how they interact introduces new problems that are costlier to fix than what they fixed. That is a possibility.

                                                                                Drivers. Microsoft Windows used to blue screen all the time for all kinds of users. The reports were through the roof. It was mostly drivers. They built a formal methods tool to make drivers more reliable. Now, Windows rarely blue screens from driver failures. There you go.

                                                                                Design flaws. You’ve personally shown how TLA+ mockups catch in minutes problems that alternative methods either don’t catch or take roughly forever to. Any research like that makes an argument for using those tools to catch those kinds of problems. I’ll limit the claim to that. It becomes a tiny, tiny claim compared to silver bullets most are looking for. Yet, it already allows one to save time on UI’s, distributed systems, modeling legacy issues, etc.

                                                                                Functional and immutable over imperative and mutable. In a nutshell, what happens as we transition from one to another is that the number of potential interactions increase. Managing them is more complex. Piles of research across fields show that both complexity and interactions drive all kinds of problems. Interestingly, this is true for both human brains and machine analysis. You’ve also linked to a formal methods article where author illustrated that mathematically for verifying functional vs imperative software. Any technique reducing both complexity and potential interactions for developers reduces their labor so long as the technique itself is understandable. That gives us root cause analysis, cross-disciplinary evidence, and mathematical proofs that it will be easier in long-term to verify programs that are more functional and use less, mutable state.

                                                                                Things we’ll be stuck with, like Internet protocols. Certain systems are set up to be hard to change or never change. We’re stuck with them. OSS, industry, and government keeps deploying bandaids or extra layers to fix problems in such systems without fixing the root. When they do fix a root cause, it’s enormously expensive (see Y2K bug). I’d argue for getting them right up-front to reduce long-term costs. I’m not sure what empirical studies have gone into detail about these systems. I just think it’s the best thing to apply that kind of thinking to.

                                                                                I’d say those are the only things I’d mention in an article like yours. They’re things that are easy to argue for using visible, real-world results.

                                                                                1. 1

                                                                                  I get a 404?

                                                                                  1. 1

                                                                                    It was up earlier. Now a 404. The cached copy being a 404 raises some questions.

                                                                                    The Wayback link works, though.

                                                                                  1. 1

                                                                                    I upvoted this because the lessons still haven’t been learned for many. If you read on it, cosmic rays flipping single bits are pretty much the only thing that comes up in most evaluating this risk.

                                                                                    “The most aggressive policies (retiring a page immediately after justone error, or retiring whole rows and columns) are able to avoidup to 96% of all errors. “

                                                                                    Obviously, anything that avoids 96% of all errors without a serious penalty is a rare find. Let’s use or build on it!

                                                                                    I’ll chime in to add that approaches like NonStop still address issues like this well. They make the internal components like black boxes that should produce same output on a given input. They do voting. If a component defects, there’s automated fixes that can get it back in shape. They also have redundancy and snapshots. Such designs knock out lots of problems people would never see coming.

                                                                                    I still think we need more modern designs following route of older ones like NonStop to architecturally block many issues with tactics like in this paper boosting reliability of individual components. We might also get them cheap if we use RISC boards for the individual components. On top of that, there’s lots of diversity in ecosystems such as ARM where the boards might have different implementations, process nodes, etc. The differences might reduce odds two components fail at the same time.

                                                                                    1. 11

                                                                                      If I’m reading this right, it talks the protocol that OTP uses for distributed Erlang (which is one of the ways you can do FFI in Erlang: write a C / whatever program that appears as one or more processes to Erlang code) in Go and provides some nice Go interfaces that look like Erlang for the Go programmer to use? Within the Go part of the world, you can have mutable (and shared mutable) state that would violate the invariants of the Erlang abstract machine if exposed there, but it’s conveniently hidden in some Go actors and so the Erlang world only sees immutable objects.

                                                                                      It looks quite neat, but you give up a lot of safety by going from Erlang to Go. If I needed single-threaded performance that badly, I think I’d probably go all of the way to C++. There seem to be a bunch of dead attempts to do this in C++, this seems to be the only actively maintained one.

                                                                                      1. 7

                                                                                        Rustler lets you code the performance-sensitive parts in Rust. Stay in Erlang for its safety. Stay safe, fast, and integrated when you leave it.

                                                                                      1. 8

                                                                                        Wow it’s crazy that Chez Scheme is from 1984 and Racket is from 1995!

                                                                                        I can definitely see that maintaining a big language implementation is a huge thing to ask, especially for 5 CS professors who are doing many other things like teaching, reviewing papers, serving on committees, etc.

                                                                                        1. 7

                                                                                          Even better, Chez Scheme goes back to Z80 processors. Many folks said you must stick entirely with C on weak hardware. They schemed up something better. Their historical paper (pdf) was full of interesting stuff.

                                                                                        1. 10

                                                                                          In other words, given a specification to copy a list, our synthesis tool was able to produce a complete self-contained C program with a separate independent proof certificate, formally guaranteeing, without a shadow of a doubt, that it fully satisfies the specification, thereby removing any need to trust a fallible human developer.

                                                                                          “Beware of bugs in the above code; I have only proved it correct, not tried it.” - Donald Knuth

                                                                                          Someone please set me straight if I’m wrong, but it looks to me like that generated code has a recursive call in a non-tail position. Pass it a large linked list and its stack will overflow and it will crash, despite its certified correctness and its guarantee that there’s no need for it to ever be double-checked by a fallible human developer.

                                                                                          1. 20

                                                                                            The F* project has been producing C code as the output from a verification toolchain for a while and this includes use in EverCrypt, where the formal proofs include security proofs of the protocols being implemented. The examples from this post look simpler than the demos of F* from 5-10 years ago.

                                                                                            There are a few problems with any of the things in this space:

                                                                                            • C is a really bad target for anything like this. C compilers all have a subtly different interpretation of the C semantics and your verified code is only correct with respect to one concrete instantiation of these semantics. Our paper from a few years ago shows the space of C semantics. Even CompCERT, which is a formally verified C compiler, only guarantees correct lowering if your input C is free from undefined behaviour.
                                                                                            • Getting the properties that you prove correct is really hard. For example, an earlier version of some of the EverCrypt code was proven to be free of temporal safety errors. The theorem was that no object may be accessed after it is freed. The proofs succeeded trivially: nothing was ever freed. Changing this to specify lifetimes and guarantee that everything was deallocated in a timely fashion was a lot of work.
                                                                                            • To the best of my knowledge, none of the proof tools work on non-trivial examples of concurrent code. CppMem is probably the best of these and it can’t handle more than a few dozen lines of code. When you can formally verify something like this multi-producer, single-consumer queue I’ll be really excited. And if your name is Mark Batty then I might even believe you can do it.
                                                                                            • Anything that the surrounding code does is an axiom. Shared-everything languages are incredibly bad for partial proofs: a memory-safety bug or a concurrency bug anywhere in the rest of your program can invalidate one of the axioms that your proof code depends on.
                                                                                            • None of the tools are good enough for large programs. This means that you invariably have to mix verified and non-verified code in the same program. Most of the synthesis tools that I’ve seen generate interfaces that are really hard to use correctly. Part of this comes from targeting C. There are a load of properties that are trivial to enforce with C++ smart pointers or type-safe enums, that the C programmer has to just remember to get right. This feeds back into the compositional correctness problems: If your interfaces are hard to use, you’ll get bugs at the boundary of the proof code. In real-world uses I’ve seen, you get more of these than you fixed in the verified part.

                                                                                            TL;DR: Verification and program synthesis are super interesting but they’re nowhere near ready for prime time.

                                                                                            1. 3

                                                                                              Verification and program synthesis are super interesting but they’re nowhere near ready for prime time.

                                                                                              The NATS iFACTS traffic control system (released in 2011) has over half a million lines of verified “crash-proof” SPARK code.

                                                                                              1. 2

                                                                                                Is there any good info on how well it has stood up since then, how much work it was to produce and verify, etc?

                                                                                                1. 2

                                                                                                  I haven’t found any cost amounts from poking around online. The Eurofighter Typhoon also uses SPARK in some of its systems. Yes, verification is hard, but there are real systems out there which do it. I think people assume it’s some unreachable goal, but with piecemeal approaches like Ada/SPARK, I think it’s a lot closer than people realize and the future is very bright.

                                                                                                  I don’t think we’ll see a big bang of “Our thing is verified!” it’s going to slow roll out with “this tiny lib we’re using is verified” and “we have some components which are verified”, and “we use verification tools” moving forward. Something along the lines of “functional core, imperative shell” but “verified core, un-verified wrappers.”

                                                                                                2. 2

                                                                                                  I’ll add the Infer tool that Facebook acquired to that. It also uses separation logic for temporal analysis of C/C++ programs. It handles massive codebases. They apply it to Java, too.

                                                                                                  The difference is that these tools narrow the problem down, aim for high automation, make tradeoffs that facilitate real-world use, and have people doing non-glamorous work supporting that (eg standard library, build integration). Academics often don’t do all this given they’re just proving a concept, doing more ambitious things, or sometime just what they enjoy.

                                                                                              2. 6

                                                                                                “Beware of bugs in the above code; I have only proved it correct, not tried it.” - Donald Knuth

                                                                                                He wrote this before we had theorem provers. He proved it by hand, which is a lot more error prone.

                                                                                                Doesn’t mean I agree with you, just that I don’t think that quote is really as damning as people say.

                                                                                                1. 1

                                                                                                  That’s an interesting comment. I never took that quote to mean that he wasn’t confident in the correctness of his handcrafted proof. I always interpreted it as a warning that proofs of code can have non-obvious limitations: they can be completely correct and internally consistent, but if the person doing the proving didn’t think to include some aspect of the desired behavior in the specification, the code can still do unexpected things.

                                                                                                  The code sample in the article is a good example. “Uses a constant amount of stack space regardless of input size” and “terminates in a well-defined way if memory allocation fails” weren’t part of the specification, so the code can bomb out even though it can be proven to perform the correct sequence of steps to copy a linked list as described by its spec.

                                                                                                  Of course, I know a fraction of a fraction of a fraction as much about formal proofs of code as you do, so take this as the mad ramblings of a neophyte; it’s just what I took away from that quote when I first read it.

                                                                                              1. 19

                                                                                                Thanks for posting! The technical side of things is quite interesting, but the writing style of the author is rather pompous.

                                                                                                “What if there were a way to automatically generate C-code, complete with formal proofs of correctness, removing any need to trust fallible human developers?” .. and what about the fallible humans writing the specs?

                                                                                                Here’s a link directly to their paper (he also provides other references at the bottom):

                                                                                                1. 3

                                                                                                  I’ll add that there’s been many specification errors in verified programs. Mutation testing was finding issues in them, too. We’ll need mamy eyeballs on them. Checking specs/proofs in general math is a social process but mathematicians don’t like computer-focused math. So, in a way, we’re moving the problems from code nobody was reviewing or analyzing to an esoteric language fewer people will check.

                                                                                                  It’s still great work due to the ubiquity of C, good tools for seperation logic, removing attack surface in spec-to-code gap, and pushing synthesis forward. Might as well keep putting good stuff together to see what happens.

                                                                                                  Far as general problem, I’m a bigger fan of doing stuff like this with notations like ASM’s that wider audience could use and review. Or languages like ML or SPARK with C generated from them. If algorithmic, a side benefit is one can retarget static analyzers and automated provers to them to confirm some properties without really getting into formal logic.

                                                                                                  1. 2

                                                                                                    There are so many memory unsafety bugs. Most of these are caused by selecting memory-unsafe languages, and C is the worst offender by far.