Journal: Until April 1 - shaolintl/fstar-type-checker GitHub Wiki

Reflection

(potentially to be referenced in final essay, & for personal benefit)

Computer Science, despite its name, is usually taught and practiced as an engineering discipline. Unlike in Physics, few laymen acknowledge the mathematical rigor and beauty that motivated many of the necessary discoveries in Computer Science, both before the proliferation of personal computing machines and today.

Maybe my nationality has something to do with it, but discussing my field of study with friends and family almost certainly degrades into a volley of buzzwords along the lines of “hacking” this or “disrupting” that. I would argue this has less to do with their non-technical understanding and more to do with the pedagogy, and even pressure, that undergraduates in this field (and in others) face, which steers Computer Sciences graduates in turn.

I also have entrepreneurial ambitions, but it should be obvious that certain entrepreneurs churn unoriginal ideas, and others steer the world in the directions of their visions. The latter requires an understanding of the orchestration of the world’s events as well as managerial skills.

Tools empower, and the most powerful is the one with the understanding of the tools’ mechanics, for he is able to repair, reapply, and reinvent.

It is difficult to see the forest through the trees as a Computer Science student: topics usually float so far above the metal that transistors are more of a cognitively recognized fact and less of a reality. But it must be reiterated that abstraction to the Computer Scientist and abstraction to the mathematician are distinct. In a sense, mathematical abstraction is orthogonal to computational abstraction, since the former usually implies generality and intellectual and personal maturity, whereas the latter is descriptive of the physicist – user gradient.

My work with Tomer at INRIA will extend into both computational and mathematical abstraction – to a certain point where researchers envision more creative and capable software solutions in application of ideas that in truth need no utilitarian justification.

To close, I extend my gratitude to Tomer for encouraging this opportunity; I believe it is my resolution to hold understanding in the same regard as action that inspired his faith in my potential as a scientist.

k. 4/03/2017

Challenges

  • Traversing a thicket of jargon and notation
  • Impressively poor documentation on many advanced topics

Skills Practiced

  • Prolog
  • Lambda-Prolog
  • OCaml
  • Reviewed use of Git version control system
  • Learned advanced material and introductory material concurrently
  • See materials page for topics