Агата Сомова · старший инспектор
Вельский прав в одном: верить нашему Допуску он не обязан. Поэтому мы и не просим верить. Есть машина, которая проверяет доказательства и ничего больше. Её писали не мы и не он, её исходники открыты, и любой может прогнать на ней наше доказательство у себя дома. Я зову её механическим прокурором: она обвиняет каждое доказательство в неполноте, пока оно не докажет обратное. Садись, познакомлю.
Вопрос Вельского старше, чем Арбитр: кто проверит проверяющего? Ответ, который придумали в 1960-х для первых машинных проверщиков, такой. Сделай проверяющую часть маленькой, настолько, чтобы её мог перечитать человек, и открытой, чтобы её мог перепроверить любой. Всё остальное, включая того, кто пишет доказательство, можно не проверять: если доказательство неверное, маленькая часть его не примет.
Сегодня эта машина у тебя на столе. Она называется Lean, и после прошлого урока ты почти умеешь на ней писать: доказательство это терм, высказывание это тип, проверка доказательства это проверка типа.
урок из курса
Урок из курса «Логика и типы». Курс покупается один раз и остаётся навсегда: 500 ₽.
Оплата пока не подключена: премиум и курсы открываются промокодом.