آموزش طراحی با قراردادهای اثبات‌پذیر - آخرین آپدیت

ستون اصلی DBC — قراردادهای فراخوان و فراخوانده The DBC Pillar — Caller/Callee Contracts

• 1.1.1 سه‌گانه هوار و چرایی اهمیت آن 1.1.1 Hoare's Triples and Why

• 1.1.2 ایفلِ مایر: Require، Ensure و Invariant 1.1.2 Meyer's Eiffel: Require, Ensure, Invariant

• 1.1.3 اصل جایگزینی لیسکوف 1.1.3 Liskov Substitution Principle

• 1.2.1 پورت به Rust: Prusti، Creusot، Requires و Ensures 1.2.1 Rust Port: Prusti, Creusot, Requires, Ensures

ستون سیستم تایپ — قراردادها از طریق بررسی‌کننده تایپ The Type-System Pillar — Contracts via the Type-Checker

• ویدیو 2.1.1: تجزیه کن، اعتبارسنجی نکن Video 2.1.1: Parse, Don't Validate

• 2.1.2: استفاده از Newtype به عنوان قرارداد بدون هزینه Video 2.1.2: Newtype as Zero-Cost Contract

• 2.1.3: PhantomData و تگ‌های زمان کامپایل Video 2.1.3: PhantomData and Compile-Time Tags

• 2.2.1: Typestate — ماشین‌های حالت در تایپ‌ها Video 2.2.1: Typestate — State Machines in Types

پل YAML — مقالات، ریاضیات و قراردادها در کد The YAML Bridge — Papers, Math, Contracts in Code

• 3.1.1: چرا مشخصات YAML به عنوان کد؟ Video 3.1.1: Why YAML Specification as Code

• 3.1.2: طبقه‌بندی تعهدات — ۱۹ ویژگی + ۷ مورد ایفل Video 3.1.2: Obligation Taxonomy — 19 Property + 7 Eiffel

• 3.1.3: ابطال پوپرایی — شکست‌های قابل اقدام Video 3.1.3: Popperian Falsification — Actionable Failure

• 3.2.1: ویژگی هفتم ایفل (pv) Video 3.2.1: pv Property 7-Eiffel

• 3.2.2: از مقاله تا YAML — یک معادله Video 3.2.2: From Paper to YAML — One Equation

صعود از نردبان اثبات‌پذیری — از سطح L1 تا L5 Climbing the Provability Ladder — L1 to L5

• 4.1.1: سطح L1 + L2 — ابزارهای Lint و تایپ‌ها روی softmax Video 4.1.1: L1 + L2 — Lint and Types on softmax

• 4.1.2: سطح L3 — تست proptest برای مجموع یک در softmax Video 4.1.2: L3 — proptest softmax sums to one

• 4.1.3: سطح L4 — استفاده از Kani برای بررسی غیرمنفی بودن softmax Video 4.1.3: L4 — Kani softmax non-negativity

• 4.2.1: هزینه در مقابل اطمینان — کدام پله مناسب است؟ Video 4.2.1: Cost vs Confidence — Which Rung Fits

پروژه پایانی — بررسی تابع softmax در هر ۵ سطح Capstone — softmax Across All Five Levels

• 5.1.1: سطح L5 — Lean 4 برای مهندسان Video 5.1.1: L5 — Lean 4 for Engineers

• 5.1.2: از مقاله تا قضیه — ایجاد استاب (Stub) در Lean Video 5.1.2: From Paper to Theorem — Lean Stub

• 5.1.3: قضیه softmax در زبان Lean Video 5.1.3: softmax Theorem in Lean

• 5.2.1: دمو — چرا اثبات‌پذیری اهمیت دارد Video 5.2.1: Demo — Why Provability Matters