I'm enjoying the #Pittsposium in #Cambridge , a workshop in honour of my PhD supervisor Andy Pitts. Loved this talk by Larry Paulson, who advocated for mathematicians to use proof assistants with liberal use of sorry / admitted for parts of proofs they are confident in to avoid burning time on small details, for example the many lines of code required when verifying one sentence proofs in a standard textbook. #ITP