"The Best New Programming Language is a Proof Assistant" by Harry Goldstein [video]