All of the above are direct consequences of the sheer scale of MMM's SMVS project, which is one of the things that set that project apart from most other ventures. MMM's SMVS project sits towards the "extreme" end of several dimensions simultaneously, which can make it very difficult for some people to comprehend -- "What is it you do again?" But that's OK - I barely understand it sometimes! :-) Other projects broadly similar to the SMVS do exist, it's just that they're so rare you have to go back in history to find them. Perhaps if we take a quick peek at one such project the SMVS won't look quite so scary!

The famous story of John Harrison's sea watches is an excellent example of a historical project that compares well with MMM's SMVS project. In the early 18th century, international trade (and, most importantly for the British, naval warfare) were totally dominated by sailing ships, but with no reliable method of determining the "longitude" component of a ship's position (how far east or west a ship is), shipwrecks were VERY common relative to today - in one incident an entire fleet went onto the rocks with the loss of 2,000 sailors! In 1714, determined that no more ships should be lost in this way, the British government offered a huge prize of £20,000 for anyone who could substantially solve the "longitude problem". John Harrison, a master clockmaker, famously spent over FORTY YEARS perfecting a series of sea watches accurate enough to allow longitude to be reliably calculated even after a transatlantic voyage (because if you know exactly what the time is at some fixed point on the globe, such as London, when the sun is directly overhead wherever you are then you can work out how far east or west you are from that fixed point). Largely as a result of Harrison's advances in time-keeping technology, the longitude problem was solved and shipping and the global trade that relied upon it were completely transformed.

A similarly critical problem exists today in that the entire developed world depends on computers and computers depend on software and SOFTWARE DOESN'T WORK PROPERLY, primarily because, despite over 60 years of effort by the world's IT experts, there is still no reliable (and at the same time economically practicable) means of getting all the bugs out of program code before it is released to customers - to all intents and purposes IT'S ALL FULL OF BUGS! This problem currently costs the world an incredible $1 billion or so every single day which, in terms of impact on global trade, makes it the modern equivalent of the 18th century's longitude problem. A genuine solution to the "software doesn't work properly" problem has proved similarly elusive (over 60 years of failure so far) and requires a technological push relative to the prevailing state-of-the-art of comparable magnitude.

So, this is the problem that MMM is trying to solve, and we're attempting to do so by carefully building a very large and complex computer program - the SMVS - that, when run, automatically constructs a fully formal mathematical proof that a given program-under-development (the "unit under test" or UUT) is 100% bug-free. (More accurately, the SMVS will attempt to construct such a proof - our job at MMM is to ensure that, when such a proof exists, the SMVS is able to find it in as high a proportion of real-world cases as possible, our goal being most real-world cases.) This "mathematical-proof-based debugging" technique, called formal program verification, has been around for a very long time and is EXTREMELY powerful in terms of its ability to detect software bugs.

Basically, any bugs present in a UUT will make it impossible for a valid formal proof of their absence to be found - you can't formally prove something that isn't true! Only if the UUT really is 100% bug-free will the SMVS be able (in most real-world cases) to construct a formal proof that this is the case, which in practical terms means that no bugs will ever get past the SMVS undetected. (In those cases where a program is genuinely bug-free but the SMVS can't find a proof 100% automatically then it will always be the case that the programmer will be able to provide additional information which allows a proof to be found.) In other words, the completed SMVS will offer a reliable (and at the same time economically practicable) means of getting ALL the bugs out of program code before it is released to customers, which is exactly what is required in order to fix the "software doesn't work properly" problem.

There's just the minor detail of course of actually designing and building the SMVS in the first place, which it turns out is not something that just anyone with a computer science degree and a library card can do - in reality this is a very difficult technical problem literally at the frontier of today's science. At the heart of the problem is exactly how to automate the SMVS in such a way and to such an extent that the formal program verification process (from the perspective of a "real-world" software developer) becomes economically attractive. Only if this has been achieved beyond any shadow of a doubt (i.e. in "slam dunk" fashion) will large numbers of software developers feel compelled to buy and use SMVS on large numbers of real-world projects, which is the whole point of the exercise!

There's a natural tension between doing the job properly and keeping the overall project a manageable size. On the one hand, the less ambitious we are in terms of the size of the market we're ultimately aiming for then the lower the degree of automation that is required, the easier the underlying technical problems are to solve and the sooner the SMVS will be completed and revenues will start to flow. On the other hand, unless and until SMVS-style formal program verification is used by a significant proportion of the world's programmers, the SMVS's genuine impact outside of the very small "safety-critical" sector will be minimal and the $1 billion per day "software doesn't work properly" problem will persist indefinitely. This for us is just not good enough, because we wish to make a genuine contribution, not simply loads of money (I neglected to mention that the financial rewards for whoever solves this problem will be essentially unlimited!) In order to get comfortably past the threshold where we start to make a real difference, we're aiming to support at least two million fee-paying end-users (or 20% of the world's 10 million professional programmers). This unfortunately translates into a much more difficult set of problems for us to solve, which greatly extends the pre-revenue part of the project, which then has to be funded somehow. In real-world practice (not like on TV!), high-tech project funding is often intermittent and unreliable at best, which means long periods of self-sacrifice for the founders, i.e. me, hence the totally bizarre nature of my life! :-)

Pitching the SMVS at such a large target market means that it needs to be practicably and economically usable by ordinary intelligent programmers not having "masters degrees in mathematical logic". For many decades this eminently noble idea was widely regarded within the computer science world as being so difficult as to be essentially (or even literally) impossible. We've now been iteratively planning, designing, building and testing the SMVS and its subsystems more-or-less continually since 1985 (for much of this time, many people thought we were crazy!) - but remember even this is way less than John Harrison spent designing his sea watches!

After seven years of basic research followed by nine years of design, we have now been physically implementing the SMVS since 2001, plus more recently the computer science community has finally (and rather whole-heartedly) accepted that what we're trying to do might actually be possible after all! After all this work, we are now getting tantalisingly close to having a non-trivial component of the SMVS (namely a highly-automated non-interactive theorem-prover for first-order logic with equality) actually working - woo hoo!

Nevertheless, for the time being at least, the going remains tough. The bottom line is it's just a matter of having the stamina to keep going even when things are personally very difficult - as they often have a tendency to be! As long as you don't give up (which is soooo easy to do!), you eventually work through whatever the problems are at the time and thus achieve one more step towards your goal, until of course the next problem arises and then the next and then the next, ad infinitum... It's much easier to keep going of course if you believe very strongly in what you're doing - strange as this may sound, it can't be solely about money and dreams of international-model-drenched Sunseekers anchored off Bora Bora!

So, believing in the SMVS project as we do, we just keep slogging away day after day, month after month, year after year (to the tune of Dory in Pixar's Finding Nemo - "Just keep swimming, just keep swimming!") and as long as we NEVER GIVE UP (or die in the process!) the target SMVS will one day become fully operational and the $1 billion per day "software doesn't work properly" problem will be solved (no more crashing or hanging up or other pesky idiosyncratic behaviour), and computers (which depend on this software) will also work properly and the developed world (which depends on these computers) will be a much better place for everyone, and, almost as a side-effect, MMM will be enormously stupendously ridiculously profitable (as it surely deserves to be), at which point Bora Bora here I come! Either that or it will all go disastrously Pete Tong along the way, which is where the dumpster option comes in! I guess we'll see... :-)