Программа без ошибок - такая же абстракция, как -273 градуса

[незваный гость]

kpierre писал(а):

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

Да речь-то не о том, доказывается ли это компилятором. А о том, что это доказать можно. То есть о том, что Ваш пример — слабый.

kpierre писал(а):

Никакой "контрол календаря" меня совершенно не интересует. А уж windows -- тем более.

То есть, Вас не интересуют практические применения. Забавно. А я считал всегда, что целью написания програм является решение практических задач. У Вас, по-видимому, не так.

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

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

kpierre писал(а):

Такого компилятора нет, зато есть инструменты, позволяющие формально описывать многие встроенные системы вплоть до fpga и доказывать их корректность. И никто не собирается сами эти инструменты запускать на целевых системах.

А это и не надо. Равно как и не надо путать Божий дар с яичницей. fpga — это совсем из другой оперы. А чтобы опровергнуть сказанное мной, приведите пример систем формального описания для таких таргетов, как PowerPC, ColdFire или Intel. А не говорите мне о чудесном урожае бузины в огороде.

kpierre писал(а):

Вот именно, что она только кажется строгой, на самом деле она там почти отсутствует

Докажите, что типизация в Алгол-68 нестрогая. Или приведите ссылки на доказательство.

kpierre писал(а):

Доказательства корректности исходного кода этой системы, к примеру -- http://coq.inria.fr/ -- были произведены вручную.

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

[kpierre]

незваный гость писал(а):

:evil:

kpierre писал(а):

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

Да речь-то не о том, доказывается ли это компилятором. А о том, что это доказать можно. То есть о том, что Ваш пример — слабый.

Что-то я не понимаю. Доказать можно, но сложно. В случае соответствующей программы на соотв. языке доказывать нужно только его некоторое ядро, что и было проделано авторами Coq.

незваный гость писал(а):

То есть, Вас не интересуют практические применения. Забавно. А я считал всегда, что целью написания програм является решение практических задач. У Вас, по-видимому, не так.

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

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

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

незваный гость писал(а):

А это и не надо. Равно как и не надо путать Божий дар с яичницей. fpga — это совсем из другой оперы. А чтобы опровергнуть сказанное мной, приведите пример систем формального описания для таких таргетов, как PowerPC, ColdFire или Intel. А не говорите мне о чудесном урожае бузины в огороде.

http://proofos.sourceforge.net/doc/ -- вот, к примеру, для x86. Или еще: http://os.inf.tu-dresden.de/papers_ps/h ... diplom.pdf.

незваный гость писал(а):

Докажите, что типизация в Алгол-68 нестрогая. Или приведите ссылки на доказательство.

Нечего тут доказывать, т.к. "строгая" -- субъективное понятие. Уже в хаскеле типизация -- полноценная логика, так что по сравнению с ней типизация алгола не сильно строгая.

незваный гость писал(а):

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

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

[незваный гость]

kpierre писал(а):

Нечего тут доказывать, т.к. "строгая" -- субъективное понятие. Уже в хаскеле типизация -- полноценная логика, так что по сравнению с ней типизация алгола не сильно строгая.

А, так Вы субъективно обращаетесь не только с видами типизации, но и с языками. Между прочим, Вы первый, кто сказал мне, что в Алголе-68 нестрогая типизация из-за того, что в Хаскеле используется Hindley-Milner type system. Все остальные считают, что тип выражения в А-68 полностью определён операндами, и никакого вывода не требуется. (т.е., если в Haskell тип 2+3 выводится (inferred), то в А-68 он однозначно определён: int). Неудобно, конечно, но тоже ничего, вполне строго.

Кстати, А-68 реализует так называемую именную типизацию, т.е. два типа равны тогда и только тогда, когда они имеют одно и тоже имя (квалифицированное в контексте). Что делает сравнение сигнатур тривиальной задачей.

А подводя итог, раз нечего доказывать, то и трепаться нечего. Общепринятое мнение, что типизация в Алголе-68 строгая.

kpierre писал(а):

А зачем вылезать за пределы их фреймворка? Для того фреймворк и есть, чтобы за него не вылезали.

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

kpierre писал(а):

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

Есть люди, которые с Вами не согласятся, например В.И.Арнольд. Сводить Computer Science к прикладным задачам глупо, но цель (и движущая сила) CS — это прикладные задачи.

И, между прочим, недостойных прикладных задач не бывает. А что касается тормозов, то я рад услышать Ваше мнение, как Вы будете писать систему управления. Начиная с работы с оборудованием и кончая интерфейсом с системами более высокого уровня. Как уже упоминалось, требования примерно таковы: 24 канала (с фиксированным сдвигом в 12.8 мкс), предельное отклонение начала чтения 1 мкс (иначе резко падает точность измерения), частота опроса 700 мкс, тактовая частота процессора 20 МГц (Motorola mpc555), архитектура PowerPC. По каждому из каналов следует определить амплитуду и фазу сигнала, плюс для двух определяемых конфинурацией — частоту. Ах да, забыл. Ещё 32 дискретных канал (с устранением дребезга). С чего начнёте? С написания своего планировщика, или с построения интерфейса к ОС РВ? Задачу я диктую по памяти, но я её успешно решил на С++ (ОС — Enea OSE). Пока жалоб на ошибки не поступало.

kpierre писал(а):

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

Я всё пытаюсь Вам объяснить, что Ваш пример сродни утверждения, что болид Формулы-1 можно разогнать до 60 км/ч. Я верю, поскольку могу это сделать на своём стареньком запорожце (если собаки не испугается). Но преимущества болида перед запором совсем другие. А о них Вы не говорите вообще.

[kpierre]

незваный гость писал(а):

kpierre писал(а):

А зачем вылезать за пределы их фреймворка? Для того фреймворк и есть, чтобы за него не вылезали.

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

Аргумент у вас просто убийственный. Значит, по-вашему, любой фреймворк/яп не достоин использования, т.к. "большинство задач вырастают". Я вам вот что скажу -- для почти любого класса задач существуют свои общие решения, иначе не было бы никогда даже яп. Для задач верификации современные инструменты я вам привел.

незваный гость писал(а):

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

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

незваный гость писал(а):

А что касается тормозов, то я рад услышать Ваше мнение, как Вы будете писать систему управления. Начиная с работы с оборудованием и кончая интерфейсом с системами более высокого уровня. Как уже упоминалось, требования примерно таковы: 24 канала (с фиксированным сдвигом в 12.8 мкс), предельное отклонение начала чтения 1 мкс (иначе резко падает точность измерения), частота опроса 700 мкс, тактовая частота процессора 20 МГц (Motorola mpc555), архитектура PowerPC. По каждому из каналов следует определить амплитуду и фазу сигнала, плюс для двух определяемых конфинурацией — частоту. Ах да, забыл. Ещё 32 дискретных канал (с устранением дребезга). С чего начнёте? С написания своего планировщика, или с построения интерфейса к ОС РВ? Задачу я диктую по памяти, но я её успешно решил на С++ (ОС — Enea OSE). Пока жалоб на ошибки не поступало.

Я ее писать не буду, т.к. это моей специализацией нисколько не является. Спрошу лишь: произведена ли вами верификация вашей программы? Если нет, то какое это имеет отношение к делу? Повторю, верификация никогда бесплатной не будет, зато сейчас она стоит сравнительно мало.

незваный гость писал(а):

kpierre писал(а):

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

Я всё пытаюсь Вам объяснить, что Ваш пример сродни утверждения, что болид Формулы-1 можно разогнать до 60 км/ч. Я верю, поскольку могу это сделать на своём стареньком запорожце (если собаки не испугается). Но преимущества болида перед запором совсем другие. А о них Вы не говорите вообще.

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

Добавлено спустя 10 минут 5 секунд:

Цитата:

А, так Вы субъективно обращаетесь не только с видами типизации, но и с языками. Между прочим, Вы первый, кто сказал мне, что в Алголе-68 нестрогая типизация из-за того, что в Хаскеле используется Hindley-Milner type system. Все остальные считают, что тип выражения в А-68 полностью определён операндами, и никакого вывода не требуется. (т.е., если в Haskell тип 2+3 выводится (inferred), то в А-68 он однозначно определён: int). Неудобно, конечно, но тоже ничего, вполне строго.

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

[незваный гость]

kpierre в сообщении #130824 писал(а):

Значит, по-вашему, любой фреймворк/яп не достоин использования, т.к. "большинство задач вырастают".

Отчего же. Очень даже достойны: они сокращают время программирования. Но, в отличие от штанишек, большинство систем программироваяния обладают одной важной особенностью: незамкнутостью. Т.е., если мне не хватает библиотеки С++ (или .NET), я могу просто вызвать функцию Windows API. Вот и приведите пример того, что думает по этому поводу система верификации.

kpierre в сообщении #130824 писал(а):

Спрошу лишь: произведена ли вами верификация вашей программы? Если нет, то какое это имеет отношение к делу?

Не произведена. Поскольку мне не известна система автоматической верификации, пригодная для этого проекта. А ручная cost-prohibitive.

Какое это имеет отношение к вопросу? Прямое -- мне безразлична цена заморских телушек, пока не упадут транспортные расходы. Хотя я верю, что полушка, и это вселяет надежду, что и у нас говядина и молоко подешевеют. Со временем.

kpierre в сообщении #130824 писал(а):

Вы про то, что верификация -- это Ф1, которой нигде кроме сухой теории не воспользуешься?

Я про то, что Ваш пример плох. Верификация может куда больше, чем Ваш пример показывает.

kpierre в сообщении #130824 писал(а):

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

Про это я совсем не понял.

Я в первый раз слышу, чтобы количество информации в типах рассматривалось как мера строгости типизации.

Кстати, недурно было бы пример в студию: пример того, как в Хаскеле тип несёт больше информации, чем в Алгол-68.

[e2e4]

незваный гость писал(а):

И, между прочим, недостойных прикладных задач не бывает. А что касается тормозов, то я рад услышать Ваше мнение, как Вы будете писать систему управления. Начиная с работы с оборудованием и кончая интерфейсом с системами более высокого уровня. Как уже упоминалось, требования примерно таковы: 24 канала (с фиксированным сдвигом в 12.8 мкс), предельное отклонение начала чтения 1 мкс (иначе резко падает точность измерения), частота опроса 700 мкс, тактовая частота процессора 20 МГц (Motorola mpc555), архитектура PowerPC. По каждому из каналов следует определить амплитуду и фазу сигнала, плюс для двух определяемых конфинурацией — частоту. Ах да, забыл. Ещё 32 дискретных канал (с устранением дребезга). С чего начнёте? С написания своего планировщика, или с построения интерфейса к ОС РВ? Задачу я диктую по памяти, но я её успешно решил на С++ (ОС — Enea OSE). Пока жалоб на ошибки не поступало.

Если не секрет, поделитесь как Вы определяли фазу и частоту сигнала? ДПФ или что-то другое?

[незваный гость]

e2e4 в сообщении #137242 писал(а):

Если не секрет, поделитесь как Вы определяли фазу и частоту сигнала? ДПФ или что-то другое?

Подробно рассказать не могу, но грубо так: поскольку частота сигнала примерно известна (50 Гц держат довольно точно), то можно сравнивать сигнал $S$ с эталоном $S_0$ (и подсчитать $S \times \bar{S_0}$). Тогда мы имеем фазу, а скорость вращения фазы позволяет уточнить частоту эталона. Дальше уже точно не мои секреты полишинеля.

[kpierre]

Цитата:

Отчего же. Очень даже достойны: они сокращают время программирования. Но, в отличие от штанишек, большинство систем программироваяния обладают одной важной особенностью: незамкнутостью. Т.е., если мне не хватает библиотеки С++ (или .NET), я могу просто вызвать функцию Windows API. Вот и приведите пример того, что думает по этому поводу система верификации.

Вы можете что угодно принять за аксиому и доказывать в другом месте. Или вобще не доказывать. Не понимаю, в чем может быть проблема. Если у вас есть алгоритм д-ва на другом языке -- конечно же, можно вызвать его (например, через ocaml+C FFI)

Цитата:

Я в первый раз слышу, чтобы количество информации в типах рассматривалось как мера строгости типизации.

Кстати, недурно было бы пример в студию: пример того, как в Хаскеле тип несёт больше информации, чем в Алгол-68.

Ну например, тип функции, фильтрующей эл-ты списка произвольного типа по предикату:

filter :: (a -> Bool) -> [a] -> [a]

Если мы хотим изобразить "функцию, фильтрующую по предикату списки, состоящие только из чисел", мы пишем:

filterNum :: Num a => (a -> Bool) -> [a] -> [a]

(важно, что информация здесь именно "произвольных чисел". Целые числа и дроби подойдут в равной мере).

Попробуйте изобразить подобные типы на Алголе.

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

[незваный гость]

kpierre в сообщении #137351 писал(а):

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

Мне трудно себе представить аксиоматически корректный Windows API. А если не доказывать, то зачем мне система верификации?! А в чём проблема — если Вы не сталкивались, спросите тех, кто пользовался WinAPI: почему их программы падают на чужом компе? почему их ломает очередной патч из Редмонда? …

kpierre в сообщении #137351 писал(а):

Если у вас есть алгоритм д-ва на другом языке -- конечно же, можно вызвать его (например, через ocaml+C FFI)

Бог с ней, с расширяемостью системы верификации. Мне фреймворк расширять надо, за счёт вызова внешних объектов.

Кажется, я начинаю понимать: меня интересует расширяемость кода, а Вы говорите о расширяемости метакода (системы верификации). Второе для меня вторично. Но давайте разберём пример, что бы расставить точки над t и чёрточки над i:

Я пишу (на привычном мне С) свою функцию:

void foo(void) {
...
}
Ежу понятно, что такому крутому парню, как я, стандартной библиотеки не хватает. Поэтому я и пишу:

extern int bar(int x, int y);

void foo(void) {
...
int ix = bar(1, 5);
…
}
Всё это проходит на ура, пока у меня нет системы верификации. Как только у меня она есть, мне становится необходимо высосать из пальца метадекларацию bar() для верификации (включая предусловие на вход, постусловие на выход и прочая, скажем, реентерабельность). Во-первых, это до хрена усилий. Во-вторых, где гарантия, что моя метадекларация корректна (соответствует описанию API). В-третьих, где гарантия, что эта реализация bar() соответствует метадекларации (я её не пишу, у меня и кода-то нет, один заголовок)?

Вот и получается, что выйти за пределы предоставляемой автором системы совсем не просто.

post scriptum к примеру: забудьте на время о типах. Я слишком легко могу себе представить программу, корректность которой зависит от того, возвращает ли int gcd(int, int) правильный наименьший общий делитель. Позвольте мне не напоминать Вам, что типы в этом случае будут не при чём.

kpierre в сообщении #137351 писал(а):

Ну например, тип функции, фильтрующей эл-ты списка произвольного типа по предикату:
…
Попробуйте изобразить подобные типы на Алголе.

А нельзя. Вообще нельзя. Нет там обобщённых типов. Соответственно, и функций таких написать нельзя, и проблемы с неточным указанием типа нет. Устарел язык, что поделаешь…

Но заметьте: Вы указали на отсутствие возможности в языке (недостаточность выразительных средств языка), а не на нестрогость системы типов. Так что я продолжаю ждать пример нестрогости типизации.

[kpierre]

Цитата:

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

Вот и получается, что выйти за пределы предоставляемой автором системы совсем не просто.

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

Цитата:

А нельзя. Вообще нельзя. Нет там обобщённых типов. Соответственно, и функций таких написать нельзя, и проблемы с неточным указанием типа нет. Устарел язык, что поделаешь…

Но заметьте: Вы указали на отсутствие возможности в языке (недостаточность выразительных средств языка), а не на нестрогость системы типов. Так что я продолжаю ждать пример нестрогости типизации.

Вот недостаточность выразительных средств и есть "нестрогость системы типов". Согласитесь, ваши слова применимы даже к динамически типизированным языкам -- у них-де нет выразительных средств для int и string, отсутствует возможность их различать

[незваный гость]

kpierre в сообщении #137440 писал(а):

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

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

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

kpierre в сообщении #137440 писал(а):

Вот недостаточность выразительных средств и есть "нестрогость системы типов". Согласитесь, ваши слова применимы даже к динамически типизированным языкам -- у них-де нет выразительных средств для int и string, отсутствует возможность их различать

Чушь. Полная. В языке ЯзНеГо (язык незваного гостя) есть только два типа данных — целое число и строка. Функции данными быть не могут. Все преобразования типов явные. Производных типов нет. Каждая переменная имеет точно описанный тип. Все функции и операторы имеют точно описанную сигнатуру (её не нужно смешивать с типом, поскольку они не значения). Перегрузка функций и операторов запрещена.

Выразительных средств маловато. Но типизация — строгая. Абсолютно строгая. Никакого смешения типов нет. Более того, все ошибки типов ловятся на момент компиляции.

Вы хотите, чтобы я нарисовал грамматику языка? Или сказанного достаточно?

PS: Есть большая разница между нельзя написать в языке и нельзя проверить. В А-68 нельзя написать универсальный фильтр списка. В динамическом языке фильтр пишется легко, но отсутствует контроль типа. В «современных» функциональных языках есть и то, и другое. Они мощнее А-68. Но это не делает систему типизации А-68 нестрогой. Как не делает ЛИСП нефункциональным языком.

[worm2]

незваный гость писал(а):

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

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

Добавлено спустя 5 минут 43 секунды:

kpierre, интересно было бы узнать Ваше мнение по поводу Total FP. Если, конечно, Вы интересуетесь этим направлением.

[незваный гость]

worm2 в сообщении #137489 писал(а):

kpierre, интересно было бы узнать Ваше мнение по поводу Total FP. Если, конечно, Вы интересуетесь этим направлением.

Эк Вы меня предупредили. А я вот собирался попросить верифицировать такую функцию:

long C(long n):
  return if n <= 1 then n elif odd(n) then C(3*n + 1) else C(n // 2)
.

где long — целый тип с произвольной точносью, а // — операция целочисленного деления, возвращающая целый результат.

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

Добавлено спустя 10 минут 48 секунд:

worm2 в сообщении #137489 писал(а):

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

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

Более того, некое подсознательное требование если и не доказательства, то по меньшей мере пригодности к доказательству, несомненно, оказывает влияние на моё проектирование и программирование постоянно. Так, когда я беру интеграл, я не доказываю каждый шаг, но постоянно слежу за (полу)корректностью преобразований. Тоже и здесь.

[kpierre]

Цитата:

kpierre, интересно было бы узнать Ваше мнение по поводу Total FP. Если, конечно, Вы интересуетесь этим направлением.

Total FP неразрывно связано с верификацией -- Coq (о котором я писал ранее) и Epigram, к примеру, total -- посему не тьюринг-полные. Без тотальности сильно сложнее доказывать корректность, к тому же без нее тяжело использовать зависимые типы -- а на них современные системы верификации и построены.

Я уверен, что это направление имеет большое будущее -- лишь бы только появился ЯП разумно сочетающий в себе total и не-total фп. Пока что мне такого видеть не довелось.

Добавлено спустя 38 минут 42 секунды:

Цитата:

Выразительных средств маловато. Но типизация — строгая. Абсолютно строгая. Никакого смешения типов нет. Более того, все ошибки типов ловятся на момент компиляции.

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

Цитата:

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

В этом я с вами вынужден согласиться

Цитата:

где long — целый тип с произвольной точносью, а // — операция целочисленного деления, возвращающая целый результат.

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

Ну разумеется любая доказательная система это вам не волшебство Почему вдруг "слабость"? Система верификации же, а не мозги

[незваный гость]

kpierre в сообщении #137501 писал(а):

Надеюсь, отрицать то, что смысл типов -- нести информацию, вы не будете.

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

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

kpierre в сообщении #137501 писал(а):

Почему вдруг "слабость"? Система верификации же, а не мозги

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

Не мозги… Конечно, не мозги. Если я не ошибаюсь, автоматическое доказательство правильности программы машины Тьюринга невозможно. Соответственно… Total FP может быть неплохим компромисом, особенно если удастся сделать практичный вариант.

kpierre в сообщении #137501 писал(а):

Ну, если вы совсем не хотите слышать от меня термин "мера строгости", я могу его не употреблять.

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

Например, я готов согласиться, что система типов А-68 проще («слабее» в смысле выразительности), чем система типов Haskel. Но это не делает её менее строгой: строгость типизации в А-68 образцово-показательная, в ущерб удобству использования.

~~~

Ну, и в заключение кину ещё один камень в огород систем верификации. Итак, система реального времени.

void foo(void) {
  t = time();
  …
  assert(time() < t + 10 ms);
}

Как будем это верифицировать? (Лучшее известное мне определение систем реального времени звучит примерно так: «РВ: это когда ответ, не данный вовремя — неправильный ответ».) Каким образом мы будем доказывать, что программе хватит ресурсов (процессора, памяти… да мало ли чего)? Можно ли без подобного анализа говорить о готовности систем верификации для этой области применения?

Добавлено спустя 6 минут 59 секунд:

P.S. Кстати, мои вопросы о смысле типа отнюдь не риторические. В традиционных языках говорят о типе значения и типе переменной. В ФЯ, как я понимаю, переменных нет. То есть, говорить можно (вроде бы) только о типе значений. Но не так ли поступают и язычники? Например, в Python типизация значений строгая. Это вот типизация переменных отсутствует.