Understanding Understanding: How Do We Reason About Computational Logic?

Abstract

Computers fundamentally do not reason like humans do, making it time-consuming and expensive for programmers to find and fix mistakes in, or maintain, hardware and software. Given that such maintenance activities can often comprise up to 90% of the total cost associated with hardware and software, interest in better preparing future programmers for the computational logic reasoning required for computer science industry and academia has grown. We argue that understanding how programmers reason about computational logic can guide tool development and training activities for more efficient logical reasoning. In this thesis, we use non-intrusive, objective measures to present three research components investigating cognition for computational logic reasoning tasks, with a focus on digital logic, mathematical logic, and programming logic. We further illuminate, and advocate the investigation of, promising cognitive interventions to help programmers reason about computers.

First, we present a first-of-its-kind automated algorithm to repair defects in hardware designs (i.e., digital logic) and a human study investigating its use as a debugging assistant for programmers. We also produce a publicly-available benchmark suite of defects for the evaluation of future automated repair techniques for hardware. We find that our approach, CirFix, is able to successfully repair 16 out of 32 defects, representing a repair rate similar to that of established software repair techniques. In our human study involving 41 participants, we further find a preference among programmers for CirFix as a debugging aid for defects spanning multiple lines, primarily in classroom contexts. Our study paves the path for exploration of automated repair of hardware designs to reduce maintenance costs in industry and help programmers in the classroom.

Second, we present a human study involving 34 participants tasked with finding mistakes in formal algorithmic proofs (i.e., mathematical logic). We use eye-tracking to investigate the effects of various problem-solving strategies on formalism comprehension task outcomes. Analyzing participant responses, we find that incoming preparation and programmer self-perceptions are not accurate predictors of task outcomes, and that differences in outcomes can be attributed to inductive and recursive logical reasoning. Analyzing eye-tracking data, we find that more-prepared programmers employ different visual strategies but achieve similar outcomes to those of less-prepared programmers, and that programmers with more successful outcomes frequently go back and forth between presented material. Our results advocate for pedagogical interventions in undergraduate computer science theory courses to better prepare future programmers for formal reasoning in industry and academia.

Third, we present a human study probing causality between spatial reasoning and program comprehension (i.e., programming logic) using transcranial magnetic stimulation (TMS), a non-invasive neurostimulation technique. Analyzing responses collected from 16 participants, we replicate a prior psychology study showing that TMS impacts spatial reasoning. More importantly, and contrary to previously-established correlations, we find no evidence of a simple causal relationship between activity in the primary motor cortex or the supplementary motor area and programming outcomes. Further, we find that TMS can affect response time for programming tasks. Ours is the first study to use TMS in a computer science context, and our results advocate for further exploration of the technique to investigate neural activity for programming.

This thesis shows that it is possible to use objective measures to obtain mathematical models describing programmer behavior and cognition for computational logic reasoning tasks, and these models can highlight prospective cognitive interventions for student training.