Now, we are talking "truth" in all of its possible aspects; in computing, we deal with whether things are done as they ought (as in, expected to or specified so as to). The whole of tru'eng deals with these issues, some of which are not of practical interest, at the moment (but will be, in time). Besides, the issues of computability, we have things like goodness of systems (methods to predict (insure) such) or their soundiness.
A key issue is addressed by Leslie Lamport: Who Builds a House without Drawing Blueprints? (ACM, Comm, Vol. 48, No. 4). Leslie describes some of the motivations for his work, namely TLA - Temporal Logic of actions. It is not that doing systems is strictly like construction, after all, we do not see flow charts being used nowadays. However, nothing good comes about, except by extreme luck, from lack of planning. Agile methods (more below) seem to be like that; from where I sit, the users are expected to adapt with whatever the developers come up with, especially in the freebie systems that are so prevalent nowadays.But, trust your life on some of this software? Earlier, we pointed to some discussion of the bazaar / cathedral theme (yes, juxtaposed, for obvious reasons). Test/code/review does not allow one to lift (to be discussed).
Now, about TLA, in the same issue of the Communications of the ACM, Amazon allowed their workers to present some comments on its use.
---
Aside: I fell out of my chair; for many reasons, one of which is that I have not dealt (by purpose) with the company ever (except from 10 yards away). So, I'm impressed and will look more closely at this. ... In actuality, the company has done very well in handling technical problems (I just hope that the owner doesn't diddle with the Washington's Post editoral nature - too much) that are not simple. They, like others, are facing problems daily for which there is no known solution (except that we can do types of approximations, adequately enough, so as to be practical - stacking up what karma that will bite us later? - that is, many (of the hapless) get pulled into the troubles without their knowledge and against their wishes - to wit, the idiocy of 2008 til now for which we are still paying and have a ways to go yet - world-class moron-hood, Jamie, et al). Now, I need to look at AWS for another project.
---
TLA has some add-ons, one of which is mentioned in the Amazon article (actually, other companies are mentioned - including Oracle): PlusCal.
Oh yes, the article: How Amazon Web Services Uses Formal Methods. There were several authors. But, this quote needs attention: A precise, testable description of a system becomes a what-if tool for designs, analogous to how spreadsheets are a what-if tool for financial models.
Of course, there is this, too: Formal methods deal with models of systems, not the systems themselves, so the adage "All models are wrong, some are useful" applies. As in, using our terms: territory-map.
One author, Marc Brooker, has blogged about his experiences (post on TLA+). Notice that the domain is fairly particular. As one travels out the abstraction chain, things get further from the machine (even if everything has to still funnel through the execution stream) into realms of creativity.
Which, then, brings up one issue. The more formal (too, the real sciences bigots who bewail that humans are so unpredictable - wake up, folks) like to think that they can compress being (whatever it is and however we might know it) into a box (actually, enmeshing our glorious selves in a trap that is onerous to the extreme) and, thereby, get risk (and all related ilk) under its thumb (hah). In actuality, we can (not the cathedral, by necessity, but with a bazaar with some bit of decorum) find our ways through to a safe and healthful experience (virtual and otherwise).
Remarks: Modified: 05/14/2015
05/14/2015 -- If you cannot read the ACM articles, please send a note. I can pull out public links from the references which would be equivalent in concept and close in content.
05/14/2015 -- And so, after the post and content has been digested (does not imply absence of forethought), then epilog bits come to fore. The first half of that letter is what resonates. Then, Ben&Steve talking "incredible returns" in the stock market grates (harshly). For one, the thing, as run now, is a ca-pital-sino and very much can be characterized by near-zero (both terms have links in the text). Too, though, is the whole thing of the magical multiplier (wild expansion of value), of returns mainly for the early birds (connivers), and of enormous grabs (by some) that desires serious analysis (again, foreclosure - not in any way now profiting, nor in the past profited, from the gaming - whose main thing is to impoverish the masses). ... There will be a change in tone, thanks to Canfield (yes, he of the chicken soup thing). --- So, the diatribe series will stand as an example: so-called constructive looks, No. 1, No. 2, No. 3.
05/14/2015 -- And so, after the post and content has been digested (does not imply absence of forethought), then epilog bits come to fore. The first half of that letter is what resonates. Then, Ben&Steve talking "incredible returns" in the stock market grates (harshly). For one, the thing, as run now, is a ca-pital-sino and very much can be characterized by near-zero (both terms have links in the text). Too, though, is the whole thing of the magical multiplier (wild expansion of value), of returns mainly for the early birds (connivers), and of enormous grabs (by some) that desires serious analysis (again, foreclosure - not in any way now profiting, nor in the past profited, from the gaming - whose main thing is to impoverish the masses). ... There will be a change in tone, thanks to Canfield (yes, he of the chicken soup thing). --- So, the diatribe series will stand as an example: so-called constructive looks, No. 1, No. 2, No. 3.
No comments:
Post a Comment