02.07.2012 19:42, Artem Chuprina пишет:
> Артём Н. -> debian-russian@lists.debian.org @ Mon, 02 Jul 2012 19:13:04
> +0400:
>
> >> >> АН> Хм... Да, пожалуй, это верно.
> >> >> АН> Но, если система выполняет ответственные действия..?
> >> >> АН> Вопрос в том совместить требования надёжности и корректности с
> >> >> АН> отказоустойчивостью и возможностью восстановления после сбоя?
> >> >> Кодогенерация сишного или даже ассемблерного кода на какой-нибудь
> agda.
> >> >> Которая из тебя душу вынет, пока ты ей корректность не докажешь.
> >> >> Правда, порог вхождения весьма высокий.
> >> АН> Про Agda не слышал. Что-то небогато по ней документации, но,
> >> АН> насколько я понял, это система автоматического доказательства
> >> АН> теорем. Не очень понимаю, как она может быть использована, в данном
> >> АН> контексте: тесты же должны выполняться после компиляции..?
> >> В данном случае компиляция выполняется вместо тестов. Тесты, в отличие
> >> от доказательства корректности, не являются гарантией надежности.
> АН> Но ведь полное доказательство корректности провести невозможно..?
> Кто сказал?
Ну это самоочевидно. В крайнем случае, возможно провести доказательство
корректности отдельно взятой функции, если она минимальна (имеет строго
определённые области значения и области определения, причём количество таких
областей ограничено и известный тип зависимостей для этих областей), что
позволяет доказать корректность, используя определённый набор правил...
А как доказать корректность сложной функции, которая образует систему простых?
Как проверить все связи?
Как доказать корректность функции с побочными эффектами?
И, например, "крайний" случай: возможно ли доказать корректность поведения
произвольной ИНС?
> >> >> Любой статически типизированный функциональный язык с нормальной
> >> >> системой типов, начиная с того же Haskell или Ocaml.
> >> АН> Ocaml? Любопытно. Пожалуй, посмотрю подробнее.
> >> АН> Для него есть какая-то IDE? И как с библиотеками?
> >> Я знаю одну IDE на все случаи жизни. Emacs.
> АН> И для всяких там GUI? ;-) В общем, я им не пользуюсь.
> Ну да. Поскольку мои дизайнерские способности ниже средних, в отличие
> от способностей в разработке поведения, я предпочитаю GUI, которые
> пишут, а не рисуют. Внешний вид - дефолтный, а поведение описывается
> словами.
Дык, "внешний вид" - это не картинка кнопки, а компоновка. Всё же словами не
опишешь. Видеть надо.
> JAPH - это не для того, чтобы писать работающую программу :)
Однако, они показывают вариации синтаксиса: такой разный стиль...
> Впрочем,
> "как на шелл" - это лучше на шелле же и писать. Ну, с привлечением sed
> и/или awk. perl позволяет писать совершенно третьим способом, и вот
> именно им и надо писать надежные программы на нем.
Эээ.... Каким?
> >> А если ты хочешь действительно прекрасного синтаксиса, возьми tcl. У
> >> него _полное_ описание синтаксиса и семантики укладывается, если я
> >> правильно помню, в одну страницу A4, а if - всего лишь процедура из
> >> стандартной библиотеки. И все необходимое из того, что я описывал, есть.
> АН> Угу. Я читал описание. Не знаю, сомнительно...
> Работает.
Ну да, только почему-то широко его не используют... Разве что, для прототипов.
> >> >> OPT_PARAM1=${OPT_PARAM1:-value1}
> >> >> и позволить пользователю переопределять именно OPT_PARAM_1,
> >> >> использование которой он потом увидит, а не неочевидно с нею связанную
> >> >> ENV_USER_PARAM1
> >> АН> Проверять наличие в окружении OPT_PARAM перед чтением конфига.
> >> АН> И записывать во внутреннюю переменную. Затем делать подстановку
> переменной по
> >> АН> умолчанию, взятой из конфига.
> >> А чего ради так извращаться, если есть более прямой путь?
> АН> Чтобы не усложнять конфиг и не вносить в него код. Не делать его
> неочевидным, не
> АН> увеличивать в размере и, следовательно, не усложнять для изменения
> АН> пользователем. При этом, гибкость почти не уменьшится.
> Если конфиг надо писать пользователем, то опять же, возьми tcl.
Ну, а в чём будет разница?
Тут дело же не в реализации, а в подходе...
> >> >> Зато, правда, тогда зачитывать этот конфиг можно будет не
> >> >> только шеллом. Но поскольку по опыту ситуация, когда один и тот же
> >> >> конфиг и сурсится шеллом, и читается чем-то еще, встречается крайне
> >> >> редко...
> >> АН> По-моему, тут дополнительные сложности и нарушение ортогональности...
> >> А по-моему, нарушение ортогональности - это как раз модификация
> >> результата чтения конфига в использующем его скрипте.
> АН> В чём нарушение?
> АН> 1. Модификации не происходит. Уменьшение ортогональности даёт
> взаимодействие с
> АН> переменными окружения (возможность переопределения значений сама по
> себе),
> АН> независимо от реализации.
> Модификации не происходит. А вот как соотносится то, что написано в
> конфиге и то, что используется на самом деле, хрен разберешь.
Да, согласен. Но здесь проблема в очевидности. Вероятно, понятия связаны.
> АН> 2. Это просто обработка значений. Переменная как влияла на подмножество
> АН> действий/объектов, так и влияет. Размер подмножества не расширяется.
> Э, нет. Она начинает на него влиять куда как более обусловленно. "Если
> выполняется это условие, проверяемое в 235-й строке, но не вон то,
> проверяемое в 538-й, то влияет, а может, и нет..."
Ээээ... Не очень вас понял. Есть переменная.
Она влияет на определённое подмножество объектов.
Её возможно задать.
Задаётся она один раз.
Задан она может быть в конфиге или в переменных окружения.
Это понижает ортогональность (ради повышения настраиваемости), поскольку есть
две точки входа, вместо одной - конфига.
Есть два варианта реализации:
1. Обработка в конфиге.
2. Обработка в основном коде.
При обработке в конфиге, есть ощущение того, что остаётся одна точка входа -
конфиг. Реально, как две точки было, так две и осталось.
Просто часть логики перелезла в конфиг. Что его усложнило.
При обработке в основном коде возможен неправильный вариант, очень сильно
повышающий ортогональность - размазать получение параметра по всему коду.
Я же говорю о правильном - локализация получения параметров в одной функции,
вызываемой один раз при инициализации.
Где тут существенное понижение ортогональности по сравнению с первым вариантом?
> >> АН> Лучший вариант - сделать единообразный формат конфига.
> >> АН> Или сервер, отдающий конфиг в каком-либо общем формате.
> >> Все известные мне попытки последнего сводятся в итоге к переусложнению
> >> конструкции и тому, что самым сложным и ненадежным местом в системе
> >> оказывается получение какой-то несчастной директории для сохранения
> >> файлов.
> АН> Хм... Любопытно. Может быть. Но вероятно, если такое требуется,
> АН> вариантов нет.
> Не вариантов, а мозгов нет.
Хех, у меня?
Ну а какие варианты, когда требуется такая сложная система? Изобретать свой
велосипед, в итоге сводящийся с СУБД?
> Варианты как раз есть. Собственно,
> проблема с ними в том, что они пытаются решать задачу, которую решать не
> надо. Вообще не надо. И мало того, пытаются решать ее способом,
> которым почти никакие задачи решать не надо, а те, которые надо, они
> решать еще не доросли.
Кто? o.O СУБД?
--
To UNSUBSCRIBE, email to debian-russian-requ...@lists.debian.org
with a subject of "unsubscribe". Trouble? Contact listmas...@lists.debian.org
Archive: http://lists.debian.org/4ff1ce2a.9070...@yandex.ru
