The role of diagrams in geometric proofs has often been misunderstood, with many authors saying that diagrams should properly have no role in correct proofs. However, diagrams can be correctly used in geometric proofs as long as the rules that govern their use are understood. In this talk, I will discuss my work creating a sound diagrammatic formal system for giving proofs in Euclidean geometry, and the implications of this system for what we say about diagrams and proof in our GeT courses. I will also discuss the computer implementation of this formal system, CDEG (“Computerized Diagramattic Euclidean Geometry”), which is a Digital Proof Tool for giving fully diagrammatic proofs in Euclidean geometry. This talk should be of significant interest to any members of the GeT community who are interested in teaching about how to use diagrams correctly in proofs, who are interested in the use of Digital Proof Tools, and/or are interested in the axiomatic foundations of geometry.