In 1969, the same year that Apollo 9 safely returned to Earth after its manned mission to the moon, in the field of computer science, the first "Request for Comment" note, RFC 1, was published (Wikipedia Writers and Editors, 2018). While the structured science of computers was arguably in its infancy, the British logician Tony Hoare developed a way to use logic to check for correctness of a computer program that very year (Wikipedia Writers and Editors, January 2019). This remarkable achievement, I think, however, was overshadowed my his even greater achievements in the field, such as the development of quicksort in 1960.
Last year, I've taught myself logic to see if I just liked the subject at all, and I pretty much did! Deciding to push myself into the field of both mathematics and computer science, I've observed the everyday environment around me for any application of logic in any form. And I've come to an entertaining thought in the bathroom, while I was thinking in the still water of the bathtub:
Premise 1: \(A\to B\)
Premise 2: \(A\)
I could interpret this as there being a computer program called \(A\to B\) that, if I put \(A\) into it, it rewrites it into \(B\), and passes over to the rest of the control flow (program) if the input wasn't \(A\). While it might be deficient to call this a "function" of any kind, I do want to take the frequent "black-box" metaphor and call that a machine. Then, it is a rewriting machine, a one-direction substitution machine, and it's an if-then statement.
Someone might think further and think of relating all the logical things onto the programming world (which would be interesting). Conversely, they could implant those "while" and "do-while" kinds of statements onto logic. I do not think it is mere coincidence (or that we should leave it as coincidence) that a natural-deduction proof and a computer program may often look similar in form.
I'm thinking that, to do something like a while loop, I'd need to keep track of the truth values of those statements that I'm having. But specifics aside, I hope I might be able to come up with certain generalization about those statements, and use it for my own gain if I delved into the programming profession.
Taking this idea further, I might, in the future, study Hoare Logic, if me and some group of people are willing to invest in the subject, create problems and maintain wiki pages, for this potentially applicable and exciting idea: Hoare Logic, proposed first by the British logician Tony Hoare in 1969, was "a formal system with a set of logical rules for reasoning rigorously about the correctness of computer programs" (Wikipedia Writers and Editors, February 2019). The Wikipedia entry is extensive, but I believe certain many people here on Brilliant would be definitely interested in integrating symbolic logic into computer science in one of the most necessary steps of practical problem-solving: Checking your work (code). The humanly effort of reorganizing our knowledge of said Logic would till the fertile soil of an idea which had stood at the spotlight for nearly half a century, and some youths would benefit from it when they realize that there is a connection between logic and programming, and perhaps, they might be the same thing.
Yet, before further study, I want to refrain from talking about the topic because I don't want to be a crackpot.
Good night, -YuJin
Wikipedia Writers and Editors, "Hoare logic." Wikipedia. 12 Feb 2019. Web. Retrieved 18 Feb 2019.
Wikipedia Writers and Editors, "1969 in science." Wikipedia. 4 Dec 2018. Web. Retrieved 18 Feb 2019.
Wikipedia Writers and Editors, "Tony Hoare." Wikipedia. 28 Jan 2019. Web. Retrieved 18 Feb 2019.