Войти в систему

Home
    - Создать дневник
    - Написать в дневник
       - Подробный режим

LJ.Rossia.org
    - Новости сайта
    - Общие настройки
    - Sitemap
    - Оплата
    - ljr-fif

Редактировать...
    - Настройки
    - Список друзей
    - Дневник
    - Картинки
    - Пароль
    - Вид дневника

Сообщества

Настроить S2

Помощь
    - Забыли пароль?
    - FAQ
    - Тех. поддержка



Пишет asocio ([info]asocio)
@ 2008-02-18 13:32:00


Previous Entry  Add to memories!  Tell a Friend!  Next Entry
Настроение:awake

Опять гуманитарии-технари.
В топе - традиционная сказка про белого бычка:

Гуманитарий (философ, историк, в меньшей степени – филолог) строит достаточно произвольные конструкции, в истинность которых имеет склонность верить.
А вот правильный ответ на это:

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

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

И до кучи - психологический текст на ту же тему: "Наука и одержимый программист"

Психологическая ситуация, в которой оказывается предающийся подобным занятиям одержимый программист, в основном определяется следующими двумя явно противоположными обстоятельствами: 1) он считает, что может заставить ЭВМ делать все, что он хочет; 2) вычислительная машина постоянно предоставляет ему неопровержимые свидетельства его неудач. И это - позор для него. Здесь нет выхода. Инженер может смириться с тем, что есть вещи, которые он не знает. Программист же действует в мире, созданном исключительно им самим. Вычислительная машина бросает вызов его могуществу, а не знаниям.
{...}
Наука и техника поддерживаются благодаря тому, что они дают возможность властвовать и управлять. В той же степени, в какой вычислительные машины и вычисления могут считаться частью науки и техники, они пользуются той же кормушкой. Крайность, представляемая одержимым программистом, демонстрирует нам, что вычислительные машины обладают могуществом, достаточным для порождения бреда мании величия. Но этот род могущества вычислительной машины-просто крайний случай могущества, являющегося неотъемлемым элементом всякой системы мышления, находящей в самой себе подтверждение своей истинности.

Рекомендую прочесть.
Хотя лично мне и так понятно, что это именно технарь "строит достаточно произвольные конструкции, в истинность которых имеет склонность верить".
Человек, который воспринимает мир как программу в отладке - с очевидностью не может быть адекватен.


(Читать комментарии) - (Добавить комментарий)


[info]0serg@lj
2008-02-19 20:43 (ссылка)
Насчет "судя по всему, собираются активно применять" - это в каких приложениях, например? Вообще, функциональное программирование остается ныне в экспериментально-зачаточном состоянии. Его ниша - разработка очень специальных вещей, требующих (и поддающихся) математически строгой верификации. Т.е. это проектирование и верификация БИС, а также отдельные аспекты системного программирования.

Чем больше ограничений, тем больше изобретается всяких хитрых решений, направленных на обход этих ограничений. Это, конечно, тоже "полет фантазии", но очень своеобразный. Более близкий термин - "хитрость" (англосаксы часто используют жаргонное словечко black magic). Тут не столько фантазия, сколько глубочайшее понимание принципов работы "железа", и умение видеть несколько вариантов решения одной и той же проблемы. Есть, конечнО, и демосцена, но это явно особое явление, не связанное с низкоуровневым программированием в целом.

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]thesz@lj
2008-02-19 21:01 (ссылка)
Да вот в каких приложится, в таких и будут применять.

Как я понимаю, вы еще и про функциональное прогарммирование все знаете, коль позволяете себе так свободно рассуждать на эту тему. Не поделитесь, где применяется, допустим, OCaml? Или Haskell?

Мы, видимо, говорим о разных ограничениях. Вы, судя по всему, о получившихся эволюционным путем (как пример - C++). Там, действительно, необходимо обходить ограничения системы типов и, часто, библиотеки времени исполнения. Я говорил об ограничениях, которые накладывает проектировщик языка программирования, отлично знакомый с проблематикой. Например, знающий, зачем нужна линейная логика во встроенных системах.

Да, кстати, вы правы. Мы успешно применили Хаскель для проверки архитектуры вполне современного микропроцессора. См. http://mskhug.ru/wiki/MskHUG1_1

Но здесь, как я понимаю, вы просто ткнули пальцем в небо и совершенно случайно попали. Просто потому, что вся индустрия по производству СБИС не использует формальных методов на полную. Тесты, тесты. Она не использует ФЯ наподобие Хаскеля. Это делают только очень отважные люди наподобие нас или ARM (по слухам).

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]0serg@lj
2008-02-20 11:14 (ссылка)
Нет, естественно, про ФП я знаю не так уж и много.
Однако я достаточно хорошо знаю историю. И знаю, сколько надежд возлагали на ФП, когда это направление еще только зарождалось. И знаю результаты 20 последующих лет. Не нашли ФП себе применения в широких областях - не нашли, точно также как и многие другие замечательные на первый взгляд идеи.

А насчет того что современная индустрия по производству СБИС "не использует формальных методов на полную" - это Вы хорошо пошутили. Если бы Вы эти слова сказали лет 20 назад, я бы Вам даже поверил :)). Но последние 10 лет все более-менее серьезные люди СБИСы верифицируют формальными методами. Правда, не микросхемы полностью (слишком трудоемко), а отдельные функциональные блоки - чего, впрочем, обычно вполне достаточно. Да и Хаскелл, насколько я понимаю, они не используют - вместо этого используют что-то verilog-подобное. Если говорить, скажем, о CPU Intel, то последний "камень" который они тестировали "моделированием" - это самый первый Pentium...

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]thesz@lj
2008-02-20 11:20 (ссылка)
Да что вы говорите! И когда же зарождалось направление ФП?.. Какие же надежды были с ним связаны? ;)

Но последние 10 лет все более-менее серьезные люди СБИСы верифицируют формальными методами.

Synopsis знаете? Должны знать. Так вот, в презентации их презентер говорил, что они не могут перебрать все возможные пути преобразований состояний на основе всех возможных входов. И что надо пользоваться тестами. "И вот, смотрите, какие у нас хорошие возможности по поддержке тестирования! Особенно вот это, это очень нравится менеджерам!! Оно позволяет понимать, где задержка!!!"

Про тесты была отдельная часть, про верификацию - пара слайдов из этой части.

Формальная верификация, хаха три раза.

Да и Хаскелл, насколько я понимаю, они не используют - вместо этого используют что-то verilog-подобное.

Хаскель используется не для тестирования, а для проверки идей. verilog-подобное в этих случаях не подходит.

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]0serg@lj
2008-02-20 20:24 (ссылка)
Да что вы говорите! И когда же зарождалось направление ФП?.. Какие же надежды были с ним связаны? ;)

ФП как направление, насколько я понимаю, зародилось в 60е и более-менее сформировалось в 70е годы прошлого века. С тех пор многие считали (и продолжают считать :)) что ФП - более совершенное и перспективное направление развития языков программирования, и с развитием вычислительных мощностей именно ФП-языки станут новым стандартом. Практика показала, что до сих пор этого не произошло.

Далее, про верификацию. Современные методы ПОЗВОЛЯЮТ перебрать все возможные варианты входных состояний и оценить, верные ли результаты при этом получаются - в 90е годы данное направление очень бурно развивалось, и достигнутые результаты по преодолению проблемы комбинаторного взрыва там впечатляют. Там по-прежнему масса нерешенных проблем - от большой вычислительной сложности (из-за которой трудно просчитать большие схемы) до ограничений на модели. По этой причине "серебряной пулей" эти методы не являются, и вполне естественно, что не существует софта, который бы на вход получал схему, а на выходе однозначно говорил, работает она или нет. Однако это не мешает серьезным производителям заниматься верификацией своей логики формальными методами, создавая для этого специализированные решения и модели.

В отношении "проверки идей" - обычно под термином "верификация" понимают все-таки не проверку идей, а проверку того, что определенная модель работает "правильно" - соответствует набору требований, полностью описывающих то, чего мы от этой модели хотим.

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]thesz@lj
2008-02-20 21:15 (ссылка)
Да что вы говорите! И когда же зарождалось направление ФП?.. Какие же надежды были с ним связаны? ;)

ФП как направление, насколько я понимаю, зародилось в 60е и более-менее сформировалось в 70е годы прошлого века. С тех пор многие считали (и продолжают считать :)) что ФП - более совершенное и перспективное направление развития языков программирования, и с развитием вычислительных мощностей именно ФП-языки станут новым стандартом. Практика показала, что до сих пор этого не произошло.
Лямбда-исчисление - основа ФП, - было представлено логиком Алонсо Черчем (Alonso Church) в 1935 году. Машина Тьюринга была представлена Аланом Тьюрингом в 1936 году.

ЛИ разрабатывалась в качестве лишенного парадоксов (парадокс забыл, чего имени, Гильберта, по-моему) средства выражения вычислений. Не оправдало.

Это стандартная ловушка, в которую попадают все, кто думает, что знает историю.

Чисто функциональных языков раз-два и обчелся. Назову два самых известных, это Clean и Haskell. Они отличаются от ML/Lithp чистотой, там есть ядро, которое не позволяет побочных эффектов (referentially transparent core language). Haskell, так вообще - лямбда-исчисление с толстым слоем синтаксического сахара сверху.

Оный Хаскель появился в 1989 году, а первые реализации с нормальным вводом-выводом в 1992 году или позже. Это далеко не 70-е.

До этого главным событием были ML - вывод типов, сравнение с образцом, все очень удобно, - и Id90, язык с lenient порядком вычислений. Это секретное оружие dataflow, он эффективно распараллеливался до 64-х процессоров на Connection Machine 5, CM-5 (конец 80-х). Не пошел потому, что был "не Фортран" и из-за неудобства программирования (M-память может дать прикурить любому;).

Кстати, энергичный порядок вычислений (ML, LISP) не параллелится. Параллелится ленивый или lenient (ленивый - приводом к lenient, надо отметить). Собственно, Clean когда-то был Concurrent Clean, возлагались на него надежды, но он перестал им быть.

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

Мне неизвестно про 70-е и 80-е в истории функциональных языков. Вся история творилась до конца 30-х и после 90-го, в промежутке была подготовка к рывку (Hindley-Milner type inference algorithm, inductive data types and pattern matching, G-machine и тп). Даже Id90 благополучно мигрировал в pH, а разработчики железа для него - в сторону multithreaded processors.

Теперь про моделирование.

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

И про проверку.

Synopsis, с их 800 PhD, решает проблему верификации очень просто - "мы генерируем случайные стартовые точки состояний и из них отправляем верификацию моделей; глубоко не ходим, ничего гарантировать не можем, объем очень большой; пользуйтесь тестами."

То, чем пользуется Интел, IBM и AMD внутри себя, на индустрию не влияет. Индустрия пользуется Synopsis, Cadence и прочими Mentor Graphics. И Synopsis, по-моему, лидер. ;)

(Ответить) (Уровень выше)


(Читать комментарии) -