Talk:Proof: Difference between revisions

 

: Putting something that looks like "2" in the CPU register, the same "2" in another, performing ADD, and getting something that looks like "4" doesn't help - that is not a proof! :) You need to ''define'' numbers, rules for arithmetic, induction, etc ''in'' the language based on a suitable [http://ncatlab.org/nlab/show/type+theory metatheory] such as [[wp:Intuitionistic_type_theory|MLTT]] or [[wp:Calculus_of_constructions|CoC]]/[[wp:Calculus_of_inductive_constructions|CoIC]], then prove. E.g., in the Agda version <code>even+even≡even</code> takes ''any'' two even numbers and returns their sum as an even number, this is a ''type'', i.e. logical ''proposition'', ''algorithm'' itself is a ''proof'' by induction which ''builds'' a required term of a given (inhabited) type, and the typechecker ''performs'' that proof (so that this is compile-time verification). &mdash; [[User:Ht|Ht]] 02:44, 12 May 2012 (UTC)