Re: Несколько вопросов вразброс
Артём Н. -> debian-russian@lists.debian.org @ Mon, 02 Jul 2012 20:36:58 +0400:
>> >> >> АН> Хм... Да, пожалуй, это верно.
>> >> >> АН> Но, если система выполняет ответственные действия..?
>> >> >> АН> Вопрос в том совместить требования надёжности и корректности с
>> >> >> АН> отказоустойчивостью и возможностью восстановления после сбоя?
>> >> >> Кодогенерация сишного или даже ассемблерного кода на какой-нибудь agda.
>> >> >> Которая из тебя душу вынет, пока ты ей корректность не докажешь.
>> >> >> Правда, порог вхождения весьма высокий.
>> >> АН> Про Agda не слышал. Что-то небогато по ней документации, но,
>> >> АН> насколько я понял, это система автоматического доказательства
>> >> АН> теорем. Не очень понимаю, как она может быть использована, в данном
>> >> АН> контексте: тесты же должны выполняться после компиляции..?
>> >> В данном случае компиляция выполняется вместо тестов. Тесты, в отличие
>> >> от доказательства корректности, не являются гарантией надежности.
>> АН> Но ведь полное доказательство корректности провести невозможно..?
>> Кто сказал?
АН> Ну это самоочевидно. В крайнем случае, возможно провести доказательство
АН> корректности отдельно взятой функции, если она минимальна (имеет строго
АН> определённые области значения и области определения, причём количество таких
АН> областей ограничено и известный тип зависимостей для этих областей), что
АН> позволяет доказать корректность, используя определённый набор правил...
АН> А как доказать корректность сложной функции, которая образует систему простых?
АН> Как проверить все связи?
АН> Как доказать корректность функции с побочными эффектами?
АН> И, например, "крайний" случай: возможно ли доказать корректность поведения
АН> произвольной ИНС?
С тех пор, надо сказать, наука шагнула довольно далеко вперед, и
рутинные операции типа проверки _всех_ связей компьютер делать уже
обучен.
А теория нам говорит, что нельзя построить универсальный автоматический
доказыватель программ. А того, что нельзя доказать конкретную
программу, даже довольно сложную - не говорит.
Но я сам с агдой не работал, и не готов тебе сказать, что именно она
позволит, а что нет. Видел, что, скажем, она не позволяет
скомпилировать функцию, определенную не на всем домене, в отличие от
хаскеля. Но по опыту работы на Хаскеле - уже даже его неполная проверка
типов, если делать типы под задачу, ловит на этапе компиляции ОЧЕНЬ
многое из того, что иначе пришлось бы ловить немеряным количеством
тестов. Да, остается возможность перепутать + с - и True с False, но за
два года работы на нем я таких ошибок сделал не больше десятка. И один
раз налетел на оставленную неполной функцию. А типичное правило с ним -
"если программа скомпилировалась, то почти наверняка она работает, и даже
правильно".
>> >> >> Любой статически типизированный функциональный язык с нормальной
>> >> >> системой типов, начиная с того же Haskell или Ocaml.
>> >> АН> Ocaml? Любопытно. Пожалуй, посмотрю подробнее.
>> >> АН> Для него есть какая-то IDE? И как с библиотеками?
>> >> Я знаю одну IDE на все случаи жизни. Emacs.
>> АН> И для всяких там GUI? ;-) В общем, я им не пользуюсь.
>> Ну да. Поскольку мои дизайнерские способности ниже средних, в отличие
>> от способностей в разработке поведения, я предпочитаю GUI, которые
>> пишут, а не рисуют. Внешний вид - дефолтный, а поведение описывается
>> словами.
АН> Дык, "внешний вид" - это не картинка кнопки, а компоновка. Всё же
АН> словами не опишешь. Видеть надо.
Компоновка как раз очень неплохо описывается словами. Заодно потом не
возникает типичных для мышконавозенного гуя ситуаций, когда при переводе
на русский половина надписей получается обрезанной, и в лучшем случае -
поперек, а то я у фотошопа видал, что видно нижнюю половину одной строки
и верхнюю - другой...
>> JAPH - это не для того, чтобы писать работающую программу :)
АН> Однако, они показывают вариации синтаксиса: такой разный стиль...
Это не столько вариации синтаксиса, сколько вариации его художественного
использования. На C, кстати, я тоже такие примеры видел - скажем,
круглую программу, вычисляющую пи.
>> Впрочем,
>> "как на шелл" - это лучше на шелле же и писать. Ну, с привлечением sed
>> и/или awk. perl позволяет писать совершенно третьим способом, и вот
>> именно им и надо писать надежные программы на нем.
АН> Эээ.... Каким?
use strict;
eval {...}; (не путать с eval "...")
system и open со списком, а не со строкой
or die "...";
open (my $fh, ...)
Для задач, которые можно решать на sh, этого достаточно. Ну, может, еще
IPC::Open2 и IPC::Open3, когда надо и на вход подавать поток, и на
выходе его забирать, да еще (в случае Open3) stderr анализировать.
Кстати, последнее, помнится, было довольно актуально при взаимодействии
с виндой, где команднострочные программы почему-то чаще пользуются
stderr, чем возвращают ненулевой код завершения в случае ошибок. Хотя у
ntbackup приходилось анализировать вообще лог.
>> >> А если ты хочешь действительно прекрасного синтаксиса, возьми tcl. У
>> >> него _полное_ описание синтаксиса и семантики укладывается, если я
>> >> правильно помню, в одну страницу A4, а if - всего лишь процедура из
>> >> стандартной библиотеки. И все необходимое из того, что я описывал, есть.
>> АН> Угу. Я читал описание. Не знаю, сомнительно...
>> Работает.
АН> Ну да, только почему-то широко его не используют... Разве что, для
АН> прототипов.
Пока я не стал большим любителем ОС Emacs, я пользовался tkabber в
качестве jabber-клиента. Остальные, сделанные на мейнстримных языках
для разработки Настоящих Приложений(tm), прямо скажем, существенно хуже,
существенно менее надежны, и в случае, когда ненадежность таки
срабатывает, их куда сложнее починить.
А что не широко - так надежные средства надежны потому, что работают на
другом уровне абстракций. Типичный индус(tm) такой уровень собственным
мозгом не освоил, поэтому пользоваться ими тупо не может. И не только
индус.
Тонкость с tkabber в том, что по крайней мере один из его ведущих
разработчиков - выпускник мехмата МГУ, и с уровнями абстракций у него
все хорошо... Поэтому ему на tcl удобно.
>> >> >> OPT_PARAM1=${OPT_PARAM1:-value1}
>> >> >> и позволить пользователю переопределять именно OPT_PARAM_1,
>> >> >> использование которой он потом увидит, а не неочевидно с нею связанную
>> >> >> ENV_USER_PARAM1
>> >> АН> Проверять наличие в окружении OPT_PARAM перед чтением конфига.
>> >> АН> И записывать во внутреннюю переменную. Затем делать подстановку переменной по
>> >> АН> умолчанию, взятой из конфига.
>> >> А чего ради так извращаться, если есть более прямой путь?
>> АН> Чтобы не усложнять конфиг и не вносить в него код. Не делать его неочевидным, не
>> АН> увеличивать в размере и, следовательно, не усложнять для изменения
>> АН> пользователем. При этом, гибкость почти не уменьшится.
>> Если конфиг надо писать пользователем, то опять же, возьми tcl.
АН> Ну, а в чём будет разница?
АН> Тут дело же не в реализации, а в подходе...
Разница будет в том, что у tcl язык задания переменных куда более
человеческий. Программисту пофиг, а пользователю - нет. (Я вот тут
сейчас по работе смотрю на описание функционала в cucumber, который
позиционируют как инструмент даже не для TDD, а для B(ehavior)DD - так у
него стиль описания еще более человеческий, и в комплекте штатные
переводы ключевых слов на N языков.)
>> АН> 2. Это просто обработка значений. Переменная как влияла на подмножество
>> АН> действий/объектов, так и влияет. Размер подмножества не расширяется.
>> Э, нет. Она начинает на него влиять куда как более обусловленно. "Если
>> выполняется это условие, проверяемое в 235-й строке, но не вон то,
>> проверяемое в 538-й, то влияет, а может, и нет..."
АН> Ээээ... Не очень вас понял. Есть переменная.
АН> Она влияет на определённое подмножество объектов.
АН> Её возможно задать.
АН> Задаётся она один раз.
АН> Задан она может быть в конфиге или в переменных окружения.
АН> Это понижает ортогональность (ради повышения настраиваемости), поскольку есть
АН> две точки входа, вместо одной - конфига.
АН> Есть два варианта реализации:
АН> 1. Обработка в конфиге.
АН> 2. Обработка в основном коде.
АН> При обработке в конфиге, есть ощущение того, что остаётся одна
АН> точка входа - конфиг. Реально, как две точки было, так две и
АН> осталось. Просто часть логики перелезла в конфиг. Что его
АН> усложнило.
При этом в конфиге _все_ переменные обрабатываются _единообразно_. Вся
однотипная логика выбора значений сконцентрирована в одном месте. Я,
собственно, опасаюсь, что если ее уносить в скрипт, она будет размазана
по всему скрипту и обладает риском расползания по мере жизни этого
скрипта.
АН> При обработке в основном коде возможен неправильный вариант, очень сильно
АН> повышающий ортогональность - размазать получение параметра по всему коду.
АН> Я же говорю о правильном - локализация получения параметров в одной функции,
АН> вызываемой один раз при инициализации.
АН> Где тут существенное понижение ортогональности по сравнению с первым вариантом?
>> >> АН> Лучший вариант - сделать единообразный формат конфига.
>> >> АН> Или сервер, отдающий конфиг в каком-либо общем формате.
>> >> Все известные мне попытки последнего сводятся в итоге к переусложнению
>> >> конструкции и тому, что самым сложным и ненадежным местом в системе
>> >> оказывается получение какой-то несчастной директории для сохранения
>> >> файлов.
>> АН> Хм... Любопытно. Может быть. Но вероятно, если такое требуется,
>> АН> вариантов нет.
>> Не вариантов, а мозгов нет.
АН> Хех, у меня?
Нет, у тех, кто делает такие системы конфигурации. Начиная с виндового
реестра, и заканчивая гномовским, и еще кем-то у нас в дистрибутиве же,
кто ради не помню чего, чуть ли не тоже конфигурации, тянет за собой
персональный экземпляр mysqld для каждого юзера. Узнать о существовании
sqlite он, видимо, ниасилил...
АН> Ну а какие варианты, когда требуется такая сложная система?
АН> Изобретать свой велосипед, в итоге сводящийся с СУБД?
Если такая сложная система конфигурации действительно требуется, то
уровень сложности самой задачи там запредельный. Настолько
запредельный, что я, со всем своим опытом, сто раз подумаю, прежде чем
начать ее решать.
И скорее всего, правильным решением будет не СУБД, и вообще не
конфигурация в привычном понимании, а протокол динамического
согласования, в духе какого-нибудь BGP.
СУБД же вообще предназначена для хранения данных, а не конфигурации. И
для хранения конфигурации подходит очень плохо.
>> Варианты как раз есть. Собственно,
>> проблема с ними в том, что они пытаются решать задачу, которую решать не
>> надо. Вообще не надо. И мало того, пытаются решать ее способом,
>> которым почти никакие задачи решать не надо, а те, которые надо, они
>> решать еще не доросли.
АН> Кто? o.O СУБД?
Те, кто делает такие конфигурации.
Reply to: