866.634.6227

parentrelations@imacs.org

The child has one intuitive aim: self development

Logic Propels CMU Freshman to Research Opportunity

IMACS alumna Naomi Spargo in her freshman year at CMU

IMACS alumna Naomi Spargo sent the following email at the end of her first semester at Carnegie Mellon University. She details the ways in which her IMACS background in mathematical logic, proof-writing, and functional programming propelled her to research and teaching assistant opportunities in only her freshman year at computer science powerhouse CMU.

 

Dear IMACS,

I’m delighted to inform you that your IMACS courses have been even more helpful than I previously expected! During my first semester at CMU, I’ve become extremely interested in type theory and it’s applications to computer science.

Because of the background IMACS gave me in the lambda calculus and Scheme, I’ve been able to immerse myself in my chosen field much faster than most freshman.

Next semester, I’m employed as a teaching assistant for a class called Principles of Functional Programming. I took the course this semester and did quite well, so I applied! My interview consisted of a brief summary of my background (where I mentioned my experience with lambda calculus through IMACS), followed by a 20-minute mock-lecture where I “taught” my interviewers course material.

Although the material itself was not part of the IMACS curriculum (it was using structural induction to prove the correctness of recursive functions), IMACS is nonetheless the foundation of how I write my proofs. At this point, my interests are completely proof-based; literally everything I do rests on the formal style I learned from your logic courses.

This summer I will be employed as a research assistant by a professor studying formal verification of computer systems. Mid-way through the semester I realized that I didn’t like statistics, which caused me to rethink my interest in AI. After scouring the internet for alternative career plans, I scheduled a meeting with a professor studying formal verification, and, after giving me advice, she invited me to a couple presentations done by her graduate students and eventually offered me employment.

She hasn’t offered any cushioning to ease my entry into a completely new discipline. She sends me her own papers and those of her graduate students and expects me to keep up. The research she is exposing me to is (unsurprisingly) very formal; there is a steep learning curve in understanding the syntax, let alone the actual content.

My background in reading symbolic logic is proving exceedingly useful in this regard. I even sent her my IMACS transcripts before she committed to take me on.

She mentioned to me that she doesn’t like to work with people who aren’t trained in writing formal proofs, and would take a logician without programming background over a programmer without mathematical background every time (and this is in CS research!). She said that it’s easy to explain programming to logicians, as they have an abstract understanding of what “correctness” requires which translates easily into writing good code. However, it’s frustratingly difficult to explain logic to programmers who haven’t written proofs before.

In general, IMACS provides an enormous service by exposing students to areas of math that aren’t taught in high school.

When I was in high school, I didn’t have the foresight to know how important a logic background would be to my future. Now, it seems as though formal logic is the gateway between everyday programming and the conceptual innovation in computer science. If you can’t write a proof, you can’t get in.

When applying for these positions, I’m sure I stood out because I was already comfortable in the niche (relative to the imperative style, which every CS freshman is comfortable in) world of formal logic and functional programming. The research I will be involved in is very syntax-heavy; it would be exceedingly difficult for me to even understand the research, let alone advance it, if I didn’t have background in reading symbolic logic.

In addition to these new benefits, everything I said before about IMACS helping me write proofs efficiently has held true throughout the semester. I’m proud to inform you that I’ve ended with a 4.0 :)!

Wishing you a happy new year!

Sincerely,
Naomi Spargo

Comments are closed.