# Lab Lunch talk by James McKinna

Provisionally entitled: 'provisionality'; cognitive dimensions of programming-as-proof-search

If programs are proofs, then writing a program to fulfil a given
specification corresponds to searching for a proof of the
corresponding proposition. Hard to do in general, we typically do this
in interactive dialogue with a machine.
In this talk, I'll try to sketch how insights from the HCI of
programming might shed light on the theory, as well as design and
implementation of environments for programming and proof.