All things are highly refined crap! ... including all computer programs. The (not-so-interesting) problem with what you lay out is that some computer programs (e.g. https://isabelle.in.tum.de/dist/library/HOL/HOL-ex/Sqrt.html) are proofs and vice versa. The interesting part is where the disjunction is nonempty. It would be cool to have a list of non-programmable proofs ... or non-provable programs.
The interesting part of what you lay out is that programs make the requirements on their language more in-your-face than in proofs. It would be cool to know how many programs survive language changes ... a bit like how (I imagine in my ignorance) category theory helps us talk about proofs that survive language changes. It's tempting to say "None. No computer programs survive language changes." But that's not entirely true. The exercise with the fast inverse square root hack, where GCC optimizes, in part, by choosing particular ASM routines but TCC does not, shows a language change where the extensional effect is similar but not the same (TCC compiled one takes longer to execute than the GCC compiled one). Typical use of "programming language" says they're the same because both TCC and GCC compile them just fine (and GCC with different -Ox flags as well). But, really, they're different languages because they have a different *product*. Encapsulation is an ideal, a myth. On 3/3/21 1:40 PM, Roger Critchlow wrote: > So all of FRIAM after my post went to the spam folder. > > It struck me that computer programs are ideal artefacts which have empirical > existence. That is, sort of like math in that they're all airy-fairy, but > then sort of like rocks, too. > > If I take a piece of gneiss and break it into pieces, I can send the pieces > to all my fellow geologists and we all can perform experiments on our > individual pieces and come to a Peircian conclusion about the nature of the > rock. I can do that with a computer program, too, but I just make copies and > send them to my fellow nerds, and we can all perform experiments on our > individual copies and come to a Peircian conclusion about the nature of the > program. > > So math proofs and scientific papers were an earlier form of this, but they > don't have an empirical existence, or none that's any help. We can come to a > Peircian conclusion about the weight and number of pages and density of type > in the manuscript, but we cannot make it run. You either understand or you > don't, and if you understand, you either agree or you don't. But the only > real existence of the proof or paper is the subjective experience of reading > the document, which quickly discourages almost everybody. > > That's a much different experience than gamers trading riffs to try out at > tricky points in a game, or climate modelers figuring out how to squeeze > another digit of signal out of the noise. There are still issues of > technical competence, but there is an object of study rather than a subject > of study, and when people share an object of study, they can independently > confirm and extend observations, which can be shared, and so on. Seems like > a kind of multiplier. > > And, of course, some computer programs are just highly refined crap, like > gmail's spam filter. -- ↙↙↙ uǝlƃ - .... . -..-. . -. -.. -..-. .. ... -..-. .... . .-. . FRIAM Applied Complexity Group listserv Zoom Fridays 9:30a-12p Mtn GMT-6 bit.ly/virtualfriam un/subscribe http://redfish.com/mailman/listinfo/friam_redfish.com FRIAM-COMIC http://friam-comic.blogspot.com/ archives: http://friam.471366.n2.nabble.com/
