On May 28, 7:28 pm, rjf <[EMAIL PROTECTED]> wrote: > I think my Tivo DVR runs Linux, and in principle I have access > to the source, but I would no more consider trying to fix a bug in it than I > would remove my own appendix.
This is more a problem of commercialization and being a closed system. There are DVRs/recievers that are Linux based, open for installing new software and have their own community of people who develop their own code. So, this is in the wild, just not by TiVo! The conclusion for me - about that and the current topic - is, that you not only need a public source code, but also the community, the ability and tools to develop, (in that case also an open hardware), howtos, and yes, basically encuragement for those who want to write software on their DVR and so on. i.e. I know that there are RSS readers for DVRs with LAN... that's geeky, but cool ;) About proofs: I think, the current state of understanding software and hardware is just not mature enough to do this. As mentioned above, this is a chain of respoinsibilites. It can't be a serious requirement to proof basic cpu commands for doing abstract algebra - maybe every time again for each command and each software package. This needs layers and a new understanding what's going on. My (prbably naiive understanding) is, that there are much more problems mentioned than in reality. e.g. if you proof a statement X in pure mathematics, you don't have to make sure that it is printed correctly in every place in the universe - it just has to be correct in some virtual space of imagination! (think of typos, ink problems, ...) The same holds true, i think, for hardware flaws. Someone just has to trust into the hardware to write correct algorithms. Also, the software itself is layered: system libraries, kernel, management tools, APIs, ... It is impossible to have to proof them just for using them. Therefore, only the actual implementation using that whole stack should be checked... At that point, maybe some time in the future, some abstract mapping of code lines to logic with inferencing for correctness and back to code will exist? To transform code into something canonical to analyze? I don't know. Also, I heared that the language Fortress want's to be close to typed math (2d formula rendering in source code ...). Maybe that's a first step towards closeing that gap between pure math and software implementations? H --~--~---------~--~----~------------~-------~--~----~ To post to this group, send email to [email protected] To unsubscribe from this group, send email to [EMAIL PROTECTED] For more options, visit this group at http://groups.google.com/group/sage-devel URLs: http://www.sagemath.org -~----------~----~----~----~------~----~------~--~---
