The requirements for optimal software

This is a repost from my rant.li post. I figured out that rant.li was full of spam so I decided to move over to a less spammy website.

Table of Contents

  1. The requirements for optimal software.
  2. Other notes
  3. Works Cited

The requirements for optimal software.

I was reading the wikipedia article for programming and would like to give my own short description of a perfect program.

I am speaking only of programs made to be systems in and of themselves, if a program exists to extend a system (like GNU/Linux command line programs) then they need different properties. I do not know of any graphical user interfaces that allow one to combine graphical programs with significant power [2,3], so every GUI program that's meant to be used frequently must be viewed as a system in and of itself. Video games and programs only meant to be used once have different criteria and they will not be considered.

In addition to the technical criteria, the program should be free software (GNU Project, 2023).

I know a total of zero programs that have these properties. Depending on the task, the efficiency requirement is basically impossible.

Other notes

  1. As far as I know, coq has not been given a formal proof of its correctness. I am not sure if you could use coq to check a proof of its own correctness but I assume you cannot.
  2. A Smalltalk Virtual machine (such as Squeak) may allow for composing GUI programs with enough power. I am not familiar enough Smalltalk to be sure.
  3. Somebody else made a similar point in a video. He mentioned GNU Xnee as something that could let you write scripts for gui programs. He did not know about Xdotool. I think I saw the video on planet.gnu.org a year ago, It may have been made by Jose E. Marchesi, but I am not 100% sure on that. Scriptability and Composability are different things but his complaint about most GUI programs being unscriptable influenced me anyways.
  4. If your operating system can do this for you, then the program does not have to do it itself. (Proven, Liam, 2023) mentions that LISP machines the ability to save their state before powering down. A more modern system, PhantomOS perserves the state of userlevel programs across reboot (Zavalishin, Dmitry, 2020). The EROS based operating systems (EROS, CAPROS, Coyotos) are also said to have this property (Chakraborty, Pinaki, 2010). I am not as sure about the EROS operating systems.
  5. The Wikipedia article lists this as “maintainability” but “program maintenance” isn't a real thing. Programs don't wear down and do not need to be “maintained” in the same way you would maintain a car ((Edsger W. Dijkstra, 1988) talks about this in more detail). What we call “program maintenance” is two unrelated tasks: Fixing program errors, and adapting the program to a new system. The former isn't necessary if you formally prove the correctness of a program, the latter is necessary if your system updates, or your libraries change.
  6. One thing I worry about with extensibility, is that giving the user unlimited ability to change its behavior code can cause the program to lose its correctness. The user must be allowed to do this anyways so, The program should be able to handle having incorrect user components without crashing or extreme loss of functionality.
  7. A good literate programming environment should support hypertext, citation management, and mathematical equations (in the prose and in source code comments). The hypertext system should let you import source code and functions from other files through hyperlinks. This would support writing programs as a series of index cards in a slip box (for more information on why I want this, read: (Ahrens, Sonke, 2022)). I would also want to have many different ways of importing the source code, some hygienic, and others unhygienic (In the sense of hygienic macros). I will describe my ideal literate programming environment in another blog post.
  8. If you use Hoare Logic, you must prove that the program terminates separately. Standard Hoare Logic does not prove the program terminates.
  9. All though it is out of style today, non fiction works used to be written in verse. Indian mathematical sutras were partially written in verse, some (or all?) essays by Alexander Pope were also in verse.

I do not like the text editor in rant.li, I wrote this in emacs org mode, exported it as markdown, and copy pasted it.

I skipped the portability section of the Wikipedia article because I don't find it very important.

Works Cited

Ahrens, Sonke (2022). How to take smart notes: One simple technique to boost writing, learning and thinking, Sonke Ahrens.

Chakraborty, Pinaki (2010). RESEARCH PURPOSE OPERATING SYSTEMS-A WIDE SURVEY., Computer Science & Telecommunications.

Datskovskiy, Stanislav (2012). Engelbart's Violin. (http://www.loper-os.org/?p=4012)

Edsger W. Dijkstra (1988). On the cruelty of really teaching computing science.

GNU Project (2023). What is Free Software?. (https://www.gnu.org/philosophy/free-sw.html)

Hoare, C. A. R. (1969). An Axiomatic Basis for Computer Programming, Association for Computing Machinery.

Klein, Gerwin and Elphinstone, Kevin and Heiser, Gernot and Andronick, June and Cock, David and Derrin, Philip and Elkaduwe, Dhammika and Engelhardt, Kai and Kolanski, Rafal and Norrish, Michael and others (2009). seL4: Formal verification of an OS kernel.

Knuth, Donald Ervin (1984). Literate programming, Oxford University Press.

Proven, Liam (2023). War of the workstations: How the lowest bidders shaped today's tech landscape, The Register. (https://www.theregister.com/2023/12/25/the_war_of_the_workstations/)

Yegge, Steve (2007). The Pinocchio Problem. (https://steve-yegge.blogspot.com/2007/01/pinocchio-problem.html)

Zavalishin, Dmitry (2020). Phantom OS Orthogonal Persistence-based OS Intro and Design Concepts. (https://video.fosdem.org/2020/K.4.601/uk_phantom.webm)

By Logan Andersen. This work is licensed under CC BY-ND 4.0

You can see my other blogs here.