Программирование как контракт с дьяволом

[fat_yankey]

The purpose of a program is informal, often unstated, criterion and the transition from informal to formal objects must forever be unformalized, lest we caught in the paradox of assuming the formalization of an object we know only informally.

Social processes and proofs of theorems and programs
DeMillo, Lipton, Perils

Не проси богов ни о чем, рискуешь получить просимое.

Древние греки иллюстрировали эту максиму историями Мидаса и Титона. Первый попросил Диониса, чтобы всё, к чему он прикоснётся, обращалось в золото. И это ему было даровано. Как выяснилось на тестовом прогоне, в обществе где все едят руками такой дар может привести к смерти от истощения. Не говоря уже о сложностях в социальной жизни - ни поздороваться, ни обнять... За второго попросила любовница. Ему посчастливилось любиться с Эос, богиней утренней зари. Та и замолвила словечко Зевсу. Попросила для своего любовника вечной жизни. И это ему было даровано. Как выяснилось на тестовом прогоне, вечная жизнь без вечной молодости штука не очень приятная. Прожив заметно больше отмеренного человеку срока, Титон страдал от всех старческих болезней, включая слабоумие, не мог пошевелить ни рукой, ни ногой, ни, к полному расстройству Эос, более важными для любовника органами. Существует версия, что он постепенно ссохся в цикаду, видимо растворив внутренний скелет и нарастив внешний. Если версия верна, то среди этих мух-переростков есть одна бессмертная.

Античность закончилась, греческих богов дарующих человеку просимое в христианской Европе сменил дьявол. Европейские фольклор и литература во множестве содержат сюжеты сделки с дьяволом, смертный контрагент которых получал именно то, о чём просил. Впрочем, были и сюжеты в которых в формальную ловушку попадал дьявол, а не человек. Наиболее известный, видимо, это сюжет "приходи завтра" ("а чего ты сегодня пришёл, разве сегодня - завтра?").

Все сюжеты объединяет то, что герой комично или трагично проваливается в зазор между формальным (то что попрошено) и неформальным (то что хотелось).

Составление контракта с дьяволом, позволяющего через просимое получить желаемое, это высокое искусство формализации неформального, просчёт последствий, обработка исключительных ситуаций, тщательное обговаривание вырожденных и пограничных случаев... вобщем всё то, что составляет суть, ядро и основу работы программиста.

В конце концов, компьютер всегда делает именно то, о чём ты его попросил.

Comments

[fat-yankey.livejournal.com]

Замечу, что хоть там все "формально" и "тривиально", желающие определить семантику реальных языков высокого уровня, сталкиваются с определёнными трудностями.

Так что даже для формальных языков не все так уж тривиально.

Но вообще тема интересная. Действительно, для составления дуракоустойчивых контрактов с дьяволом нужен формальный язык. С формальной же семантикой.

[fat-crocodile.livejournal.com]

Чем дальше от ассемблера, чем выразительнее хочется сделать язык, тем сложнее с формальной семантикой. Но в компьютерном мире ассемблер все же очень близко, и это база, ниже которой идти некуда, так что можно все свести к нему и это не слишком сложно.

А у нас на роль очевидной базы претендует разве что физика, на уровне элементарных частиц. Все остальное уже сомнительно. Но эта физика настолько далеко внизу, что никаких шансов сказать что-то содержательное на таком языке просто нет.

И все объекты, которыми мы пользуемся в нашем языке настолько высокоуровневые, что что же они означают "точно" определить очень сложно.

Может быть можно найти другую формальную базу, поближе -- но это нужно уже как-то аргументировать.

[fat-yankey.livejournal.com]

Ну отчего же некуда ниже. Ниже ассемблера микрокод. И в современных процессорах это большой скачок. На интелях (или AMD) потроха уже кардинально отличаются от набора инструкций для x86.

Но допустим вы определили семантику ассемблерной программы. Помогате ли это с формализацией семантики высокоуровневого языка? Тут можно обратить внимание, что языки высокого уровня родились, чтобы семантика программы не зависела от железа. В этом смысле, допустим brainfuck вполне высокоуровневый язык.

Пробуя выразить семантику текста на языке высокого уровня через ассемблер, мы можем заметить, что даже для одного о того же железа (или одного и того же байткода) текст программы, даже на таком приближенном к ассемблеру языке как С, можно скомпилировать в довольно разные ассемблерные тексты используя разные компиляторы и их ключи. Теперь требуется доказывать, что семантика всех этих разных ассемблерных/байткодных текстов эквивалентна. В итоге выходит, что через редукцию вы определяет семантику какого-то конкретного семейства компиляторов, а не языка.

Если для С подход с редукцией дает хотя бы иллюзию корректного выхода, то попробуйте редуцировать к ассемблеру текст на SQL...

То есть даже с формальными языками редукция к нижнему уровню работает плоховато. С неформальными языками она не работает вовсе.

[fat-crocodile.livejournal.com]

Это не совсем так работает.

Некуда в том смысле, что на этом уровне уже достаточно точно задана семантика. Есть внутренние детали типа обращения к виртуальной памяти и т.п., но даже ими можно пренебречь и получить очень хорошую модель вычислений.

Ассемблер это уровень абстракции, на который можно опираться, он не подведет.

Действительно, Вы правы, когда я говорил про редукцию к ассемблеру я имел ввиду языки типа С/С++. Если авторы языка сделали свою виртуальную машину, редуцировать его к ассемблеру непродуктивно. Но это и не нужно, так как значит у нас есть другой надежный базовый уровень -- эта виртуальная машина.

[shadow-ru.livejournal.com]

C -- это макроассемблер. C++ -- это макроассемблер с ООП.

Есть же нормальные, человеческие языки с денотационной (напр., лямбда-исчисление) или аксиоматической (напр., категорной) семантикой: лиспы, ML'ли, Haskell.

[fat-yankey.livejournal.com]

Вместо "нормальные" и "человеческие" следовало бы сказать "академические"

[shadow-ru.livejournal.com]

Предпочту сказать "с высоким порогом вхождения", а то у некоторых и формальная грамматика -- "заумный академизм".

Не всем же на PHP кодить, некоторые могут освоить и инструменты помощнее.

[fat-yankey.livejournal.com]

Ну, если вы пишете парсер, то формальная грамматика ваш хлеб насущный. А если вы не пишете парсер, то заумный академизм.

Высокий порог вхождения с точки зрения промышленного программирования означает, что вам очень трудно будет набрать команду чтобы развивать и поддерживать codebase. Что эффективно и означает академизм.

[shadow-ru.livejournal.com]

Со вторым абзацем я полностью согласен, но вот что касается первого... Компьютерные программы имеют свойство расти и усложняться, а программисты -- матереть. Возможно, вчера достаточно было процедурного программирования, сегодня им (программе и программисту) требуется ООП, а завтра, глядишь, и разного рода заумный "матан". Поэтому не лучше ли сразу взять язык, спроектированный правильным образом?

Тут хорошим примером является PHP: обладая изначально отвратительным дизайном, но (из-за своей простоты) огромным числом пользователей, он постепенно в силу потребностей пользователей и необходимости более абстрактных методов написания программ эволюционировал в нечто относительно приличное. Правда, фундаментальные последствия родовой травмы так и остались непреодолены, поэтому писать на PHP -- пытка.

[fat-crocodile.livejournal.com]

Да, спасибо, я немного в курсе.

Просто пошел за логикой мысли про ограниченность и формальность компьютерного мира, а из неё сразу получается ассемблер и т.п.

[thesz.livejournal.com]

Сертификация программ на языке Си производится для определённого железа. Например, OS X является Unix на x86, но не на PowerPC (заново сертифицировать надо). Поэтому фиксация ассемблера важна.