Greg Wilson asked "How Reliable is Scientific Software?" https://neverworkintheory.org/2021/09/25/how-reliable-is-scientific-software.html
which is a really interesting read. For example" [Hatton1994], is now a quarter of a century old, but its conclusions are still fresh. The authors fed the same data into nine commercial geophysical software packages and compared the results; they found that, "numerical disagreement grows at around the rate of 1% in average absolute difference per 4000 fines of implemented code, and, even worse, the nature of the disagreement is nonrandom" (i.e., the authors of different packages make similar mistakes). On 9/26/21, Tim Daly <axiom...@gmail.com> wrote: > I should note that the lastest board I've just unboxed > (a PYNQ-Z2) is a Zynq Z-7020 chip from Xilinx (AMD). > > What makes it interesting is that it contains 2 hard > core processors and an FPGA, connected by 9 paths > for communication. The processors can be run > independently so there is the possibility of a parallel > version of some Axiom algorithms (assuming I had > the time, which I don't). > > Previously either the hard (physical) processor was > separate from the FPGA with minimal communication > or the soft core processor had to be created in the FPGA > and was much slower. > > Now the two have been combined in a single chip. > That means that my effort to run a proof checker on > the FPGA and the algorithm on the CPU just got to > the point where coordination is much easier. > > Now all I have to do is figure out how to program this > beast. > > There is no such thing as a simple job. > > Tim > > > On 9/26/21, Tim Daly <axiom...@gmail.com> wrote: >> I'm familiar with most of the traditional approaches >> like Theorema. The bibliography contains most of the >> more interesting sources. [0] >> >> There is a difference between traditional approaches to >> connecting computer algebra and proofs and my approach. >> >> Proving an algorithm, like the GCD, in Axiom is hard. >> There are many GCDs (e.g. NNI vs POLY) and there >> are theorems and proofs passed at runtime in the >> arguments of the newly constructed domains. This >> involves a lot of dependent type theory and issues of >> compile time / runtime argument evaluation. The issues >> that arise are difficult and still being debated in the type >> theory community. >> >> I am putting the definitions, theorems, and proofs (DTP) >> directly into the category/domain hierarchy. Each category >> will have the DTP specific to it. That way a commutative >> domain will inherit a commutative theorem and a >> non-commutative domain will not. >> >> Each domain will have additional DTPs associated with >> the domain (e.g. NNI vs Integer) as well as any DTPs >> it inherits from the category hierarchy. Functions in the >> domain will have associated DTPs. >> >> A function to be proven will then inherit all of the relevant >> DTPs. The proof will be attached to the function and >> both will be sent to the hardware (proof-carrying code). >> >> The proof checker, running on a field programmable >> gate array (FPGA), will be checked at runtime in >> parallel with the algorithm running on the CPU >> (aka "trust down to the metal"). (Note that Intel >> and AMD have built CPU/FPGA combined chips, >> currently only available in the cloud.) >> >> >> >> I am (slowly) making progress on the research. >> >> I have the hardware and nearly have the proof >> checker from LEAN running on my FPGA. >> >> I'm in the process of spreading the DTPs from >> LEAN across the category/domain hierarchy. >> >> The current Axiom build extracts all of the functions >> but does not yet have the DTPs. >> >> I have to restructure the system, including the compiler >> and interpreter to parse and inherit the DTPs. I >> have some of that code but only some of the code >> has been pushed to the repository (volume 15) but >> that is rather trivial, out of date, and incomplete. >> >> I'm clearly not smart enough to prove the Risch >> algorithm and its associated machinery but the needed >> definitions and theorems will be available to someone >> who wants to try. >> >> [0] https://github.com/daly/PDFS/blob/master/bookvolbib.pdf >> >> >> On 8/19/21, Tim Daly <axiom...@gmail.com> wrote: >>> ========================================= >>> >>> REVIEW (Axiom on WSL2 Windows) >>> >>> >>> So the steps to run Axiom from a Windows desktop >>> >>> 1 Windows) install XMing on Windows for X11 server >>> >>> http://www.straightrunning.com/XmingNotes/ >>> >>> 2 WSL2) Install Axiom in WSL2 >>> >>> sudo apt install axiom >>> >>> 3 WSL2) modify /usr/bin/axiom to fix the bug: >>> (someone changed the axiom startup script. >>> It won't work on WSL2. I don't know who or >>> how to get it fixed). >>> >>> sudo emacs /usr/bin/axiom >>> >>> (split the line into 3 and add quote marks) >>> >>> export SPADDEFAULT=/usr/local/axiom/mnt/linux >>> export AXIOM=/usr/lib/axiom-20170501 >>> export "PATH=/usr/lib/axiom-20170501/bin:$PATH" >>> >>> 4 WSL2) create a .axiom.input file to include startup cmds: >>> >>> emacs .axiom.input >>> >>> )cd "/mnt/c/yourpath" >>> )sys pwd >>> >>> 5 WSL2) create a "myaxiom" command that sets the >>> DISPLAY variable and starts axiom >>> >>> emacs myaxiom >>> >>> #! /bin/bash >>> export DISPLAY=:0.0 >>> axiom >>> >>> 6 WSL2) put it in the /usr/bin directory >>> >>> chmod +x myaxiom >>> sudo cp myaxiom /usr/bin/myaxiom >>> >>> 7 WINDOWS) start the X11 server >>> >>> (XMing XLaunch Icon on your desktop) >>> >>> 8 WINDOWS) run myaxiom from PowerShell >>> (this should start axiom with graphics available) >>> >>> wsl myaxiom >>> >>> 8 WINDOWS) make a PowerShell desktop >>> >>> https://superuser.com/questions/886951/run-powershell-script-when-you-open-powershell >>> >>> Tim >>> >>> On 8/13/21, Tim Daly <axiom...@gmail.com> wrote: >>>> A great deal of thought is directed toward making the SANE version >>>> of Axiom as flexible as possible, decoupling mechanism from theory. >>>> >>>> An interesting publication by Brian Cantwell Smith [0], "Reflection >>>> and Semantics in LISP" seems to contain interesting ideas related >>>> to our goal. Of particular interest is the ability to reason about and >>>> perform self-referential manipulations. In a dependently-typed >>>> system it seems interesting to be able "adapt" code to handle >>>> run-time computed arguments to dependent functions. The abstract: >>>> >>>> "We show how a computational system can be constructed to "reason", >>>> effectively >>>> and consequentially, about its own inferential processes. The >>>> analysis proceeds in two >>>> parts. First, we consider the general question of computational >>>> semantics, rejecting >>>> traditional approaches, and arguing that the declarative and >>>> procedural aspects of >>>> computational symbols (what they stand for, and what behaviour they >>>> engender) should be >>>> analysed independently, in order that they may be coherently >>>> related. Second, we >>>> investigate self-referential behavior in computational processes, >>>> and show how to embed an >>>> effective procedural model of a computational calculus within that >>>> calculus (a model not >>>> unlike a meta-circular interpreter, but connected to the >>>> fundamental operations of the >>>> machine in such a way as to provide, at any point in a computation, >>>> fully articulated >>>> descriptions of the state of that computation, for inspection and >>>> possible modification). In >>>> terms of the theories that result from these investigations, we >>>> present a general architecture >>>> for procedurally reflective processes, able to shift smoothly >>>> between dealing with a given >>>> subject domain, and dealing with their own reasoning processes over >>>> that domain. >>>> >>>> An instance of the general solution is worked out in the context of >>>> an applicative >>>> language. Specifically, we present three successive dialects of >>>> LISP: 1-LISP, a distillation of >>>> current practice, for comparison purposes; 2-LISP, a dialect >>>> constructed in terms of our >>>> rationalised semantics, in which the concept of evaluation is >>>> rejected in favour of >>>> independent notions of simplification and reference, and in which >>>> the respective categories >>>> of notation, structure, semantics, and behaviour are strictly >>>> aligned; and 3-LISP, an >>>> extension of 2-LISP endowed with reflective powers." >>>> >>>> Axiom SANE builds dependent types on the fly. The ability to access >>>> both the refection >>>> of the tower of algebra and the reflection of the tower of proofs at >>>> the time of construction >>>> makes the construction of a new domain or specific algorithm easier >>>> and more general. >>>> >>>> This is of particular interest because one of the efforts is to build >>>> "all the way down to the >>>> metal". If each layer is constructed on top of previous proven layers >>>> and the new layer >>>> can "reach below" to lower layers then the tower of layers can be >>>> built without duplication. >>>> >>>> Tim >>>> >>>> [0], Smith, Brian Cantwell "Reflection and Semantics in LISP" >>>> POPL '84: Proceedings of the 11th ACM SIGACT-SIGPLAN >>>> ymposium on Principles of programming languagesJanuary 1 >>>> 984 Pages 23–35https://doi.org/10.1145/800017.800513 >>>> >>>> On 6/29/21, Tim Daly <axiom...@gmail.com> wrote: >>>>> Having spent time playing with hardware it is perfectly clear that >>>>> future computational mathematics efforts need to adapt to using >>>>> parallel processing. >>>>> >>>>> I've spent a fair bit of time thinking about structuring Axiom to >>>>> be parallel. Most past efforts have tried to focus on making a >>>>> particular algorithm parallel, such as a matrix multiply. >>>>> >>>>> But I think that it might be more effective to make each domain >>>>> run in parallel. A computation crosses multiple domains so a >>>>> particular computation could involve multiple parallel copies. >>>>> >>>>> For example, computing the Cylindrical Algebraic Decomposition >>>>> could recursively decompose the plane. Indeed, any tree-recursive >>>>> algorithm could be run in parallel "in the large" by creating new >>>>> running copies of the domain for each sub-problem. >>>>> >>>>> So the question becomes, how does one manage this? >>>>> >>>>> A similar problem occurs in robotics where one could have multiple >>>>> wheels, arms, propellers, etc. that need to act independently but >>>>> in coordination. >>>>> >>>>> The robot solution uses ROS2. The three ideas are ROSCORE, >>>>> TOPICS with publish/subscribe, and SERVICES with request/response. >>>>> These are communication paths defined between processes. >>>>> >>>>> ROS2 has a "roscore" which is basically a phonebook of "topics". >>>>> Any process can create or look up the current active topics. eq: >>>>> >>>>> rosnode list >>>>> >>>>> TOPICS: >>>>> >>>>> Any process can PUBLISH a topic (which is basically a typed data >>>>> structure), e.g the topic /hw with the String data "Hello World". eg: >>>>> >>>>> rostopic pub /hw std_msgs/String "Hello, World" >>>>> >>>>> Any process can SUBSCRIBE to a topic, such as /hw, and get a >>>>> copy of the data. eg: >>>>> >>>>> rostopic echo /hw ==> "Hello, World" >>>>> >>>>> Publishers talk, subscribers listen. >>>>> >>>>> >>>>> SERVICES: >>>>> >>>>> Any process can make a REQUEST of a SERVICE and get a RESPONSE. >>>>> This is basically a remote function call. >>>>> >>>>> >>>>> >>>>> Axiom in parallel? >>>>> >>>>> So domains could run, each in its own process. It could provide >>>>> services, one for each function. Any other process could request >>>>> a computation and get the result as a response. Domains could >>>>> request services from other domains, either waiting for responses >>>>> or continuing while the response is being computed. >>>>> >>>>> The output could be sent anywhere, to a terminal, to a browser, >>>>> to a network, or to another process using the publish/subscribe >>>>> protocol, potentially all at the same time since there can be many >>>>> subscribers to a topic. >>>>> >>>>> Available domains could be dynamically added by announcing >>>>> themselves as new "topics" and could be dynamically looked-up >>>>> at runtime. >>>>> >>>>> This structure allows function-level / domain-level parallelism. >>>>> It is very effective in the robot world and I think it might be a >>>>> good structuring mechanism to allow computational mathematics >>>>> to take advantage of multiple processors in a disciplined fashion. >>>>> >>>>> Axiom has a thousand domains and each could run on its own core. >>>>> >>>>> In addition. notice that each domain is independent of the others. >>>>> So if we want to use BLAS Fortran code, it could just be another >>>>> service node. In fact, any "foreign function" could transparently >>>>> cooperate in a distributed Axiom. >>>>> >>>>> Another key feature is that proofs can be "by node". >>>>> >>>>> Tim >>>>> >>>>> >>>>> >>>>> >>>>> On 6/5/21, Tim Daly <axiom...@gmail.com> wrote: >>>>>> Axiom is based on first-class dependent types. Deciding when >>>>>> two types are equivalent may involve computation. See >>>>>> Christiansen, David Thrane "Checking Dependent Types with >>>>>> Normalization by Evaluation" (2019) >>>>>> >>>>>> This puts an interesting constraint on building types. The >>>>>> constructed types has to export a function to decide if a >>>>>> given type is "equivalent" to itself. >>>>>> >>>>>> The notion of "equivalence" might involve category ideas >>>>>> of natural transformation and univalence. Sigh. >>>>>> >>>>>> That's an interesting design point. >>>>>> >>>>>> Tim >>>>>> >>>>>> >>>>>> On 5/5/21, Tim Daly <axiom...@gmail.com> wrote: >>>>>>> It is interesting that programmer's eyes and expectations adapt >>>>>>> to the tools they use. For instance, I use emacs and expect to >>>>>>> work directly in files and multiple buffers. When I try to use one >>>>>>> of the many IDE tools I find they tend to "get in the way". I >>>>>>> already >>>>>>> know or can quickly find whatever they try to tell me. If you use an >>>>>>> IDE you probably find emacs "too sparse" for programming. >>>>>>> >>>>>>> Recently I've been working in a sparse programming environment. >>>>>>> I'm exploring the question of running a proof checker in an FPGA. >>>>>>> The FPGA development tools are painful at best and not intuitive >>>>>>> since you SEEM to be programming but you're actually describing >>>>>>> hardware gates, connections, and timing. This is an environment >>>>>>> where everything happens all-at-once and all-the-time (like the >>>>>>> circuits in your computer). It is the "assembly language of >>>>>>> circuits". >>>>>>> Naturally, my eyes have adapted to this rather raw level. >>>>>>> >>>>>>> That said, I'm normally doing literate programming all the time. >>>>>>> My typical file is a document which is a mixture of latex and lisp. >>>>>>> It is something of a shock to return to that world. It is clear why >>>>>>> people who program in Python find lisp to be a "sea of parens". >>>>>>> Yet as a lisp programmer, I don't even see the parens, just code. >>>>>>> >>>>>>> It takes a few minutes in a literate document to adapt vision to >>>>>>> see the latex / lisp combination as natural. The latex markup, >>>>>>> like the lisp parens, eventually just disappears. What remains >>>>>>> is just lisp and natural language text. >>>>>>> >>>>>>> This seems painful at first but eyes quickly adapt. The upside >>>>>>> is that there is always a "finished" document that describes the >>>>>>> state of the code. The overhead of writing a paragraph to >>>>>>> describe a new function or change a paragraph to describe the >>>>>>> changed function is very small. >>>>>>> >>>>>>> Using a Makefile I latex the document to generate a current PDF >>>>>>> and then I extract, load, and execute the code. This loop catches >>>>>>> errors in both the latex and the source code. Keeping an open file >>>>>>> in >>>>>>> my pdf viewer shows all of the changes in the document after every >>>>>>> run of make. That way I can edit the book as easily as the code. >>>>>>> >>>>>>> Ultimately I find that writing the book while writing the code is >>>>>>> more productive. I don't have to remember why I wrote something >>>>>>> since the explanation is already there. >>>>>>> >>>>>>> We all have our own way of programming and our own tools. >>>>>>> But I find literate programming to be a real advance over IDE >>>>>>> style programming and "raw code" programming. >>>>>>> >>>>>>> Tim >>>>>>> >>>>>>> >>>>>>> On 2/27/21, Tim Daly <axiom...@gmail.com> wrote: >>>>>>>> The systems I use have the interesting property of >>>>>>>> "Living within the compiler". >>>>>>>> >>>>>>>> Lisp, Forth, Emacs, and other systems that present themselves >>>>>>>> through the Read-Eval-Print-Loop (REPL) allow the >>>>>>>> ability to deeply interact with the system, shaping it to your >>>>>>>> need. >>>>>>>> >>>>>>>> My current thread of study is software architecture. See >>>>>>>> https://www.youtube.com/watch?v=W2hagw1VhhI&feature=youtu.be >>>>>>>> and https://www.georgefairbanks.com/videos/ >>>>>>>> >>>>>>>> My current thinking on SANE involves the ability to >>>>>>>> dynamically define categories, representations, and functions >>>>>>>> along with "composition functions" that permits choosing a >>>>>>>> combination at the time of use. >>>>>>>> >>>>>>>> You might want a domain for handling polynomials. There are >>>>>>>> a lot of choices, depending on your use case. You might want >>>>>>>> different representations. For example, you might want dense, >>>>>>>> sparse, recursive, or "machine compatible fixnums" (e.g. to >>>>>>>> interface with C code). If these don't exist it ought to be >>>>>>>> possible >>>>>>>> to create them. Such "lego-like" building blocks require careful >>>>>>>> thought about creating "fully factored" objects. >>>>>>>> >>>>>>>> Given that goal, the traditional barrier of "compiler" vs >>>>>>>> "interpreter" >>>>>>>> does not seem useful. It is better to "live within the compiler" >>>>>>>> which >>>>>>>> gives the ability to define new things "on the fly". >>>>>>>> >>>>>>>> Of course, the SANE compiler is going to want an associated >>>>>>>> proof of the functions you create along with the other parts >>>>>>>> such as its category hierarchy and representation properties. >>>>>>>> >>>>>>>> There is no such thing as a simple job. :-) >>>>>>>> >>>>>>>> Tim >>>>>>>> >>>>>>>> >>>>>>>> On 2/18/21, Tim Daly <axiom...@gmail.com> wrote: >>>>>>>>> The Axiom SANE compiler / interpreter has a few design points. >>>>>>>>> >>>>>>>>> 1) It needs to mix interpreted and compiled code in the same >>>>>>>>> function. >>>>>>>>> SANE allows dynamic construction of code as well as dynamic type >>>>>>>>> construction at runtime. Both of these can occur in a runtime >>>>>>>>> object. >>>>>>>>> So there is potentially a mixture of interpreted and compiled >>>>>>>>> code. >>>>>>>>> >>>>>>>>> 2) It needs to perform type resolution at compile time without >>>>>>>>> overhead >>>>>>>>> where possible. Since this is not always possible there needs to >>>>>>>>> be >>>>>>>>> a "prefix thunk" that will perform the resolution. Trivially, for >>>>>>>>> example, >>>>>>>>> if we have a + function we need to type-resolve the arguments. >>>>>>>>> >>>>>>>>> However, if we can prove at compile time that the types are both >>>>>>>>> bounded-NNI and the result is bounded-NNI (i.e. fixnum in lisp) >>>>>>>>> then we can inline a call to + at runtime. If not, we might have >>>>>>>>> + applied to NNI and POLY(FLOAT), which requires a thunk to >>>>>>>>> resolve types. The thunk could even "specialize and compile" >>>>>>>>> the code before executing it. >>>>>>>>> >>>>>>>>> It turns out that the Forth implementation of >>>>>>>>> "threaded-interpreted" >>>>>>>>> languages model provides an efficient and effective way to do >>>>>>>>> this.[0] >>>>>>>>> Type resolution can be "inserted" in intermediate thunks. >>>>>>>>> The model also supports dynamic overloading and tail recursion. >>>>>>>>> >>>>>>>>> Combining high-level CLOS code with low-level threading gives an >>>>>>>>> easy to understand and robust design. >>>>>>>>> >>>>>>>>> Tim >>>>>>>>> >>>>>>>>> [0] Loeliger, R.G. "Threaded Interpretive Languages" (1981) >>>>>>>>> ISBN 0-07-038360-X >>>>>>>>> >>>>>>>>> >>>>>>>>> >>>>>>>>> >>>>>>>>> On 2/5/21, Tim Daly <axiom...@gmail.com> wrote: >>>>>>>>>> I've worked hard to make Axiom depend on almost no other >>>>>>>>>> tools so that it would not get caught by "code rot" of libraries. >>>>>>>>>> >>>>>>>>>> However, I'm also trying to make the new SANE version much >>>>>>>>>> easier to understand and debug.To that end I've been >>>>>>>>>> experimenting >>>>>>>>>> with some ideas. >>>>>>>>>> >>>>>>>>>> It should be possible to view source code, of course. But the >>>>>>>>>> source >>>>>>>>>> code is not the only, nor possibly the best, representation of >>>>>>>>>> the >>>>>>>>>> ideas. >>>>>>>>>> In particular, source code gets compiled into data structures. In >>>>>>>>>> Axiom >>>>>>>>>> these data structures really are a graph of related structures. >>>>>>>>>> >>>>>>>>>> For example, looking at the gcd function from NNI, there is the >>>>>>>>>> representation of the gcd function itself. But there is also a >>>>>>>>>> structure >>>>>>>>>> that is the REP (and, in the new system, is separate from the >>>>>>>>>> domain). >>>>>>>>>> >>>>>>>>>> Further, there are associated specification and proof structures. >>>>>>>>>> Even >>>>>>>>>> further, the domain inherits the category structures, and from >>>>>>>>>> those >>>>>>>>>> it >>>>>>>>>> inherits logical axioms and definitions through the proof >>>>>>>>>> structure. >>>>>>>>>> >>>>>>>>>> Clearly the gcd function is a node in a much larger graph >>>>>>>>>> structure. >>>>>>>>>> >>>>>>>>>> When trying to decide why code won't compile it would be useful >>>>>>>>>> to >>>>>>>>>> be able to see and walk these structures. I've thought about >>>>>>>>>> using >>>>>>>>>> the >>>>>>>>>> browser but browsers are too weak. Either everything has to be >>>>>>>>>> "in >>>>>>>>>> a >>>>>>>>>> single tab to show the graph" or "the nodes of the graph are in >>>>>>>>>> different >>>>>>>>>> tabs". Plus, constructing dynamic graphs that change as the >>>>>>>>>> software >>>>>>>>>> changes (e.g. by loading a new spad file or creating a new >>>>>>>>>> function) >>>>>>>>>> represents the huge problem of keeping the browser "in sync with >>>>>>>>>> the >>>>>>>>>> Axiom workspace". So something more dynamic and embedded is >>>>>>>>>> needed. >>>>>>>>>> >>>>>>>>>> Axiom source gets compiled into CLOS data structures. Each of >>>>>>>>>> these >>>>>>>>>> new SANE structures has an associated surface representation, so >>>>>>>>>> they >>>>>>>>>> can be presented in user-friendly form. >>>>>>>>>> >>>>>>>>>> Also, since Axiom is literate software, it should be possible to >>>>>>>>>> look >>>>>>>>>> at >>>>>>>>>> the code in its literate form with the surrounding explanation. >>>>>>>>>> >>>>>>>>>> Essentially we'd like to have the ability to "deep dive" into the >>>>>>>>>> Axiom >>>>>>>>>> workspace, not only for debugging, but also for understanding >>>>>>>>>> what >>>>>>>>>> functions are used, where they come from, what they inherit, and >>>>>>>>>> how they are used in a computation. >>>>>>>>>> >>>>>>>>>> To that end I'm looking at using McClim, a lisp windowing system. >>>>>>>>>> Since the McClim windows would be part of the lisp image, they >>>>>>>>>> have >>>>>>>>>> access to display (and modify) the Axiom workspace at all times. >>>>>>>>>> >>>>>>>>>> The only hesitation is that McClim uses quicklisp and drags in a >>>>>>>>>> lot >>>>>>>>>> of other subsystems. It's all lisp, of course. >>>>>>>>>> >>>>>>>>>> These ideas aren't new. They were available on Symbolics >>>>>>>>>> machines, >>>>>>>>>> a truly productive platform and one I sorely miss. >>>>>>>>>> >>>>>>>>>> Tim >>>>>>>>>> >>>>>>>>>> >>>>>>>>>> >>>>>>>>>> On 1/19/21, Tim Daly <axiom...@gmail.com> wrote: >>>>>>>>>>> Also of interest is the talk >>>>>>>>>>> "The Unreasonable Effectiveness of Dynamic Typing for Practical >>>>>>>>>>> Programs" >>>>>>>>>>> https://vimeo.com/74354480 >>>>>>>>>>> which questions whether static typing really has any benefit. >>>>>>>>>>> >>>>>>>>>>> Tim >>>>>>>>>>> >>>>>>>>>>> >>>>>>>>>>> On 1/19/21, Tim Daly <axiom...@gmail.com> wrote: >>>>>>>>>>>> Peter Naur wrote an article of interest: >>>>>>>>>>>> http://pages.cs.wisc.edu/~remzi/Naur.pdf >>>>>>>>>>>> >>>>>>>>>>>> In particular, it mirrors my notion that Axiom needs >>>>>>>>>>>> to embrace literate programming so that the "theory >>>>>>>>>>>> of the problem" is presented as well as the "theory >>>>>>>>>>>> of the solution". I quote the introduction: >>>>>>>>>>>> >>>>>>>>>>>> >>>>>>>>>>>> >>>>>>>>>>>> This article is, to my mind, the most accurate account >>>>>>>>>>>> of what goes on in designing and coding a program. >>>>>>>>>>>> I refer to it regularly when discussing how much >>>>>>>>>>>> documentation to create, how to pass along tacit >>>>>>>>>>>> knowledge, and the value of the XP's metaphor-setting >>>>>>>>>>>> exercise. It also provides a way to examine a methodolgy's >>>>>>>>>>>> economic structure. >>>>>>>>>>>> >>>>>>>>>>>> In the article, which follows, note that the quality of the >>>>>>>>>>>> designing programmer's work is related to the quality of >>>>>>>>>>>> the match between his theory of the problem and his theory >>>>>>>>>>>> of the solution. Note that the quality of a later programmer's >>>>>>>>>>>> work is related to the match between his theories and the >>>>>>>>>>>> previous programmer's theories. >>>>>>>>>>>> >>>>>>>>>>>> Using Naur's ideas, the designer's job is not to pass along >>>>>>>>>>>> "the design" but to pass along "the theories" driving the >>>>>>>>>>>> design. >>>>>>>>>>>> The latter goal is more useful and more appropriate. It also >>>>>>>>>>>> highlights that knowledge of the theory is tacit in the owning, >>>>>>>>>>>> and >>>>>>>>>>>> so passing along the thoery requires passing along both >>>>>>>>>>>> explicit >>>>>>>>>>>> and tacit knowledge. >>>>>>>>>>>> >>>>>>>>>>>> Tim >>>>>>>>>>>> >>>>>>>>>>> >>>>>>>>>> >>>>>>>>> >>>>>>>> >>>>>>> >>>>>> >>>>> >>>> >>> >> >