Curry-Howard Correspondence
কারি-হাওয়ার্ড করেসপন্ডেন্স
'Propositions as types, proofs as programs' — একটা type একটা logical proposition, আর সেই type-এর একটা term সেই proposition-এর একটা প্রমাণ।
also: Curry-Howard Isomorphism, Propositions as Types
Function type A → B মানে logical implication A ⟹ B; product
type A × B মানে conjunction A ∧ B; sum type A + B মানে
disjunction A ∨ B। একটা প্রোগ্রাম টাইপ-চেক করা মানেই সেই
প্রোগ্রামের টাইপ যে proposition বোঝায় তার একটা বৈধ প্রমাণ পাওয়া।
Simply-typed lambda calculus-এ প্রতিটা well-typed term টার্মিনেট
করে (strong normalization) — তাই non-terminating Ω-এর মতো term
ব্যাকরণগতভাবেই বাতিল হয়ে যায়। এই কারণেই dependently-typed ভাষা
(Coq, Agda, Lean) সরাসরি এই correspondence-এর উপর দাঁড়িয়ে প্রমাণ
লেখায় — compiler নিজেই proof-checker, আর CompCert/seL4-এর মতো
formally-verified সফটওয়্যার এভাবেই তৈরি।