Rust? Какой нафиг шраст-мраст, Эппол открывает Swift позже в этом году!

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

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

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

Для доказательства подобных теорем необходимо точно знать, какая часть глобального state досягаема из реализации и каким образом эта досягаемая часть мутирует. Rust с его ownership system / borrow checker в этом плане чрезвычайно интересен.

Эта задача, вообще говоря, неразрешима.

В общем случае доказательство лежит на плечах программиста. Чтобы такое программирование было хоть сколько-нибудь практичным, нужно:
1. напихать в компилятор эвристики и схемы доказательств для типовых случаев/ситуаций
2. реализовать язык подсказок, на котором программист будет указывать, какую именно из схем доказательств к каким именно точкам кода нужно приятнуть, чтобы солвер смог построить доказательство

Пока мы от этого удручающе далеки.

учите язык ада

напихать в компилятор эвристики и схемы доказательств для типовых случаев/ситуаций

Нечто вроде тактик, только намного мощнее.

учите язык ада

http://www.youtube.com/watch?v=8t8WEqg9tvE

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

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

учите язык ада

«Управление тепловыми установками, а так же полная автоматизация цикла варки грешников в кипящей смоле с помощью ПХП, 1С и VBA! Тринадцатая редакция.»

А кто будет проверять спецификацию тогда? Ведь она в данном случае не проще кода

Проще. За счет того, что спецификация описывает абстракцию, а не детали того, как абстракция реализована.

сам код является спецификацией

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

У меня сложилось прямо противоположное впечатление и от ооп теперь подташнивает.

гибкость

Как у осьминога. Только на суше без скелета туго совсем.

Проще.

Нет, не проще. Любая полная спецификация эквивалентна коду по определению.

Нет. По этой причине код нельзя использовать в качестве спецификации.

Это опровергается практикой - компиляторы используют код в качестве спецификации. Программисты используют код в качестве спецификации. Код является спецификацией.

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

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

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

Так что возвращаемся к исходному вопроса - как проверить корректность спецификации?

Ну, например, она должна быть непротиворечива.

Любая полная спецификация эквивалентна коду по определению.

В каком смысле «полная»? Пойди прочитай что-нибудь про инкапсуляцию.

Ну, например, она должна быть непротиворечива.

А дальше? Корректной она не станет от этого. Кто проверять на корректность будет?

В каком смысле «полная»?

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

Ну получится же.

А дальше?

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

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

Вообще-то нет. Непротиворечивость на вероятность ошибки никак не влияет.

в целом отличный язык между прочим

Говноязыки, в которых «0» == 0 == «» должны сдохнуть.

Сообщения обязательны, наследование - нет. В Lua нет наследования, а вот объекты есть. Про Haskell не глупостей, там есть классы.

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

Про Haskell не надо глупостей

self-fix

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

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

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

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

Сообщения обязательны, наследование - нет.

Ну, значит, Java — не ОО-язык.

там есть классы

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

Ты не понимаешь, что ООП может иметь различные формы? В Java, Smalltalk, Lisp (CLOS), Oberon, Lua и Haskell оно разное, но все эти языки - объектно-ориентированные.

Непротиворечивость на вероятность ошибки никак не влияет.

Разве? Если есть лишь одно условие, ему нечему противоречить. Если есть два условия, то первое может противоречить второму. Если три — первое может противоречить второму или третьему. Очевидно, с ростом условий резко растёт и количество возможных противоречий.

Ты не понимаешь, что ООП может иметь различные формы?

Но ты сказал «сообщения обязательны». В Java нет передачи сообщений.

Есть - посредством вызова методов, как и в C++.

Классы типов это совсем другое

Трейты не обязательно использовать в роли классов типов - можно в роли интерфейсов.

в прочих языках их зовут типажами

Нигде их так не зовут.

Нигде их так не зовут.

Типажи в расте практически совпадают с классами типов в хаскеле.

Типажи в расте

Даже не знаю, о чем ты. Я говорю о трейтах.

практически совпадают с классами типов в хаскеле

Трейты Rust совпадают с интерфейсами в Java не менее практически.

Semantics for container.IsSorted():
    ∀ i ∈ Integers ∀ j ∈ Integers (container.IsValidIndex(i) && container.IsValidIndex(j) && i <= j) → (container.At(i) <= container.At(j))

Postcondition for container.Sort():
    container.IsSorted() ≡ True

Разве? Если есть лишь одно условие, ему нечему противоречить. Если есть два условия, то первое может противоречить второму. Если три — первое может противоречить второму или третьему. Очевидно, с ростом условий резко растёт и количество возможных противоречий.

А вероятность ошибки тут при чем? Как могли ошибиться в самом первом условии так и дальше можем.

Даже не знаю, о чем ты.

https://ru.wikipedia.org/wiki/Типаж_(абстрактный_тип)

Трейты Rust совпадают с интерфейсами в Java не менее практически.

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

ну и ошибка

вот тебе функция:

sort lst = Nil

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

Как бы тезис о том, что писать правильные спецификации не проще, чем правильный код - можно считать подтвержденным, нет?

https://ru.wikipedia.org/wiki/Типаж_(абстрактный_тип)

Ссылка на русскую Википедию в компьютерной теме, ага.

Трейты Rust совпадают с интерфейсами в Java не менее практически.

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

Трейты умеют всё, что интерфейсы. Так что совпадают.

Могли. Но разговор шёл не про вероятность ошибки как таковой, а про вероятность ошибки, сохраняющей непротиворечивость.

ну и ошибка
твоей спецификации удовлетворяет, но нихрена не сортирует

Да, ты прав.

Иными словами, написать корректную спецификацию ты не шмог.

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

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

Но разговор шёл не про вероятность ошибки как таковой

Нет про это и шел.

вероятность содержать ошибку и в то же время не быть противоречивой

Читай внимательнее.

На то есть оправдание: у меня нет опыта и привычки писать формальные спецификации.

Дело не в этом.

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

Написание кода - это то же самое. Так правильную спецификацию напишешь? ;)

Так правильную спецификацию напишешь? ;)

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

Так правильную спецификацию напишешь? ;)

Похоже, что так:

Postcondition for container.Sort():
    1. container.IsSorted() ≡ True
    2. container.GetNumberOfItems() ≡ Oldstate(container).GetNumberOfItems()
    3. ∀ i ∈ Integers ∃ j ∈ Integers Oldstate(container).IsValidIndex(i) ⇒ ( container.IsValidIndex(j) && (container.At(j) IsAssignedFrom Oldstate(container).At(i)) ) 

sort Nil = Nil
sort [x:xs] = copy x ((length xs) +1)

опять не сортирует это уже вторая попытка

Мне непонятна нотация, которую ты используешь. Вторую строчку можешь описать словами?

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

А если совпадающие элементы есть - будет работать неправильно.

Что именно она будет делать неправильно? Речь ведь о Sort(), а не о StableSort() ?

Ну допустим тебе на вход пришел список [1,1,1], а она вернет [1,2,3].

Ну допустим тебе на вход пришел список [1,1,1], а она вернет [1,2,3].

Под «container.At(j) IsAssignedFrom Oldstate(container).At(i)» подразумевается, что результирующее состояние ячейки j получено путем копирования исходного состояния ячейки i. Не равно исходному состоянию (IsEqual/≡), а именно получено путем копирования (IsAssignedFrom). Допустим, если ты сперва скопировал в голову хвост, а затем скопировал в голову середину, то голова теперь получена копированием из середины, а не из хвоста. Поэтому твой контрпример спецификации не соответствует.

А, тогда ок. Но ирл такие предикаты - это вафли полные.