Каким должен быть язык программирования? Анализ и критика Описание языка Компилятор
Отечественные разработки Cтатьи на компьютерные темы Компьютерный юмор Новости и прочее

Права доступа к переменным

Со времени предыдущих историй прошло всего-то лет пять, а как стал меняться компьютерный мир. В том числе, и в НПО. В отделах стали появляться персоналки: у кого IBM-PC/XT, у кого «Правец», у кого ЕС-1840. Число пользователей БЭСМ и даже ЕС и СМ-4 стало асимптотически приближаться к нулю. На фоне новых возможностей все их «фишки» сразу побледнели. Например, смешно, что ещё недавно какая-нибудь замена терминала VT-340 на VT-52100 c памятью на 5 страниц, позволяющей вводить текст ещё до включения БЭСМ, казалась важной.

            Расстаться со старыми заделами и навыками психологически мне было даже проще, чем многим, поскольку после двухлетнего отсутствия я вернулся на работу уже в другой отдел и, так сказать, сразу отрекся от старого мира и отряхнул его прах со своих ног. Впрочем, последние годы работа с БЭСМ через диалоговую программу «Пульт» (разработка МГУ) как раз очень напоминала работу за первыми персоналками и поэтому переход был несложным. А вот задачи стали другие. Отдел занимался разработкой ПО системы управления «Энергия-Буран». Точнее, отдел занимался комплексацией, верификацией, взаимодействием с наземным ПО и т.п., а собственно разработкой занималось сразу несколько отделов. Я впервые принимал участие в проекте, где были заняты десятки программистов. Язык программирования — ПРОЛ-2 разработки ИПМ АН СССР.

            Вообще-то, девичья фамилия этого языка была «Пролог-Ц» от ПРОграммирования ЛОГики. Но поскольку в то время на слуху был японский Пролог с его транспьютерами, вероятно разработчикам надоело отвечать на вопросы о применении транспьютеров в «Буране», поэтому вторая версия языка вышла под таким скромным и безликим именем.

            Язык был специфический, для задач управления. Типичный алгоритм выглядел так: выдать такую-то команду, подождать 0.3 миллисекунды, проверить такую-то переменную. Если она нулевая — выдать другую команду и запустить такой-то процесс. И все в таком духе.

            Разумеется, инструментальных средств под x86 ещё не было. Поэтому в отделе родилась идея, а затем — предложение — указание — распоряжение — создать отладочный или, точнее, проверочный транслятор для персоналки. Во-первых, он облегчит процесс комплексирования и верификации, а во-вторых, возможно, несколько увеличит производительность и в других отделах, сократив число подходов к штатному транслятору (на ЕС).

            Сказано-сделано. Часть транслятора была написана на ассемблере и поэтому летал он ласточкой.

            В то время было модно извлекать из внутреннего динамика персоналки разные звуки. Ребята из моего бывшего отдела даже спаяли простой АЦП на параллельный разъем и через микрофон от древней «Яузы-5» мы записали ряд сигналов и фраз. Например, при отсутствии замечаний проверочный транслятор бесцветным голосом произносил половинку подходящего к случаю т.н. «заходеризма» (т.е. афоризма Б. Заходера): «если взглянуть формально, все обстоит нормально».

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

            Для повышения надежности в языке ПРОЛ-2 описание нелокальных переменных должно было включать и права доступа в виде списка имен процедур, которым разрешается к этой переменной обращаться.

            Так вот, проверочный транслятор выдал большое число сообщений, что идет обращение к переменным без права доступа. Отдельческое начальство поморщилось: дескать, уж такую несложную ветку в проверочном трансляторе можно было бы сделать с первого раза и без ляпов. Штатный транслятор давно отлажен и многократно проверен. Таких нарушений он бы просто не пропустил. Откуда в проверенных программах взялись сотни ошибок доступа?

            Но разбирательство показало, что таки-да, в штатном трансляторе помарка. Вероятно, она проникла в транслятор, когда выяснилось, что ресурсов одной БЦВМ не хватает и приняли решение поставить в «Буране» две машины, разделив ПО между ними. Транслятор подправили для двух ЭВМ, но он перестал проверять доступ переменной из процедуры на соседней БЦВМ (или, наоборот, на той же, я уже не помню). В общем, выключилась одна из проверок.

            После выяснения этого даже было совещание. Не столько на тему помарки в трансляторе, сколько на тему технологи разработки. Ведь рассчитывали на что? Что разработчики проанализируют сферу действия каждой переменной и явно и осмысленно укажут множество объектов, которые могут эту переменную читать/писать. А что получилось в реальности? Разработчики чихали на анализ и совали свои модули в транслятор. Ругнулся он по поводу прав — так и быть допишем список, не ругнулся — и так сойдет. В текстах даже нашли издевательские описания нелокальных переменных с пустыми списками, т.е. по правилам языка к ним вообще никто не мог обращаться. И при этом все работало нормально и казалось, что защита от порчи «чужих» данных хорошо обеспечена.

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

            А что, разве при отработке не было случаев, когда один процесс портил переменную другому процессу? Конечно, были. Только во всех этих случаях как раз с доступом все было хорошо.

            С тех пор прошло уже десятка три лет. Программирование и теоретически и практически ушло далеко вперед и добилось больших успехов.

            Но когда я читаю о новом языке, который «просто не позволит вам написать ошибочную конструкцию», о том, что какая-нибудь инкапсуляция или запрет преобразования типов автоматически сделают вашу программу надежной и правильной и о прочих, ежедневно отливаемых «серебряных пулях», я нет-нет, да и вспомню ту давнюю историю, как иллюстрацию того, что формальные методы борьбы за правильность и надежность чаще всего дают и формальные же результаты. В духе так и не озвученной нами в трансляторе второй половины афоризма Бориса Заходера.

Автор: Д.Ю.Караваев. 10.02.2017

Опубликовано: 2018.08.26, последняя правка: 2019.01.28    20:43

ОценитеОценки посетителей
   ██████████████████████████████████████████ 1 (100%)
   ▌ 0
   ▌ 0
   ▌ 0

Отзывы

     2018/10/21 13:50, Comdiv          # 

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

     2018/10/21 20:13, Автор сайта          # 

Согласен: один частный случай не говорит о том, что формальные методы изрядно хромают. Но во фразе «в теории, теория и практика неразделимы; на практике это не так» больше правды, чем шутки. Читаю как-то на Хабре статью о том, как замечателен Haskell. Задаю в комментариях вопрос автору: «А как в этом языке отслеживается переполнение?». Мне отвечают: «Никак». Язык, который вроде бы как находится на передовом рубеже, — и никак. Между тем Дмитрий Юрьевич в своём компиляторе PL/1 контролизует переполнения и бьёт тревогу из-за того, что команда INTO, которая делала такой контроль «дешёвым», исключена из архитектуры x86-64. Т.е. на словах он критикует, а на деле делает то, что и должно.

Здоровый скепсис по поводу чьих-то разрекламированных возможностей полезен.

     2018/10/22 15:13, Comdiv          # 

Переполнение чего — массивов? Судя по REPL контролируется. Если чисел, то числа там безразмерные. Это далеко не всегда хорошо, даже если не учитывать производительность.
А скепсис — он для всего полезен. Но за скепсис у нас нередко принимают нечто иное.

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

1. В полных по Тьюрингу языках невозможно что-либо запретить полностью, потому что на них можно смоделировать всё что угодно, и любую ошибку тоже. Можно лишь сократить вероятность ошибок.

2. Очень сложно оценить предотвращение чего-либо. Когда формальный метод спасает от ошибки, то Вы просто этого не замечаете. В силу 1-го пункта ошибка всё равно может проявится, а уж это Вы заметите. После этого можно смело иронизировать про формальные методы, особенно, если они не смогли предотвратить ошибку, не связанную с ними.

3. Люди любят всё доводить до абсурда, чтобы ни было предложено.

     2018/12/18 18:33, Автор сайта          # 

Пораздумывал над Вашей фразой «формальные методы борьбы за правильность и надежность чаще всего дают и формальные же результаты». А если отказаться от формальных методов, то какие альтернативы?
  • Отладка. Дотошно проверяем каждый бит и байт. Работа и труд всё перетрут. Но при росте объёма и сложности программы трудоёмкость отладки растёт не в линейной прогрессии. Во-вторых, полная отладка марсохода возможна только на Марсе — имитация внешней среды не всегда возможна.
  • Других альтернатив не вижу. Не кропить же написанный код святой водой?
Получается, что уповать можно только на науку и на её формальные методы. А в описанной Вами истории формальные методы оторвались от реальности, вот и результат.

     2018/12/18 20:28, Comdiv          # 

Просто в статье смешиваются понятия формальных методов и формалистических. Выступая против второго, высмеивают первое.

     2018/12/19 18:34, Автор сайта          # 

Но всё-таки надо отметить, как бы ни была хороша формализация, её результаты всё равно надо сверять с жизнью. Меня иногда удивляют к завышенные ожидания от «доказательства правильности программ». Что доказали? Доказали соответствие результата техническому заданию, которое вполне может быть в чём-то неправильным или что-то не учесть. Кому доказали? Да тому, кто писал это техническое задание. Но даже правильное задание и 100-процентное его выполнение могут столкнуться с неудачей.

Когда МВД перешло с бумажных архивов на электронные базы данных, то начался обмен старых документов на новые. Одной женщине много месяцев не могли выдать новый паспорт. Причина: она, согласно ранее выданных документов, родилась 31 ноября. В базу данных МВД эту дату внести невозможно: тип данных «дата» не имеет реализации для 31 ноября. Но внести надо. Тут даже абсолютно правильное ТЗ потерпело неудачу. Внести в базу другую, правильную дату тоже нельзя — по закону в новых документах всё должно соответствовать старым.

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

     2018/12/19 23:46, Comdiv          # 

В каком смысле "надо отметить"? Только основанный на жизни формализм и имеет смысл. Формализмы, высасываемые из пальца — это и есть формалистический подход.

Но даже правильное задание и 100-процентное его выполнение могут столкнуться с неудачей.

Какое же оно тогда правильное? Узнали, что было неправильно — исправили. Единственная серьёзная причина отказываться от формального доказательства корректности — это дороговизна его достижения, а потому недостижимость для большинства задач.

     2018/12/20 13:58, Автор сайта          # 

Да никому и в голову не могло прийти, что в ноябре 31 день. Любая академия наук утвердила бы ТЗ на тип данных «дата». И только реальная жизнь нашла ошибки в правильном ТЗ. Дискутировать тут особо не о чем.

     2018/12/20 14:14, Бурановский дедушка          # 

прочих, ежедневно отливаемых «серебряных пулях»

31 ноября

На каждую серебряную пулю найдётся ствол с винтовой нарезкой

     2018/12/20 14:21, MihalNik          # 

Да никому и в голову не могло прийти, что в ноябре 31 день. Любая академия наук утвердила бы ТЗ на тип данных «дата».

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

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

     2018/12/21 18:34, Автор сайта          # 

Задним умом все крепки. А если Вы за всё хорошее и против всего плохого, то ответьте на один простой вопрос, связанный со временем. Раз уж мы рассуждали тут про даты. Загадываю Вам загадку.

31 декабря 2011 года из Ростова-на-Дону вышел поезд, когда часы на вокзале показывали 23 часа, 00 минут, 00 секунд. Когда он пришёл в Донецк 1 января 2012 года, то часы на донецком вокзале показывали 01 час, 00 минут, 00 секунд. Вопрос: сколько секунд был в пути этот поезд? Обоснуйте свои выкладки. Только решите эту задачку без ошибок, чтобы не уподобляться тем, кто забыл про 31 ноября.

     2018/12/22 02:20, MihalNik          # 

Так говорили уже про задний ум, но какой-нибудь Дракон же для непрограммистов Вам не нравится. Потому что сложнейшие схемы в голове проворачиваете. А жить мы будем и дальше в стране заднего ума. Где ТЗ изначально не по уму, а по распилу денег, где никакие "шибко умные" никому не нужны.

     2018/12/22 20:36, Автор сайта          # 

Ну к чему кидаться в какие-то высокие материи? Зачем повторять либеральные пассажи про «эту страну» и «распил денег»? Просто напишите формулу решения для загадки про поезд из Ростова в Донецк. Одна формула и несколько цифр вместо тысячи слов. Просто я моделирую ситуацию: Вы пишите ТЗ, и когда допускаете ошибку, то получаете на свою голову обвинения в чём угодно: и в распиле, крепости задним умом и прочих грехах. Просто напишите правильное ТЗ, то бишь формулу расчёта времени в секундах. И всё. Будет правильно — Вы спаситель Родины, нет — Вы «распильщик этой страны». Ну или признайтесь, что предпочитаете постоять в сторонке.

Ну а «Дракон» тут вообще ни при чём. Как бы он помог в случае с 31 ноября? «Дракон» — это про алгоритмы. А тип «дата» — это про данные. Если взять тип «дата» из Unix, то он имеет целочисленное представление, поэтому втиснуть 31 ноября между 30 ноября и 1 декабря не удастся. А если взять тип «дата» из формата dbf, то это строка вида «20181231». Она позволяет втиснуть спорную дату. И где тут пахнет сложными алгоритмами?

Сложнейшие схемы в голове — это глупость. Всё сложное надо разбивать на множество мелких и браться только за лёгкие задачи. И решать их по очереди. Есть у меня перед глазами пример мастерства декомпозиции, я тут только в подмастерья гожусь.

     2018/12/23 05:04, MihalNik          # 

Как бы он помог в случае с 31 ноября? «Дракон» — это про алгоритмы. А тип «дата» — это про данные.

При чем тут тип "дата" в какой-то операционной системе (или конкретной программе) и интервал времени? Шкала времени известна, секундные поправки, если они необходимы — известны, ну, будет формула не вида Б-А, что с того? Форматы данных не задают алгоритмы. Раздайте программистам или тем более студентам структуру узла сбалансированного дерева (красно-чёрного или АВЛ) и предложите построить процедуры вставки/удаления с асимптотикой O(ln(N)). Сколько из них самостоятельно догадаются/вспомнят и сколько у них уйдет на это времени? А это самый простейший пример. Формат данных не определяет алгоритмы, а выбирается исходя из них.

31 ноября — проблема в АЛГОРИТМЕ обработки данных. Во-первых, необходимо зарегистрировать ошибку в алгоритме. Далее ОТВЕТСТВЕННЫЙ технический специалист должен как можно скорее провести анализ и предложить решение. Например: завести базу данных исключителыных соответствий. Довести до законодательной инстанции о том, что имеются документы с ошибками и для их исправления необходима АДМИНИСТРАТИВНАЯ ПОПРАВКА на случай несоответствия данных в новых и старых документах — сверять их на соответствие по базе данных, куда заносить все исключительные ситуации.

Давайте я тоже Вам дам загадку: Вам дали посчитать площадь круга. Допустимая погрешность 0,01%. Вам дали формулу S=Pi*R^2 и сказали считать число Pi строго равным 3. Ваше решение?

     2018/12/28 22:07, Автор сайта          # 

Форматы данных не задают алгоритмы... Формат данных не определяет алгоритмы, а выбирается исходя из них.

Форматы зависит зачастую не от алгоритма, а от достаются «извне». Например, классификатор адресов России (КЛАДР) достаётся нам в виде готовых данных определённого формата, а не в виде готовых алгоритмов.

31 ноября — проблема в АЛГОРИТМЕ обработки данных.

Алгоритм тут простой:

если (полномочия текущего пользователя && разрешена запись неправильных данных)
дата рождения = поле ввода даты рождения;
Этот алгоритм одинаков хоть для формата Unix, хоть для формата dbf. Просто в первом случае правильное ТЗ не учитывает неправильность реальной жизни, его надо подгонять под эту жизнь.

Вам дали посчитать площадь круга. Допустимая погрешность 0,01%. Вам дали формулу S=Pi*R^2 и сказали считать число Pi строго равным 3.

Вы, вероятно, имели в виду относительную погрешность, а не просто погрешность.Погрешность — это разность между фактическим измерением и истинным. Относительная — это отношение погрешности к числу. Тогда:
S приблизительная = 3 * радиус * радиус
S точная = Пи * радиус * радиус
относительная погрешность = (S точная - S приблизительная) / S приблизительная
относительная погрешность = (Пи - 3) / 3
относительная погрешность = (3.14159 - 3) / 3
относительная погрешность = 0.072 или 7.2%
В Ваши 0,01% «вписаться» можно только тогда, когда вместе с Пи синхронно «колеблется» квадрат радиуса. Если на экране компьютера нарисовали круг площадью 4 пиксела, то какой радиус у этого круга? Смотришь, и видишь, что радиус равен единице. Такое возможно при больших погрешностях. А Вы таки не решили мою задачку. Ведь кто-то пишет ТЗ на программу составления транспортных расписаний, а кто-то это ТЗ воплощает. Т.е. задача не оторвана от жизни.

     2019/01/02 02:58, rst256          # 

С 31 ноября алгоритм простой, по закону паспорт, содержащий неверные данные, считается недействительным. Поэтому просто шлём его владельца получать новый паспорт. Как получит «новый» (но старого образца) паспорт уже без ошибок, сможет наконец отдать его на замену и получить новый.

А задача с поездами вроде бы решается так. Примем допущение что в обоих городах показания времени брались с часов, показывающих местное время. Ведь на вокзалах принято так же устанавливать часы, показывающие время и в других часовых поясах. Согласно найденным источникам на том период в Донецке был UTC+2:
(https://ru.wikipedia.org/wiki/%D0%92%D1%80%D0%B5%D0%BC%D1%8F_%D0%BD%D0%B0_%D0%A3%D0%BA%D1%80%D0%B0%D0%B8%D0%BD%D0%B5#Попытка_отмены_сезонного_перевода_часов)
Тогда как для Ростова-на-Дону UTC+4:
(http://ru.timeofdate.com/city/Russia/Rostov-on-Don/timezone/change?start=2010)
Приводим одну из дат к часовому поясу другой. 31 декабря 2011 года, 23 часа, 00 минут, 00 секунд в Ростове-на-Дону это 31 декабря 2011 года, 21 часа, 00 минут, 00 секунд в Донецке.
Разница дат равна 4 часам. Это будет искомый ответ, если его удастся перевести в секунды и если верно сделанное нами допущение.

     2019/01/02 14:32, Автор сайта          # 

Не знаю, как была решена проблема с 31 ноября. То ли базу данных переделали, то ли законодательство подправили. А задачку зря вы решали. Она ведь была не для Вас.

     2019/01/09 10:14, utkin          # 

31 декабря 2011 года из Ростова-на-Дону вышел поезд, когда часы на вокзале показывали 23 часа, 00 минут, 00 секунд. Когда он пришёл в Донецк 1 января 2012 года, то часы на донецком вокзале показывали 01 час, 00 минут, 00 секунд. Вопрос: сколько секунд был в пути этот поезд?

Для этого давно стандартно используют пересчёт в одни единицы измерения. Это стандартная школьная задача (не с поездами, а пересчёт в единую систему координат). У поезда Московское время. И на вокзалах также. Поэтому проблема, которую Вы описали не существует. Просто пересчитываете время туды-сюды и всё.

Не знаю, как была решена проблема с 31 ноября.

А решать её следует специальным внутренним документом — исправление ошибки. То есть ответственный специалист получает документы такого рода, убеждается, что имеется ошибка и составляет специальный электронный (и бумажный, раз уже без бюрократии никуда) документ, в котором будет исправляться данная ошибка методами специалиста. А уж как он решит — это его проблема, может он затребует сведения о прошлых паспортах или вообще свидетельство о рождении (например, у человека, у которого возникла проблема). И всё. Вопрос исчерпан. А проблема здесь в проекте системы. Люди посчитали, что система безупречна и не предусмотрели возможность исправления ошибки. А если читали бы программную инженерию, то знали, что в больших системах с большим участием людей невозможно работать без ошибок. И поэтому обязательно должна быть подсистема для их исправления. Так что претензия тут вообще не к типам данных, а вообще к организации процессов взаимодействия и недостаточным погружением в предметную область проектировщиков.

     2019/01/10 11:41, Автор сайта          # 

Спорить я с Вами не буду, хотя логика Ваших рассуждений небезупречна. Главный посыл статьи — «формальные методы дают формальные же результаты». Тему неправильных ТЗ тут рассмотрели со многих сторон. А вот формальные методы борьбы за правильность — нет, к сожалению. А стоило бы. Вот цитата с форума:

У функциональной парадигмы есть одно преимущество, о котором не все догадываются... Дело в том, что так уж сложилось, что никто не требует доказательства правильности программы. Обычно ограничиваются парой тестов. Работает? Ну так что же вам ещё? Хотя понятно, что даже 1000 верных тестов не доказывает, что 1001-й тест будет верным. Представьте, что я предлагаю некую физическую формулу (расчета тока, потока тепла, энергии — чего угодно), а в качестве доказательства говорю: «Вот я проверил и на этих данных, и на этих — все верно. Значит формула верна для всех данных». Понятно, что в науке меня просто засмеют. Но в программировании это — нормальная ситуация.

Так вот: ФП позволяет смотреть на программу, как на теорему в математике. И математически доказывать её правильность. Конкретно это означает следующее. Вот код Паскале, который считает сумму элементов массива:

s:=0;
   for i:=1 to n do s:=s+X[i];

Попробуйте доказать, что код считает сумму n элементов любого массива. Это будет непросто. А вот тот же код на Haskell:

sum [] = 0
sum (x:sx)=x+sum(xs)

Здесь все готово для того, чтобы доказать по индукции, что функция sum вычислит сумму элементов любого списка s конечной длины.

Многие люди из нашего круга общения хотят написать компилятор Oberon-2, Lisp, C (с вариациями, с доработками). Но что-то никто не горит желанием написать свой Haskell, свою систему доказательного программирования. Увы.

А вот мне нравится доказуемость. С тех пор, как мне доказали теорему Пифагора, мне нравится доказывать. Хотя в вышеприведённом коде на Haskell
sum [] = 0
sum (x:sx)=x+sum(xs)
с доказанной правильностью («функция sum вычислит сумму элементов любого списка s конечной длины») я укажу на ошибку, из-за которой функция sum не всегда вычислит сумму не любого списка. Просто в этом коде на Haskell опять «сломалось» ТЗ и его надо подправить. И снова можно верить в доказательства.

     2019/01/10 12:45, utkin          # 

Спорить я с Вами не буду, хотя логика Ваших рассуждений небезупречна.

Естественно, это личное мнение, а оно всегда субъективно.

Дело в том, что так уж сложилось, что никто не требует доказательства правильности программы. Обычно ограничиваются парой тестов. Работает? Ну так что же вам ещё? Хотя понятно, что даже 1000 верных тестов не доказывает, что 1001-й тест будет верным.

На самом деле есть такое направление — верификация и валидация программного обеспечения (а также проекта, модели и пр.). И там такие вопросы рассматриваются. Если эта культура не свойственна нашим производственным предприятиям, ну извините, натягивать шаблон на всё тоже не стоит.

Так вот: ФП позволяет смотреть на программу, как на теорему в математике. И математически доказывать её правильность.

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

Попробуйте доказать, что код считает сумму n элементов любого массива. Это будет непросто. А вот тот же код на Haskell:

Это будет просто, потому что всегда можно провести эквивалентные преобразования к какому-нибудь абстрактному Haskell. Иными словами, при верификации той же программы на Паскале она транслируется в коды такого виртуального математического языка и далее всё следует аналогично. Так что проблем нет, было бы желание (подкрепленное большими деньгами).

Многие люди из нашего круга общения хотят написать компилятор Oberon-2, Lisp, C (с вариациями, с доработками). Но что-то никто не горит желанием написать свой Haskell, свою систему доказательного программирования. Увы.

Потому что очень высокий порог вхождения.

И снова можно верить в доказательства.

Игры в ребусы на Хаскелле это скорее его минус, чем плюс. Это все здорово при исследовании и творчестве и абсолютное зло при промышленном программировании.

     2019/01/11 11:58, Автор сайта          # 

верификация и валидация ... не свойственна нашим производственным предприятиям

Общество позволяет государство проводить беззубую экономическую политику, поэтому интересы потребителей не защищены от произвола «as is» («как есть»). Люди платят деньги за ПО, но никак не защищены. Вот появятся требования по качеству — тогда и будет внимание к доказательству правильности программ.

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

Это угрожает Вашей непорочности? :)

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

А зачем переводить на особый математический язык? Может, лучше сделать такой язык, чтобы он был удобен, понятен, общедоступен и при этом «математичен», чтобы проводить формальные проверки? «Два в одном»?

Потому что очень высокий порог вхождения

Так его надо понижать. Во-первых, отказаться и сказать «это слишком сложно» никогда не поздно. Во-вторых, сложность связана, зачастую, лишь с плохим изложением материала. Вот статья на подобную тему: «Проблемы современной записи математических текстов». Оттуда:

Первая проблема — значимость не показана. Ещё один подарок от Евклида: «Дай вопрошающему грош, если он ищет выгоды, а не математики». Авторы начинают вводить определения, доказывать теоремы и творить прочую математику без объяснения зачем оно вообще нужно. Пример: учебник по математическому анализу от Фихтенгольца. Почитайте первую главу: «из школьного курса вы знаете про рациональные числа, но потребности математики понуждают нас ввести вещественные...» и понеслась. Какие потребности, какой математики, чем не устраивают рациональные — да пёс его знает. «Очевидно».

     2019/01/12 07:22, utkin          # 

Общество позволяет государство проводить беззубую экономическую политику, поэтому интересы потребителей не защищены от произвола «as is» («как есть»). Люди платят деньги за ПО, но никак не защищены. Вот появятся требования по качеству — тогда и будет внимание к доказательству правильности программ.

Да есть такое. Мое мнение — в нашем государстве общество давно в заложниках и поэтому его никто не спрашивает уже давно.

Это угрожает Вашей непорочности? :)

У меня другие грехи :). Собственные.

А зачем переводить на особый математический язык? Может, лучше сделать такой язык, чтобы он был удобен, понятен, общедоступен и при этом «математичен», чтобы проводить формальные проверки? «Два в одном»?

Затем что матан сложен для человека. Язык математики не естественнен и поэтому даётся далеко не всем. Это же и проблема Хаскелла — простым людям сложно его понимать.

Так его надо понижать. Во-первых, отказаться и сказать «это слишком сложно» никогда не поздно. Во-вторых, сложность связана, зачастую, лишь с плохим изложением материала.

Не получается. Хаскелл есть давно, но он не лидер, почему? Что за это время не выпустили книг или они все так плохи? Нет, просто концепции, которыми он оперирует, далеки от повседневного использования.

Первая проблема — значимость не показана. Ещё один подарок от Евклида: «Дай вопрошающему грош, если он ищет выгоды, а не математики». Авторы начинают вводить определения, доказывать теоремы и творить прочую математику без объяснения зачем оно вообще нужно. Пример: учебник по математическому анализу от Фихтенгольца. Почитайте первую главу: «из школьного курса вы знаете про рациональные числа, но потребности математики понуждают нас ввести вещественные...» и понеслась. Какие потребности, какой математики, чем не устраивают рациональные — да пёс его знает. «Очевидно».

Это уже давно не так. Почитайте, что такое витагенные технологии образования. Там вот прямо в младших класса учитель излагает материал именно на окружающих ученика предметах. Учебнику Фихтенгольца уже куча лет. Сейчас там в школьную математику введены элементы теории вероятности (в моё время точно не было). Объяснить её не на предметах в младших классах просто невозможно.

     2019/01/12 11:23, Автор сайта          # 

И всё-таки, я думаю, стоит побороться за снижения порога вхождения. А вдруг родятся витагенные технологии в доказательном программировании?

     2019/01/14 07:23, utkin          # 

И всё-таки, я думаю, стоит побороться за снижения порога вхождения. А вдруг родятся витагенные технологии в доказательном программировании?

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

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

Просто Вам для примера — операция сложения.
plus = λx. λy. λs. λz. x s (y s z)
Классно, да?

     2019/01/15 15:40, Автор сайта          # 

Сомневаетесь — ради бога. Пессимисты плачутся в жилетку, оптимисты плачутся в декольте. Тут дело не только в доказательном программировании, но и в статических анализаторах кода. Уж они-то точно получили место под солнцем. Императивный код сложнее анализировать.

Я что-то не слышал о конкуренции форм записи среди математиков. Вот они и привносят свой язык с формой записи, ещё помнящей Ньютона, в функциональное программирование. Просто нужно думать и придумывать. Но Вас к этому не призываю :)

     2019/01/16 07:18, utkin          # 

Императивный код сложнее анализировать.

Может быть всё дело в том, что его пишут не для анализа, а для исполнения? А математики свои закорючки пишут как раз для того, чтобы проводить анализ.

Я что-то не слышал о конкуренции форм записи среди математиков.

А я слышал, например, римские цифры и арабские цифры. Было такое? Было.

Просто нужно думать и придумывать.

Я Вам верю, но эра одиночек в гаражах уже прошла. Есть целые кафедры функциональных языков в уважаемых институтах, которые думают, думают и никак не придумают. У всех использовавших функциональные языки очень приятные воспоминания о них. Проблема в том, что только воспоминания. И функциональные примочки хороши только на бумаге. На практике их использование приводит к жестким проблемам, о которых стараются не говорить. И Вы их тоже избегаете. Я Вам дам простой вопрос — как описать мир с побочными эффектами языком без побочных эффектов? Вот повесили Хаскелл на знамя — надо думать и придумывать. Так придумайте! Почему Хаскелл не на первом месте среди языков, ведь он так крут? А может потому, что в нём проблем дофига?

     2019/01/16 15:36, Автор сайта          # 

например, римские цифры и арабские цифры.

И всё? А языков программирования что-то около восьми тысяч. Это цифра, где-то озвученная несколько лет назад. Восемь тысяч форм записи! На три порядка больше, чем в математике. Просто математика сосредоточена на содержании, а не на форме. Просто перенос математики в язык программирования надо попытаться сделать с большим уважением к форме. С большим дружелюбием.

эра одиночек в гаражах уже прошла

Мои порывы не связаны с тем, что я бензина нанюхался.

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

Я несколько лет ломал голову над тем, как возвратить из функции объект переменной длины. В итоге нашёл решение, которое очень просто в реализации. А ведь сколько кафедр и институтов 70 лет ходило мимо, его не замечая. А теперь некоторые сотрудники РАН, которые в курсе, отдают должное. А Вы поищите в литературе, какие модели памяти знает наука — и моего новшества там не найдёте.

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

На практике их использование приводит к жестким проблемам, о которых стараются не говорить. И Вы их тоже избегаете. Я Вам дам простой вопрос — как описать мир с побочными эффектами языком без побочных эффектов?

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

     2019/01/17 14:05, utkin          # 

И всё? А языков программирования что-то около восьми тысяч. Это цифра, где-то озвученная несколько лет назад. Восемь тысяч форм записи! На три порядка больше, чем в математике. Просто математика сосредоточена на содержании, а не на форме.

Нет, не всё. На вики есть статья об истории математической записи. Я просто сказал о первой ассоциации. Второе — математика развивалась гораздо раньше и не имела такого опыта, как языки, которым нет и столетия. Поэтому пренебрежительное сравнение тут не корректно. Третье: Вы снова пытаетесь не видеть проблему. Математика сосредоточена на АНАЛИЗЕ записи. Программирование сосредоточено на ВЫПОЛНЕНИЕ полезной работы электронными устройствами. Не пытайтесь сравнить мягкое и сиреневое.

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

Было это уже, называется язык программирования APL. Не нужно пытаться наступать на те же грабли.

Мои порывы не связаны с тем, что я бензина нанюхался.

Я имел ввиду более приятные ассоциации — Б. Гейтса и С. Джобса.

А ведь сколько кафедр и институтов 70 лет ходило мимо, его не замечая.

Значит это не такая важная проблема на фоне других проблем.

Но я ведь и не претендую на ваше личное время. От Вас ничего не убудет.

Убывает время, которое я трачу, читая Ваши выкладки. При этом процесс не завершен и не факт, что будет завершен. Но я не жалуюсь :). Я получаю взамен пищу для размышлений. Так что, мне кажется, сделка честная.

Проблема в том, что общая картина не столь непонятна, сколь противоречива.

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

     2019/01/17 17:43, Автор сайта          # 

Я имел ввиду более приятные ассоциации

Прекрасно понял, кого и что Вы имели в виду. Отечественная традиция не окружает гаражи таким ореолом романтики :)

Значит это не такая важная проблема на фоне других проблем.

Да, настолько неважная, что в Haskell объекты по сей день создаются в «куче», хотя есть способы побыстрее. Плачем, тормозим, произносим заклинания «наши программы быстры, как никогда», но всё равно едим кактусы.

Убывает время, которое я трачу, читая Ваши выкладки ... сделка честная.

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

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

У Вас очень оригинальный угол.

     2019/01/18 08:54, utkin          # 

Да, настолько неважная, что в Haskell объекты по сей день создаются в «куче», хотя есть способы побыстрее.

В Хаскелле есть проблемы по важней. Первая — высокий порог вхождения. Вторая — пляски вокруг побочных эффектов.

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

Так это не Ваша главная цель. Ваша главная цель, как я понял, спроектировать и создать язык. А, все остальное делается ради этого, а не ради бесед со мной.

У Вас очень оригинальный угол.

Потому что других ходов там нет. Вы же хотите чистую математику. Разница между ней и императивом в том, что, во-первых, в императиве есть нарратив, а, во-вторых, мир не Вы описали своими закорючками, а кто-то другой. И, соответственно, все множество объектов и правил их взаимодействия Вам не известны. Чего не может быть в математике. Если, например, строил свою геометрию, то там и объекты множества, и весь доступный операционный класс. Нет в арифметике неизвестного действия. И хуже того, каждое действие ГАРАНТИРОВАННО дает предсказуемый результат. Даже деление на нуль в арифметике каждый раз гарантированно даёт Вам какую-то хрень. А вот в программировании это всё совсем не факт.

     2019/01/18 13:53, Автор сайта          # 

Понимаете, это не я хочу математику. Это она заставит нас преодолевать повышенный порог вхождения. Резервов в развитии программирования немного, и ФП — один из них. И если мафия бессмертна и непобедима ФП неизбежно, то этот процесс надо возглавить.

Пляски вокруг побочных эффектов есть — это как раз в императивных языках. В Haskell — другие пляски, вокруг кода. Надо сказать, что Clean мне нравится больше. Но для пользы дела неплохо бы изучить оба. Не столько с позиции программиста-пользователя, сколько с позиции разработчика языка и компилятора.

Насчёт гарантий результата скоро будет статья.

     2019/01/18 14:23, MihalNik          # 

В Хаскелле есть проблемы по важней. Первая — высокий порог вхождения. Вторая — пляски вокруг побочных эффектов.

Хаскелл их решать не собирается.

1) Привычка кушать кактусы. Аналогично некоторые люди готовят блюда из довольно опасных продуктов, например, ядовитых рыб. И да, научно обосновано, что это можно cделать безопасно, но высокий порог вхождения.

2) Неверное соотнесение задач и средств решения. Задачи, для которых подходит Хаскелл, во-первых, встречаются на практике не часто, во-вторых решаются более простыми средствами. Например, на Прологе и разных других языках/специализированных системах вывода доказательств по правилам (есть библиотеки на многих). Т.е. Хаскелл для своих задач ни разу ни уникален и уж тем более принятая в нём форма записи не является необходимым условием решения, зато очень своеобразна.

А ещё люди очень любят говорить о сложных вещах, в которых мало кто разбирается, даже не потрудившись разобраться в более простых. Соответственно, их высказывания редко подвергаются доказательствам и проверкам. Отсюда возникает подозрение, что доля разных недоказанных (и неверных среди них) утверждений программистов о языке Хаскелл намного выше доли таковых о более простых и распространённых языках. Проверка корректности императивных программ в основном сводится к простым неравенствам и логическим выражениям. Т.е. на уровне логики обычных школьников и студентов. Самое слабое звено в проверки корректности — сами люди. Поэтому там, где это критично, берутся более простые и легче проверяемые стандартизированные алгоритмы с увеличением вычислительных ресурсов, а не пытаются загружать память и ядра на 99%.

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

Так делается в Оберонах. Цена выражается в конечных процентах потери вычислительной производительности и минимизации функциональности, но расширение функций программ/ОС само по себе представляет разные угрозы, так что минимализм там ставится как задача. Тыкнуть случайно в хромобраузере андроида на смартах из коробки куда-нибудь не туда и уже устанавливаются неизвестные приложения/иконки, соответственно, закладки/дыры/управляемость под вопросом.

     2019/01/18 14:48, MihalNik          # 

Пляски вокруг побочных эффектов есть — это как раз в императивных языках. В Haskell — другие пляски, вокруг кода

Это всего лишь игра слов.

Попробуйте доказать, что код считает сумму n элементов любого массива. Это будет непросто. А вот тот же код на Haskell
sum [] = 0
sum (x:sx)=x+sum(xs)

Который есть просто мусор для программиста в промышленности. Потому что инженер смотрит на ограничения по типам данным, количеству элементов и вычислительных ресурсов. А в указанном коде ничего этого нет. Значит, задачу инженера он не решит.

с доказанной правильностью («функция sum вычислит сумму элементов любого списка s конечной длины») я укажу на ошибку, из-за которой функция sum не всегда вычислит сумму не любого списка. Просто в этом коде на Haskell опять «сломалось» ТЗ и его надо подправить. И снова можно верить в доказательства.

Укажите на ошибку и получится решение какой-то совершенно другой задачи, а не исходно вырванной из контекста. Потому что в Хаскелле предполагалось действие каких-то аксиом, а у Вас они нарушатся. Если написать что-то вроде:
var
s: LongInt;
e: Word;
A: array[1..1000] of Word;
procedure CalculateSum;
begin
s:= 0;
for e in A do s+= e;
end;
Корректность/некорректность кода можно объяснить даже школьнику, потому что там простые арифметические действия и неравенства. И это-то как раз будет очень просто. Заменяем Word на Longint и подпрограмма в принципе вне контекста становится непроверяемой никакой математикой. И эта локальная проверяемость/непроверяемость также легко объяснима. Так что проблема не в Хаскелле и не в императивных языках, а в желаниях усидеть на двух стульях. Например, быстрота и безопасность.

     2019/01/18 15:59, Автор сайта          # 

Укажите на ошибку

Указываю. Вышеприведённый пример имеет недостаток: он с большим доверием относится ко входным данным и не предполагает, что при суммировании возникнет переполнение. А где обработка переполнения? А нет её.

Вы в своём примере подстраховались тем, что элементы имеют тип Word, а сумма — LongInt. А вы исправьте так, чтобы обоих случаях был одинаковый тип и вставьте в код проверку ошибок. Тогда будет ясно, как ваш язык обрабатывает ошибки.

Стремиться же изменить Ваше мнение о Haskell, не собираюсь. Тем более я не его фанат и меня он самого местами просто бесит.

     2019/01/18 19:21, utkin          # 

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

Да в каком это месте? Она локализована строго в библиотеках и в самом приложении самая распространенная математика это +1. Деление есть не в каждой программе. Так что тут вопрос весьма спорный.

Резервов в развитии программирования немного, и ФП — один из них.

Это вряд ли. Лисп же чуть ли не первый дедушка на деревне.

Пляски вокруг побочных эффектов есть — это как раз в императивных языках.

Да в каком это месте? В половине языков так вопрос даже не стоит. Куча программистов вообще не знают, что такое побочный эффект и не парятся.

Тыкнуть случайно в хромобраузере андроида на смартах из коробки куда-нибудь не туда и уже устанавливаются неизвестные приложения/иконки, соответственно, закладки/дыры/управляемость под вопросом.

А в моем китайце установить что-то можно только с гугл плея :). Вшито в систему и абзац. Опция доверять источникам есть, но она не рабочая.

Указываю. Вышеприведённый пример имеет недостаток: он с большим доверием относится ко входным данным и не предполагает, что при суммировании возникнет переполнение. А где обработка переполнения? А нет её.

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

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

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

А зачем? Ну увидите Вы блок try-except. И что Вам это даст? Не понял я тут хода Ваших мыслей...

     2019/01/19 00:52, MihalNik          # 

А вы исправьте так, чтобы обоих случаях был одинаковый тип и вставьте в код проверку ошибок.

Одинаковый тип — это и есть ошибка. Точнее говоря, ошибка в приравнивании понятия одинакового типа к понятию одинакового размера. Потому что сделает код непроверяемым вне контекста. Речь то как раз об этом. Безопасность, например, достигается использованием локально верифицируруемых подпрограмм. А проверка ошибки лежит где-то извне, её нельзя впихнуть внутрь подпрограммы по определению — там просто нет необходимых данных. Одинаковая размерность слагаемых и результата математически записывается вот как:
var a,b,c: Byte;
begin
a:= (b+c) mod 256;
end;
Переполнения нет — это иллюзия, навязываемая формой записи, которая позволяет опускать "mod 256", а точнее записывать знаком "+" совершенно разные действия. Т.е. знак вроде бы один, но операции — разные, по виду совершенно неочевидные. Нужно смотреть определения типов переменных, порядок выполнения операций и соглашения для типов получаемых результов в зависимости от операндов. Аналогично вот эта запись:
if (a=b) c+= 1;
Рождает иллюзию проверки на равенство. Это не проблема императивного программирования. Это проблема нарушения стандартизации.

     2019/01/19 07:29, utkin          # 

Вообще раз уже пошла такая пьянка, то мне непонятны претензии к сложению двух байтов. Это вообще-то не математическая операция. Потому что в математике как мы знаем складывают абстракции. И с таких позиций пример кода на Хаскелле был абсолютно корректен. Потому что 2 + 2 = 4. Это 2 яблока + две груши = 4 фрукта и отсюда проблемы типа фрукты это не яблоки. При работе с абстракциями там все правильно в коде было. Просто автор сайта начал на математику натягивать ограничения системы (а это уже не математика) и тут обнаружил вдруг то, что и так всем давно известно.

Указываю. Вышеприведённый пример имеет недостаток: он с большим доверием относится ко входным данным и не предполагает, что при суммировании возникнет переполнение. А где обработка переполнения? А нет её.

А где в математике работа с переполнениями? У множества всяких типов чисел (натуральные, там рациональные, комплексные и т.д.) домен значений не определен нигде. Тут либо крестик снять надо, либо трусы надеть. Либо работать с математикой, либо программировать систему с побочными эффектами и ограниченной в ресурсах.

     2019/01/20 18:12, Автор сайта          # 

Одинаковый тип — это и есть ошибка.

Ошибка, говорите? Да она в стандартах языков зафиксирована! В C++, например, вот так:
int operator+=(int& a1, int a2)
Везде тип одинаковый. А вот операции
int operator+=(int& a1, short a2)
не существует, хотя, по Вашей логике, именно её правильно применять. Да и Ваш пример с
A: array[1..1000] of Word;
легко сломать, увеличив количество элементов в массиве. Ладно, дискуссия давно пора прекращать. Даю ссылку на новую статью: «Обработка ошибок».

     2019/01/20 19:04, utkin          # 

Ошибка, говорите? Да она в стандартах языков зафиксирована! В C++, например, вот так:

Дык, там же и предусмотрено её решение путем генерации исключения в случае переполнения.

легко сломать, увеличив количество элементов в массиве.

Да, но зачем? Можно тупо делить на нуль первым оператором в программе. Вы пытаетесь автоматически ловить логические ошибки. Но в этом и есть проблема современности — что НЕТ ГРАНИЦЫ между алгоритмом и логической ошибкой. Какие-то проблемы верифицируемы(математически или в результате приобретенного опыта), а какие-то нет.

     2019/01/21 11:53, Автор сайта          # 

Современность работает над как можно большим контролем кода. К примеру, при сравнении объектов между собой встречаются случаи, когда объект сравнивается сам с собой. Статические анализаторы кода типа PVS Studio это отлавливают. Но этот анализатор имеет потолок, определяемый архитектурой языка. Потолок можно поднять, поменяв архитектуру языка. Но всегда можно сказать: «Вы всё равно всё не проверите, а раз так, то и вообще ничего не надо проверять». Вы, похоже, именно этой точки зрения и придерживаетесь. Ничего не имею против. Но Вам обязательно нужно было донести свою точку зрения? Именно здесь?

     2019/01/21 13:11, utkin          # 

Современность работает над как можно большим контролем кода.

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

Но Вам обязательно нужно было донести свою точку зрения?

Я пытаюсь понять суть Ваших идей. Анализировать новое, то чего ещё нет, можно самым простым способом. Сравнивать с имеющимися решениями. Если Ваши решения не удовлетворительны, есть два варианта:
1. Вы не можете грамотно объяснить суть идеи. Тут проблема может быть лично в Вас. То есть идея может быть гениальна и решать все проблемы. Но Вы не можете её раскрыть так, чтобы не возникало вопросов.
2. Идея не удачна и не дает преимуществ перед имеющимися решениями.

     2019/07/20 19:42, Александр Коновалов aka Маздайщик          # 

sum [] = 0
sum (x:sx)=x+sum(xs)

Указываю. Вышеприведённый пример имеет недостаток: он с большим доверием относится ко входным данным и не предполагает, что при суммировании возникнет переполнение. А где обработка переполнения? А нет её.

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

А с точки зрения Хаскеля (и любого другого языка, не только функционального) этот код имеет другой недостаток. Вызов sum в нём не хвостовой, а значит, для вычисления суммы нужна рекурсия глубиной размером с длину списка. Стек интерпретатора может находиться в куче, так что программа может не вылететь с переполнением стека. Но с точки зрения быстродействия это всё равно хуже, чем цикл/хвостовая рекурсия.

Есть ли в Хаскеле типы для целых чисел ограниченной разрядности? Вроде есть, ведь они нужны для интерфейса с языком Си. Как с ними реализована арифметика и что в этом случае происходит с переполнением? Понятия не имею. По идее, программисты на Хаскеле должны ими пользоваться только для взаимодействия с библиотеками на Си, в обычной практике они должны предпочитать «безграничные» натуральные числа.

Добавить свой отзыв

Написать автору можно на электронную почту mail(аt)compiler.su

Авторизация

Регистрация

Выслать пароль

Карта сайта


Содержание

Каким должен быть язык программирования?

Анализ и критика

Описание языка

Компилятор

Отечественные разработки

Cтатьи на компьютерные темы

●  Двадцать тысяч строк кода, которые потрясут мир?

●  Почему владение/заимствование в Rust такое сложное?

●  Масштабируемые архитектуры программ

●  Почему Хаскелл так мало используется в отрасли?

●  Программирование исчезнет. Будет дрессировка нейронных сетей

●  Бесплатный софт в мышеловке

●  Исповедь правового нигилиста

●  Русской операционной системой должна стать ReactOS

●  Почему обречён язык Форт

●  Программирование без программистов — это медицина без врачей

●  Электроника без электронщиков

●  Программисты-профессионалы и программирующие инженеры

●  Статьи Дмитрия Караваева

●●  Идеальный транслятор

●●  В защиту PL/1

●●  К вопросу о совершенствовании языка программирования

●●  О реализации метода оптимизации при компиляции

●●  О реализации метода распределения регистров при компиляции

●●  О распределении памяти при выполнении теста Кнута

●●  Опыты со стеком или «чемпионат по выполнению теста Кнута»

●●  О размещении переменных в стеке

●●  Сколько проходов должно быть у транслятора?

●●  Чтение лексем

●●  Экстракоды при синтезе программ

●●  Об исключенных командах или за что «списали» инструкцию INTO?

●●  Типы в инженерных задачах

●●  Непрерывное компилирование

●●  Об одной реализации специализированных операторов ввода-вывода

●●  Особенности реализации структурной обработки исключений в Win64

●●  О русском языке в программировании

●●  Формула расчета точности для умножения

●●  Права доступа к переменным

●●  Заметки о выходе из функции без значения и зеркальности get и put

●●  Модификация исполняемого кода как способ реализации массивов с изменяемыми границами

●●  Ошибка при отсутствии выполняемых действий

●●  Скорость в попугаях

●●  Крах операции «Инкогнито»

●●  Предопределённый результат

Компьютерный юмор

Новости и прочее




Последние отзывы

2019/11/09 21:27 ••• kt
Программирование без программистов — это медицина без врачей

2019/11/07 10:58 ••• kt
Признаки устаревшего языка

2019/10/28 23:55 ••• Автор сайта
Типы в инженерных задачах

2019/10/15 16:32 ••• kt
Модификация исполняемого кода как способ реализации массивов с изменяемыми границами

2019/10/07 14:15 ••• Автор сайта
О наименовании проекта и языка программирования

2019/09/19 15:23 ••• kt
Некошерный «goto»

2019/09/13 16:38 ••• Автор сайта
Программирование исчезнет. Будет дрессировка нейронных сетей

2019/09/12 20:40 ••• Александр Коновалов aka Маздайщик
Циклы

2019/08/30 07:57 ••• Noname
Почему обречён язык Форт

2019/08/29 09:07 ••• рст256
Устарел ли текст как форма представления программы

2019/08/19 19:19 ••• Автор сайта
Шестнадцатиричные и двоичные константы

2019/07/30 14:06 ••• Александр Коновалов aka Маздайщик
К вопросу о совершенствовании языка программирования