clojure после common lisp - насколько омерзительно и в чём именно?

Ты серьёзно предлагаешь вместо С и С++ взять Common Lisp?..

Смотря для каких задач. Если писать драйверы, то нет.

Им все равно никто не пользуется, ни первым, ни вторым.

То есть, сначала ты приводишь язык в пример, а потом он оказывается не при чём.

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

Ты вечно выдёргиваешь какие-то отдельные фразы и начинаешь непонятно с чем спорить.

А мне что нужно целые посты цитировать?

Неприятно вести такое общение, можешь засчитывать слив.

Как скажешь.

Он в Си компилируется. Поэтому библиотеку туда можно почти любую воткнуть.

Как я уже сказал, я не знаком с ATS от слова совсем, надо будет глянуть.

А чем он хуже раста?

Нет лайфтаймов.

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

Тогда почему не взлетел ATS?

так тупые все

Probably the biggest problem with ATS2 is the very steep learning curve associated with it. Very few programmers were able to ever overcome it to reach the point where they could truly start enjoying the tremendous power of (advanced) type-checking and (embeddable) templates.

github

Это, я так понимаю, уже пошла racket-вкусовщина?

Не только Racket. Object Pascal, Ada, C++, Java. Всюду есть инкапсуляция, которая позволяет разбить программу на независимые модули. В лиспе независимость модулей на честном слове. В принципе, аналогичная проблема у C++ с указателями, но именно поэтому там теперь целый вагон обёрток поверх них и административный запрет на их прямое использование.

любом динамическом языке можно «случайно запороть» … А запрещать такую возможность тоже странно, хотя бы потому что негибко.

Гм. В питоне запрещено.

$ cat foo.py
def f1(x):
    return x + 1

def f2(x):
    return f1(x) + 1

$ cat bar.py
from foo import *

def f1(x):
    return x - 1

print f1(3)
print f2(3)

$ python bar.py
2
5

foo.f1 не изменилось.

Это, как я понимаю, только в случае с непреднамеренным затиранием имени или что-то еще имеется ввиду?

Имени, значения. Содержимого любого экспортированного объекта. Иногда неаккуратное уточнение defmethod. Например, как у меня в https://github.com/Kalimehtar/cffi-objects/blob/master/redefines.lisp .

А таких средств нету что ли, чтобы найти?

Не знаю. Можно получить список всех реализация метода с описаниями классов. И посмотреть с какими классами вызываешь.

Это пример о том, что кто-то не разобравшись в коде все сломал?

Нет. Это пример про разное понимание «как надо». Вот опять же пример с той же самой моей ссылки. Мне не нравилось, что (defcfun sin :double (x :double)) жёстко требует именно double-float. Я сделал возможность передавать любой объект, который можно преобразовать в double-float (то есть, любое число). Но если кто-то где-то завязался на то, что передача целого числа какой-либо функции должна вызвать исключение и в обработке исключения сделал какой-то нетривиальный код, получится, что совместно мы поломали программу.

В широко используемых языках поломать можно только в наследнике класса в ООП. Но там сразу видно, кто и где поломал. А в моём примере expand-to-foreign-dyn – не мой метод. cffi::foreign-built-in-type – не мой тип. И доопределяю я его даже не по первому аргументу, а по четвёртому. А потом если кто-то захочет найти, почему (defcfun sin :double (x :double)) у него принимает целые значения, ему придётся перелопатить половину потрохов библиотеки cffi.

Но если мы хотим манки-патчинг, что мы будем изолировать?

Как в Racket или python. Можно переопределить любую функцию поверх импортированной. Но нельзя изменить экспортированные имена. А если очень надо, то как в python foo.f1 = f1. Без явного указания модуля не работает.

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

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

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

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

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

Поэтому прототипы пишут на чём-то типа питона и только когда архитектура застыла в граните, переписывают на Java или C++.

Из этого должно следовать, что все проекты (ну кроме тех, где архитектура «застыла в граните» ещё при проектировании на бумажке) начинают на «чём-то типа питона», но это очевидно не так.

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

Можно перефразировать как:

Говно невкусное? Ты просто не умеешь его готовить ;)

В итоге документация где-то устарела, где-то её тупо нет, как и комментариев к коду.

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

Из этого должно следовать, что все проекты (ну кроме тех, где архитектура «застыла в граните» ещё при проектировании на бумажке) начинают на «чём-то типа питона», но это очевидно не так.

Разве? Я даже примера не припомню, чтобы писали на Си++ без архитектуры, а как в PERL/Python: давай накидаем куски алгоритмов, которые понятны и посмотрим, что получится. Один из проектов с PERL на C лично переписывал под заказ (ради производительности).

Зависимые типы вообще имеют очень ограниченную область полезности.

Крайне любопытно, можешь пожалуйста раскрыть мысль?

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

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

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

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

А чем он хуже раста?

Нет лайфтаймов.

Кстати, линейные типы есть в идрисе.

Кстати, линейные типы есть в идрисе.

В ATS тоже есть.

http://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/x3534.html

Но ведь, в отличие от rust, они там не повсюду.

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

Не любые, а только зависящие от натурального числа. Уже для типов - вещественных диапазонов не работает. И даже для целочисленной арифметики по модулю 2^64 не очень работает.

При этом резко усложняются типы функций.

Но ведь, в отличие от rust, они там не повсюду.

В идрисе вроде вполне повсюду, хотя я могу путать, надо будет поглядеть подробнее.

Не любые, а только зависящие от натурального числа. Уже для типов - вещественных диапазонов не работает. И даже для целочисленной арифметики по модулю 2^64 не очень работает.

При этом резко усложняются типы функций.

гм, я не знаю как работать с вещественной арифметикой, спасибо за вопрос.

В идрисе вроде вполне повсюду, хотя я могу путать, надо будет поглядеть подробнее.

Насколько я понимаю, в идрисе можно указать, что тип линейный (а можно не указывать). А в расте, если ссылочный тип не линейный, кусок кода с ним надо завернуть в unsafe.

Насколько я понимаю, в идрисе можно указать, что тип линейный (а можно не указывать).

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

Кстати, флоатинг поинт вполне себе верифицируется

http://iste.co.uk/book.php?id=1238

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

но таки подход описан и похоже можно пользоваться

Понятно, что в компьютере можно вещественное определить как набор целых. Но вот гарантия упорядоченности, которая для Nat выглядит как

natLTETrans : (n, m, o : Nat) -> LTE n m -> LTE m o -> LTE n o
natLTETrans Z _ _ _ _ = lteZero
natLTETrans (S n) (S m) (S o) (lteSucc p) (lteSucc q) = lteSucc (natLTETrans n m o p q)

natLTEEith : (x, y : Nat) -> Either (LTE y x) (LTE x y)
natLTEEith Z _ = Right lteZero
natLTEEith _ Z = Left lteZero
natLTEEith (S n) (S m) with (natLTEEith n m)
  | Right x = Right (lteSucc x)
  | Left y = Left (lteSucc y)

totNat : TotalOrder Nat LTE 
totNat = TotO (PrO natLTETrans) natLTEEith

для вещественных будет весьма нетривиальна.

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

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

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

С натуральными много возьни потому что ими практически всё кодируется, от завершаемости программы до сам не знаю чего. А вещественными, если не специалист, я думаю можно пользоваться прочитав какие то основы. Но я до этого не дошёл.

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

Вот нашёл, положил в закладки, https://www.lri.fr/~melquion/doc/19-jfla30-expose.pdf

Разве? Я даже примера не припомню, чтобы писали на Си++ без архитектуры, а как в PERL/Python: давай накидаем куски алгоритмов, которые понятны и посмотрим, что получится.

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

Я пытаюсь понять суть твоего вопроса не вникая в вопрос с вещественной арифметикой, но получается не очень, честно говоря.

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

массивы не индексируются вещественными, к примеру

Смотря какие. d[0.5] = 2 в Python работает.

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

То есть, с точки зрения использования, лучше какая-то система контрактов, которые проверяются по возможности статически (если компилятор может доказать).

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

И это уже работает даже в компиляторах C++.

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

Те программисты на Java и C++ (которые не писали на других языках), с которыми я общался, всегда сначала проектировали архитектуру (типы, структуры данных). Даже для прототипа. Сначала доска или бумажка, часто обсуждение, а только потом код.

На perl почти всегда наоборот: вот кусок кода, давайте обсудим подойдёт ли такое решение.

Смотря какие. d[0.5] = 2 в Python работает.

Как по мне так аргумент так себе.

То есть, с точки зрения использования, лучше какая-то система контрактов, которые проверяются по возможности статически (если компилятор может доказать).

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

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

В зависимых типах как раз проверяется при компиляции всё что может (в идеале всё).

И это уже работает даже в компиляторах C++.

Видимо, именно поэтому если программа на с++, то она даже после 10 лет фиксов хоть где то да сигфолтится.

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

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

Про это ничего не скажу. Кок он больше про доказательства, идрис всё ещё ранняя альфа, про агду не скажу.

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

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

Кмк, зависимые типы и есть замечательный (и достаточно простой) способ указывать эти контракты.

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

Не говоря уж о нормальных контрактах наподобие:

(provide
 (contract-out
  [argmax
    (->i ([f (-> any/c real?)] [lov (and/c pair? list?)]) ()
         (r (f lov)
            (lambda (r)
              (cond
                [(empty? (rest lov)) (eq? (first lov) r)]
                [else
                 (define f@r (f r))
                 (define flov (map f lov))
                 (and (is-first-max? r f@r (map list lov flov))
                      (dominates-all f@r flov))]))))]))

; f@r is greater or equal to all f@v in flov
(define (dominates-all f@r lov) ...)
 
; r is (first x) for the first
x in lov+flov s.t. (= (second x) f@r)
(define (is-first-max? r f@r lov+flov) ...)

Вот как сделаешь на зависимых типах функцию, которая должна принимать функцию и список и возвращать первый элемент, на котором результат максимален?

Сама функция вот:

argmax :: Ord t1 => (t2 -> t1) -> [t2] -> t2
argmax f [x] = x
argmax f (x:xs) = inner (f x) x f xs
  where 
    inner s r f [] = r
    inner s r f (x:xs) = if s > f x 
      then inner s r f xs 
      else inner (f x) x f xs

контракт в терминах Haskell (от аргументов и результата):

contract f l r =
  l /= [] && all (<= f r) fl && firstEq (f r) l fl r
  where 
    fl = map f l
    firstEq s [] [] r = False
    firstEq s (x:xs) (y:ys) r = if s == y 
      then x == r
      else firstEq s xs ys      ​

Как будет выглядеть динамический тип argmax, которым описывается такой контракт?

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

В Idris для зависимого типа приходится его прописывать как отдельный тип. Нельзя написать List a ** length a == n, надо делать Vect n a. А если требуется не равенство? Какой тип делать, если надо сравнить дины двух списков? Например для

after (x:xs) (y:ys) = after xs ys
after [] ys = ys

надо указать, что длина второго списка больше, чем первого. Как? Делать ещё один тип?

Видимо, именно поэтому если программа на с++, то она даже после 10 лет фиксов хоть где то да сигфолтится.

А это потому, что там есть функция с типом «указатель на неосвобождённые данные -> данные», которую статически почти невозможно проверить (а динамически можно, но дорого) и которая делает что угодно при нарушении своего типа.

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

Спасибо за приведённый пример и вопросы!

Те программисты на Java и C++ (которые не писали на других языках), с которыми я общался, всегда сначала проектировали архитектуру (типы, структуры данных). Даже для прототипа.

Значит я неправильно твой изначальный посыл понял.

Смотря какие. d[0.5] = 2 в Python работает.

А как оно работает? А то у меня получилось «list indices must be integers or slices, not float».

А то у меня получилось «list indices must be integers or slices, not float».

list

Значит d инициализировал списком

А надо массивом с произвольными индексами:

>>> d = {}
>>> d[0.5] = 1

С кодом на хаскеле вроде более-менее понятно, код лиспа попробую тоже поглядеть.

На лиспе то же самое. Подробно вот: https://docs.racket-lang.org/guide/contracts-first.html

Поправка к коду на Haskell:

contract f l r =
  l /= [] && all (<= f r) fl && firstEq (f r) l fl r
  where
    fl = map f l
    firstEq s [] [] r = False
    firstEq s (x:xs) (y:ys) r = if s == y
      then x == r
      else firstEq s xs ys r

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

Вот правильный вариант описания типов (LH):

{-@ after :: l1:[a] -> {l2:[b] | len l2 >= len l1} -> [b] @-}
after (x:xs) (y:ys) = after xs ys
after [] ys = ys

Лаконично и без лишних сущностей.

А надо массивом с произвольными индексами:

Понял, спасибо.

Всё таки отвлёкся...

Но у меня тут вопрос возник по ходу дела: скажи, а когда и как этот контракт вызывать надо?

Т.е. возникает ощущение что это что то вроде теста. Но как именно пользоваться?

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

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

Что то не выходит каменный цветок. Отпишу как видно будет что там получается/не получается.

В общем то сама спека не сложная... как бы..
(код на Коке)

Fixpoint argmax (default : nat) (f : nat -> nat) (xs : list nat) : nat :=
  match xs with
  | [] => default
  | [x] => x
  | x::xs => inner (f x) x f xs
  end
with inner (s r : nat) (f : nat -> nat) (xs : list nat) : nat :=
       match xs with
       | [] => r
       | x::xs' => let fx := f x in
                 if s <? fx
                 then inner fx x f xs'
                 else inner s r f xs'
       end.


Theorem argmax_correct (d : nat) (f : nat -> nat) (xs : list nat) (x : nat): 
    argmax d f xs = x ->
    ((xs = [] /\ x = d) \/
     exists ix, nth_error xs ix = Some x /\
           (forall y iy, nth_error xs iy = Some y -> f y < f x \/ ix <= iy)).
Proof. Admitted.

\/ - дизъюнкция
/\ - конъюнкция

В общем то сама спека не сложная… как бы..

Только все типы у тебя свелись к натуральным числам.

Вот правильный контракт на LH: http://goto.ucsd.edu:8090/index.html#?demo=permalink%2F1617307141_30996.hs

Но у меня не хватает мозгов, как заставить его вывести доказательство.

Только все типы у тебя свелись к натуральным числам.

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

LH конечно интересная штука, но только если с зависимыми типами не знаком.

LH конечно интересная штука, но только если с зависимыми типами не знаком.

Чем? Чтобы вместо {l:[a] | len l = n} писать Vect a n и придумывать по типу на каждое условие?

Тем что привязано непосредственно к коду. И тем как в идрисе редактируется код (https://flowing.systems/assets/game/01/blog_idris_evaluate.gif). И выразительностью. И предполагаемыми возможностями оптимизации.

Кстати, ну вроде ничего не мешает написать вот так (в идрисе, но не поручусь за точность синтаксиса, давно не писал на нём).

after : (xs ys : list a) -> (length xs < length ys) -> list a
after (x::xs) (y::ys) prf = after xs ys (congr S prf что ли.. вроде как то несложно)
after [] ys _ = ys

Только все типы у тебя свелись к натуральным числам.

кстати, я не уверен что всё просто там, где требуется ord. t2 можно заменить на что угодно, зря я nat написал. а вот с ord мне не приходилось работать. Но, кажется, всё должно доказаться.

after : (xs ys : list a) -> (length xs < length ys) -> list a

(length xs < length ys) – не тип. Разве так можно?

(length xs < length ys) – не тип. Разве так можно?

Я сейчас до путя не помню как именно в идрисе, но в целом это работает так: есть два варианта <, один для типов и второй булевский. В коке те которые для типов обозначаются <, <=, >, >= (или соотвественно lt, le, gt, ge), а те которые булевские - <?, <=?, >?, >=? (ltb, leb, gtb, geb). В идрисе точно не помню, но там так же. Нужен соответсвенно тот который для типов. (Т.е. тот который булевский - принимает два натуральных числа, а возвращает булевское значение, а тот который для типов - принимает два натуральныч числа, а возвращает тип).

Но на доказательстве я что то поплыл. Может как то кривовато сформулировал…

Вот это настоящая проблема достаточно мощных статических систем типов. Что-то чуть более нетривиальное, чем сортировку доказать крайне сложно. Можно написать assume, но в контракты времени выполнения условие не сконвертируется и вполне может оказаться ложным.

В общем-то всё доказалось, там не очень сложно. Запутался скорее от недостатка опыта (плюс ошибку сделал при определении inner, в коде выше правда кажется уже поправлено). Попробую сделать орд вместо нат.

Спецификация осталась та же по моему (только я более общий тип добавил для списка).

Fixpoint argmax (A : Type) (default : A) (f : A -> nat) (xs : list A) : A :=
  match xs with
  | [] => default
  | [x] => x
  | x::xs => inner (f x) x f xs
  end
with inner (A : Type) (s : nat) (r : A) (f : A -> nat) (xs : list A) : A :=
       match xs with
       | [] => r
       | x::xs' => let fx := f x in
                 if s <? fx
                 then inner fx x f xs'
                 else inner s r f xs'
       end.

Theorem argmax_correct (A : Type) (d x : A) (f : A -> nat) (xs : list A) :
    argmax d f xs = x ->
    ((xs = [] /\ x = d) \/
     exists ix, nth_error xs ix = Some x /\
           (forall y iy, nth_error xs iy = Some y -> f y < f x \/ ix <= iy)).
Proof. Admitted.

Вот это настоящая проблема достаточно мощных статических систем типов. Что-то чуть более нетривиальное, чем сортировку доказать крайне сложно. Можно написать assume, но в контракты времени выполнения условие не сконвертируется и вполне может оказаться ложным.

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

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

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

Вот ссылка на рабочий код (coq 8.13)

Злобный матан, однако. Ты это всё вручную писал? У меня ощущение, что написать доказательство на бумажке и отдать кому-нибудь на вычитку будет гораздо быстрее.

Если брать контракты, то те же яйца вид сбоку: что мешает сделать ошибку в контракте?

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

При этом логические спецификации читаются по-моему гораздо лучше.

Гм… Считаешь, что «если argmax от f xs равно какому то x, то существует такой индекс ix, что x стоит на месте ix в массиве xs и для любого y стоящего на месте iy в массиве xs выполняется следующее: либо f y < f x либо ix <= iy.» лучше понимается, чем «если argmax от f xs равно какому то x, то s = f x больше или равен любому элементу из map f x и x – первый элемент, для которого f x = s»?

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

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

Существуют истинные недоказываемые утверждения.

Злобный матан, однако. Ты это всё вручную писал? У меня ощущение, что написать доказательство на бумажке и отдать кому-нибудь на вычитку будет гораздо быстрее.

Да, вручную. Несколько часов (больше двух), но у меня практики нет вообще. Вероятно при чуток большем опыте (больше привычки к досадным ошибкам и поведению системы при их наличии) минут 40 должно быть. Доказательства (с использованием тактик) практически нечитаемы, но писать их не так сложно.

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

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

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

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

Ввероятно, лучшее что можно сделать, это рандомизированное тестирование, +-.

А доказательтво - это гарантия, что функция соответствует спецификации. Т.е. вот для любой такой ф-ции, оно будет работать как описано и всё тут.

Гм… Считаешь, что «если argmax от f xs равно какому то x, то существует такой индекс ix, что x стоит на месте ix в массиве xs и для любого y стоящего на месте iy в массиве xs выполняется следующее: либо f y < f x либо ix <= iy.» лучше понимается, чем «если argmax от f xs равно какому то x, то s = f x больше или равен любому элементу из map f x и x – первый элемент, для которого f x = s»?

Я говорю что при небольшой привычке проще читать мат. нотацию, чем код, Нотация более декларативна, что ли.

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

Да, теорему тоже можно написать тоже в терминах той функции другой функции. Не совсем пойму правда на вскидку что тогда нужно будет доказывать. Скорее всего корректность функции contract а потом её эквивалентность функции argmax.

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

Существуют истинные недоказываемые утверждения.

Ну и слава богу, потому что иначе программисты были бы не нужны (потому что система была бы разрешима).