Трішки вільний, бо стиль автора дуже стислий, переклад статті (https://supaiku.com/what-does-a-lean-proof-prove) від spike.

Альтернативна назва: епістеміка довіри до Lean з точки зору практикуючого програміста.

Коротко:

  • Исторія Lean є несуперечливою відносно ZFC
  • Основна реалізація, схоже, опосередковано відповідає теорії.
  • Реалізація переважно вільна від помилок судячи із практики.
  • Помилки, які наразі були виявлені, не були фатальними і виправлені.
  • Окрім головноії реалізації існує невелика, але зростаюча сім’я незалежних реалізацій, які підкріплюють модель довіри до Lean та доведень, написаних у ньому.
  • Можливо, не варто довіряти твердженням про програмне забезпечення, написане на Lean.

Термінологія Lean

все стане технічним, але це нормально, ось довідник.

  • Тип: це фундаментальний будівельний блок усіх об’єктів у Lean. думайте про Nat, Bool, List тощо.

  • Терм: це мешканець типу. думайте про число 4, яке є мешканцем Nat.

  • Твердження (proposition): це спеціальний тип, що живе у всесвіті Prop Lean1, мешканцями якого є доведення, а не дані. наприклад, 2 + 2 = 4 є твердженням. Доведення цього є термом цього типу. True і False самі по собі є твердженнями - True має тривіальне доведення, тоді як False не має мешканців взагалі.

  • Мета (goal): це твердження, яке ви намагаєтесь довести, разом з гіпотезами, які у вас є.

для твердження “якщо я маю доведення A і B, тоді я маю доведення B,” це кодується як:

A B : Prop
h : A ∧ B
⊢ B

Українською, кожен рядок каже:

A і B є твердженнями

  • наша гіпотеза h є доведенням A ∧ B

  • нам потрібно побудувати доведення B

  • Доведення: це терм, що населяє твердження (точно так само, як 4 населяє Nat).

для наведеного вище прикладу щодо A і B:

theorem and_right' (A B : Prop) (h : A ∧ B) : B :=
 h.right -- .right деконструює 'h' в його правий елемент, у цьому випадку B, що ми й хочемо показати/довести.
  • Тактика: це процедура, що трансформує мету. Маючи мету, тактика або завершує доведення, або створює простіші підмети.

Наприклад, тактика rewrite бере доведене твердження і намагається зіставити його з поточним станом мети. скажімо, ми маємо твердження, що у нас є два натуральних числа n і m, і ми хочемо показати, що n + m = m + n. це буде закодовано в Lean як:

example (n m : Nat) : n + m = m + n := by

Скажімо, ми також довели, що додавання натуральних чисел є комутативним (що називається Nat.add_comm), яке виглядає так. Тоді ми можемо застосувати тактику rewrite до нашого твердження:

example (n m : Nat) : n + m = m + n := by
 rw [Nat.add_comm]

що трансформує стан мети з

n m : Nat
⊢ n + m = m + n

до

n m : Nat
⊢ m + n = m + n -- тривіально істинно!
  • Коректність (soundness): формальна система є коректною, якщо кожне доводиме твердження є істинним у передбаченій інтерпретації.

Тобто синтаксис (що можна вивести) відповідає семантиці (що насправді істинно). у випадку Lean це означало б, що якщо у вас є терм t : P, тоді P дійсно виконується в математичній моделі.

  • Несуперечливість (consistency): формальна система є несуперечливою, якщо вона не може довести False.

Еквівалентно, вона не може довести і твердження, і його заперечення одночасно (в системах з принципом вибуху ці визначення збігаються). для повноти зазначу, що несуперечливість є строго слабшою за коректність — несуперечлива система може доводити хибні речі, поки вона не доводить сам False. див. цю дискусію

  • Теорія типів: це набір тверджень щодо типів (та пов’язаного теоретичного апарату), як їх використовувати, (опціонально) властивостей цієї системи в цілому.

у випадку Lean це модифікована версія теорії типів Мартіна-Льофа (MLTT) або інстітуціоналістьска теорія типів.

  • Ядро Lean (також називається перевірювач типів): це програмне забезпечення, яке реалізує цю теорію типів, завдання якого — перевірити, що для даного типу і терму, який повинен населяти цей тип, терм дійсно створює щось цього типу.

у випадку Lean це навмисно зроблено дуже маленьким. незважаючи на це, на момент написання існує кілька незалежних реалізацій різними мовами / різними людьми, і це має наслідки для епістеміки довіри до ядра Lean, про що буде сказано в наступному розділі.

примітка щодо взаємодії тактик з ядром: тактики взагалі не з’являються в артефактах, які ядро повинно перевіряти. оскільки тактики навмисно розроблені для створення лише термів доведення, вони самі можуть бути “елабороровані”2. як результат, людям дозволено використовувати химерні тактики на кшталт hammer, все ще довіряючи, що це не ускладнює роботу ядра.

Чому нас хвилює коректність?

коректність означає, що кожне доводиме твердження є істинним у передбаченій інтерпретації — символи означають те, що ви думаєте.

чому це важливо?

  • якщо система є некоректною, ви можете доводити твердження, які не виконуються в моделі, що вас цікавить. ваші доведення проходять перевірку типів, але вони не є “істинними” в будь-якому значущому сенсі. система тихо вам бреше.

  • несуперечливість (не доводити False) є слабшою. несуперечлива, але некоректна система не вибухне, але вона також не розповість вам нічого надійного про математику.

Чому нас хвилює несуперечливість?

  • теорія типів Lean приймає принцип вибуху: з протиріччя випливає будь-що. якщо ви можете довести False, ви можете довести що завгодно, роблячи систему непридатною.

  • несуперечливість гарантує, що цього не станеться. це мінімальна вимога для того, щоб логічна система мала хоч якусь цінність.

коректність дає вам значення. несуперечливість дає вам нетривіальність. ми хочемо обидва.3

Чи варто довіряти Lean?

коротка відповідь: так, мабуть

довга відповідь: це потрібно робити в двох частинах

  • що Lean (теоретичний об’єкт) описує коректну/несуперечливу формальну систему

  • що Lean (програмне забезпечення) точно реалізує цю теорію

Епістеміка Lean (теорія)

  • теорія типів Lean формально специфікована (це не завжди було так. нам пощастило!)

  • ця формально специфікована теорія була доведена несуперечливою відносно ZFC4

тобто, припускаючи, що ZFC є несуперечливою (як роблять всі практикуючі математики), Lean є несуперечливою. це формальний шантаж: ви не можете турбуватися про несуперечливість Lean, не турбуючись також про ZFC.

примітка: це найкраще, на що можна сподіватися. Lean підпадає під другу теорему Геделя про неповноту: системи, здатні описувати арифметику натуральних чисел, не можуть довести власну несуперечливість. тому доведення несуперечливості мають бути відносними.

  • коректність Lean (сильніша властивість) залишається недоведеною.

пригадайте: несуперечливість каже “ви не можете довести False.” коректність каже “кожне доводиме твердження є істинним у передбаченій моделі” — символи означають те, що ви думаєте.

дисертація Карнейро накидає доведення коректності відносно моделі ZFC, але воно неповне (кілька розділів позначені “НЕЗАКІНЧЕНО”). lean4lean працює над механізацією цього, але на момент написання лише частини перевірювача типів були верифіковані і всюди є sorries.

на практиці цей розрив невеликий — якби базові типи на кшталт Nat і = не означали те, що ми думаємо, ми б, ймовірно, це вже помітили. але філософський розрив між “мабуть нормально” і “доведено” залишається.

Епістеміка Lean (програмне забезпечення)

  • Lean 4 (той, що всі використовують) написаний на C++ і не доведено, що він відповідає теорії типів Lean.

ще більш тривожно, теорія типів Lean формально не існувала протягом більшої частини історії Lean. специфікація з’явилася лише близько 2019 року (дисертація Маріо Карнейро).

  • як результат, модель довіри для Lean нагадує ландшафт компіляторів: якщо дві незалежні реалізації дають різні результати, принаймні одна помиляється. але ситуація Lean складніша, оскільки нам потрібна довіра на двох рівнях:

    • реалізація: чи правильно ядро реалізує теорію типів? (кілька реалізацій тут допомагають)

    • теорія: чи сама теорія типів є коректною? (це вимагає зовнішнього доведення, і за Геделем, не може бути зроблено в самому Lean)

  • lean4lean існує: реімплементація ядра Lean 4 на самому Lean 4 (самоописана як “точной копией” реалізації на C++). це дозволяє перехресну перевірку, хоча з очевидною циклічністю — ви довіряєте Lean 4 перевіряти Lean 4.

Примітка: доведення несуперечливості з дисертації Карнейро було доведенням на папері про теорію типів Lean 3, а не механізованим доведенням у lean4lean. Механізовані доведення знаходяться в процесі на момент написання.

  • в процесі перекладу ядра Lean з C++ на Lean4, кілька помилок дійсно було знайдено. На щастя, всі вони піддавались виправленню. але враховуючи, що lean4lean навмисно був максимально близьким до оригінальної реалізації, залишається можливість існування інших помилок.

Крім того, ці помилки виникали лише в крайніх випадках і не анулювали ретроактивно жодних існуючих доведень у mathlib / основних модулях Lean.

  • Дуже мало існує інших незалежних реалізацій: є nanoda_lib (від автора “Type Checking in Lean 4”. Хоча на момент написання вона не досягає повноти щодо всього mathlib), trepplein (лише Lean 3), та кілька інших у процесі розробки.

Я сам працюю над lean4idris, який покриває близько 95% основних модулів Lean, але все ще далекий від стану, коли він мав би якісь наслідки для цієї дискусії.

Наскільки я маю довіряти доведенням, написаним у Lean?

Для більшості цілей, для домену, якому Lean присвячує більшість своєї роботи, тобто математиці, він наближається до золотого стандарту довіри. Навіть більше, ніж математичне доведення на папері, зрозуміло, якщо прийняти, що ядро Lean є надійним.

Хоча Lean доведено що він несуперечливий, але не доведено що він коректний, залишається можливість, що наші доведення проходять перевірку типів ідеально, але не означають те, що ми думаємо. Система не вибухне - вона просто тихо нам брехатиме.

Є додаткове занепокоєння, яке є звичайними моделями довіри, пов’язаними з аудитом коду. Я сам не повністю пройшов через доведення відносної несуперечливості Lean щодо ZFC; проте я довіряю, що цей результат, ймовірно, істинний з тієї ж причини, з якої практикуючі професіонали в будь-якій технічній галузі довіряють більшості речей у своїй галузі - інші розумні люди так сказали.

Тож безумовно є соціологічний кут, із якого можна дивитися, коли йдеться про довіру до ядра Lean не лише на глобальному рівні (знання всіх доведень, читання всіх статей, мати об’єднання всіх експертів Lean в одному мозку), але також на індивідуальному та організаційному рівні.

Що Lean має сказати про програмне забезпечення?

Коротка відповідь: не так багато, як ви б сподівались.

Маркетинг Lean все більше підкреслює верифікацію програмного забезпечення, і є реальні історії успіху (AWS Cedar, деяка робота з блокчейном), але є значні прогалини між “Lean може верифікувати програмне забезпечення” і “Lean надає ті ж гарантії для програмного забезпечення, що й для математики.”

1. Проблема коіндукції

Lean не має нативної підтримки коіндуктивних типів. це означає, що ви не можете природно моделювати:

  • нескінченні потоки (як цикли подій сервера)
  • ліниві структури даних
  • реактивні системи
  • будь-що, що працює вічно без завершення

Coq і Agda мають коіндукцію в своїх ядрах. Підхід Lean — кодувати коіндукцію через фактор-множини поліноміальних функторів (QPF), що працює, але є незручним і погано підтримується інструментарієм. Є поточна робота (QpfTypes), але вона не зріла.

Це важливо, тому що більшість реального програмного забезпечення не завершується: сервери, операційні системи, цикли подій UI. Lean може міркувати про обчислення, що завершуються, але хліб і масло системного програмування залишаються поза досяжністю.

2. Проблема середовища виконання

Навіть якщо ви доведете властивості про код Lean, ви стикаєтесь зі стеком проблем довіри:

a. Компілятор Lean не верифікований. ваш доведений код Lean компілюється в C, який компілюється gcc/clang. Нічого з цього не верифіковано.

b. Середовище виконання не верифіковане. Середовище виконання Lean (підрахунок посилань, керування пам’яттю, FFI) — це код C++ поза ядром. Помилки тут можуть порушити будь-які інваріанти, встановлені вашими доведеннями.

c. FFI руйнує все. FFI Lean дозволяє викликати довільний код C, який може робити будь-що — пошкоджувати пам’ять, порушувати безпеку типів, вводити невизначену поведінку. Тут немає історії верифікації.

d. Пов’язано з попереднім пунктов, бо іноді це має наслідки і для сторони доведення теорем Lean, оскільки деякі тактики, як native_decide, викликають середовище виконання, і таким чином дещо ускладнюють модель довіри виведеного доведення.

3. Проблема перекладу

Навіть з ідеальним середовищем виконання, вам все одно потрібно довіряти, що ваша модель Lean точно відображає програмне забезпечення, яке вас цікавить. Якщо ви моделюєте свою систему в Lean і доводите речі про модель, ці доведення нічого не говорять про ваш фактично розгорнутий код, якщо ви не можете верифікувати переклад; чого ви наразі не можете.

4. Верифікація апаратного забезпечення не є фокусом Lean

Coq має десятиліття роботи з верифікації апаратного забезпечення (CompCert тощо). Спільнота Lean — переважно математики. Із архівів Zulip: “здається, Lean був написаний для математиків, тоді як Coq був написаний для верифікації програмного забезпечення.”

Це повільно змінюється, але бібліотеки, інструментарій та експертиза ще недостатня в Lean.

5. Чому можна довіряти?

Якщо ви доводите щось у чистому Lean (без IO, без FFI, без unsafe), ви можете довіряти, що:

  • математичне твердження виконується (з урахуванням коректності Lean)
  • якщо ви витягнете код Lean і запустите його через інтерпретатор Lean, він обчислиться правильно

але “Lean верифікував моє програмне забезпечення” — це не те саме, що “мій розгорнутий бінарник є правильним”. Розрив між ними значний і наразі не подоланий. Якщо вас цікавить верифікація саме програмного забезпечення, то дозвольте представити вам нашого Господа і спасителя Idris2

Посилання

Виноски

  1. Всесвіти самі по собі також є типами, мешканцями яких є типи (приблизно). Вони існують для запобігання парадоксів (а також для узгодженої роботи поліморфізмів і великих елімінацій), що не стосується змісту цього блогу. думайте про це як про формальну вимогу охорони праці.

  2. Якщо ви не знаєте, що це означає, це те саме, що функції “компілюються” в інструкції переходу. машина (у цьому випадку ядро) бачить лише свою ISA (законні операції з типами).

  3. Хоча несуперечливість виводиться з коректності, це не єдиний спосіб її отримати. В принципі, це припускає існування систем, які є некоректними, але тим не менш несуперечливими. Простою мовою це припускає системи, які всіма засобами є цілком придатними як логічні системи, з усіма речами внутрішньо несуперечливими, і все ж доводять речі, які є повністю чужими тому, що ви мали на увазі. Пошук такої системи / пов’язаних робіт залишається уважному читачеві.

  4. Точніше, ZFC + n скінченних недосяжних, але значення цього розрізнення насправді не має значення для наших цілей. Для повноти зазначу, що точне формулювання тут полягає в тому, що Lean є еквіконсистентним з версією ZFC з доступом до скінченного числа недосяжних кардиналів. див. Наслідок 24 з дисертації Маріо Карнейро для детального доведення.