Good morning, schmeagy deags. I bring tell of great tidings. I have finally started birthing an Orchid. To formalize the previous statement, my mind has begun the painful, several-year-long process of giving birth to Orchid. What is Orchid? Certainly not a human child. I don’t have the biological hardware for that. Will it be as good as a human child? I suppose that will be for the world to decide.
You’ll notice I never answered the first question. To put it in the most boring way humanly possible, Orchid will be a piece of mathematical software. Bleh. To put it in a far more intriguing way, Orchid will be a tool that allows human beings to mercilessly take advantage of the parts of computer that are better than humans to construct magnificent pieces of logical structure with extreme simplicity.
If you’re at all involved in STEM, you probably have some level of familiarity with Mathematica, Maple, or Matlab. For the uninitiated, these are all programs that have been developed over the course of several decades and are essentially superpowered calculators. I do not mean for Orchid to attempt to overthrow these three giants of this particular industry. That would be ultimate folly for several reasons:
Goodness, that was only two reason. Last I checked, “two” doesn’t fall within the set of numbers described by “several.” Well I think they are both good enough. Those of you familiar with the Big Three mathematical programs know the staggering breadth of mathematical material that they support. What then could I possibly wish to accomplish with Orchid? What will Orchid be able to do that these pieces of software cannot?
I will answer by giving you the story that motivated Orchid in the first place. Last semester, I wanted a break from my regular schoolwork, so I bopped on over to the law library and violently threw open Steven Weinberg’s Foundations of Quantum Field Theory. That book is, in a word, dense. With my other courses last semester, I took me about four months to get through the first (real) chapter of the book. I was finally at the point where I could start working through the problems at the end of the chapter. To many of you readers not actively involved in physics, you may be wondering why on Earth I was purposely subjecting myself to the third level of hell. To many of you readers actively involved in physics, you may be wondering why on Earth I was purposely subjecting myself to the third level of hell. To those of you readers who actually enjoy theoretical physics, you will know exactly why I was purposely subjecting myself to the third level of hell, and understand I was doing this for the same reason a drug addict will go to any lengths to get another sweet, sweet hit of whatever particular substance has been giving them problems.
Because I was in Weinberg’s book, the problems were hard. Like really, really hard. However, I wasn’t annoyed by the length of the problems, I was annoyed at how I was doing the problem. I was naturally doing everything with pencil and paper, and I found that I was constantly rewriting extremely long equations with an incredible number of moving parts. I think everyone except the true weirdos can agree that the act of constantly rewriting extremely long equations is incredibly tedious, but it is also extremely prone to errors. Eventually, blessed readers, I had had enough. You better believe I wanted to find the Lie Algebra of the Galilean group, but at a certain point, a girl has got to put her foot down. I, being the metaphorical girl, fled the Law Library feeling particularly defeated.
As a budding computer scientist, however, I had another reason to be frustrated. Literally one of the biggest purposes of computers is to do simple monotonous tasks that probably could be done by humans. Why couldn’t I just use a computer to find the Lie Algebra of the Galilean group for me?
With this question glistening upon my tongue, I started a deep dive into the documentation of all the major pieces of math software with which I’m familiar. These pieces of software are incredibly good and fast at doing standard computations in a wide variety of fields in mathematics. Their issue is that they don’t allow you to define your own logical structures with their own rules. The particular piece of mathematics that I needed to do cannot easily be done using the Big Three.
I then began researching the incredibly huge variety of other pieces of mathematical software. The closest thing I found to a software that could solve my problems are two programs called Coq and Lean. Let me tell you, the language and interface for both of these pieces of software are absolutely disgusting. Coq in particular has that “90s software” feel that makes everyone want to amputate one of their feet.
From the beginning of this venture, I felt I would likely need to develop my own piece of software to accomplish my needs, and as I continued to research, the requirements and features of what I now call Orchid came to me as though from a half-remembered dream. In essence, I have two main requirements for Orchid:
As a final note, some of you overly masculine readers may ask why I am choosing to call the system Orchid. I could give you some hooplala about Orchids being beautiful yet unique, or them having cool adaptations that mirror logical structures. That ain’t true. I wanted to name it something cool that in my mind evokes a similar emotion in my being as when I think about the Euler-Lagrange equation. “Orchid” therefore, fit the bill remarkably well.