> There are two meanings of prove. The one that type theorists are using is roughly "to derive your statement from axioms with pure logic." This sense of the te

> There are two meanings of prove. The one that type theorists are using is roughly "to derive your statement from axioms with pure logic." This sense of the term can never apply to things in the real world... I am not sure it's a meaningful distinction. There are no triangles in the "real" world -- if you look close under a microscope, there will be more than three sides -- but geometry proves to be of great practical value just the same.