Снова о статической типизации

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

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

Вот это открытие, конечно.

Никакие правила дорожного движения не помогут вам гарантированно избежать аварий.

Никакая розетка не поможет вам гарантированно избежать удара током.

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

Вывод из этого какой?

Нужно ездить на красный, сувать пальцы в розетку и бухать не просыхая? Или что?

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

[[ skipped ]]

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

Да не нервничайте Вы уж так сильно. Я может Вам вагон времени сэкономил. Идея - мертворождённенькая, как по мне. Овчинка выделки не стоит - нет там ничего помимо code bloat и wasted CPU cycles.

Времени? «Идея» тривиально реализуется за 10 минут на крестах.

Здесь нет никакой новой идеи. Идеей это выглядит только для тех, кто начитался «питон для чайников».

В реальной жизни моё время экономят вещи, которые не заставляют меня работать мясным тайпчекером при наличии тайпчекера в софте.

wasted CPU cycles

Может вы еще и пальцем на них покажете?

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

Я в настоящее время читаю доку по austral-lang, на которую давал ссылку страницей ранее.

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

Может вы еще и пальцем на них покажете?

Начнём с пропихивания лишних аргументов, да и собственно самих лишних function calls.

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

Там где хорошие аннотации полностью решают проблему Вы пытаетесь привносить сущности сверх необходимого. Это пройдёт.

Начнём с пропихивания лишних аргументов, да и собственно самих лишних function calls.

Вы про инлайнинг слышали?

Там где хорошие аннотации полностью решают проблему Вы пытаетесь привносить сущности сверх необходимого. Это пройдёт.

И как же они решают проблему? За одно, опишите и проблему, которую они решают. А то как показывает обсуждение, вы решаете какие-то свои проблемы, имеющие слабое отношение к поставленным в ОП.

Это главный бич современной разработки.

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

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

Если не трогать STM, то ближе всех к решению — макрос, который обернёт «функции второго вида не могут быть вызываны при незахваченном мьютексе»

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

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

Гм-гм.. как то двусмысленно. В смысле «не поможет писать» в смысле не будет за вас стучать клавишами и шевелить мозгами. Верно.

Но, «не поможет написать» в смысле «не гарантирует правильность» - не верно.

Правильная статическая типизация гарантирует правильность.

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

Порождение такой правильной типизации эквивалентно порождению правильного алгоритма,

гм, ну нет

Вот пример. Скажем, задача, написать SMT-solver (https://ru.wikipedia.org/wiki/Задача_выполнимости_формул_в_теориях).

Если говорить кратко, есть список булевских переменных (пусть для простоты [a,b,c]). Ну и есть формула, ну пусть a || (b && c). Пусть нужно определить, есть ли такой набор значений для переменных a, b и c, на котором формула приобретает истиное значение. Или же для всех наборов формула ложна.

В таком случае тип для нашей функции solve принимающий на вход формулу f и список переменных xs будет какой-то такой (на Coq).

Definition solve (xs : list bool) (f : formula) : {truth | formulaDenote truth f} + {forall truth, ~~formulaDenote truth f}

кто сказал, что она правильная?

думаю, очевидно

Кстати monk, возвращаясь к дискуссии(Зависимые типы, жидкие типы. Что лучше? (комментарий)): а вот такое утверждение на «жидких типах» напишется? (я думаю вряд ли)

Порождение такой правильной типизации эквивалентно порождению правильного алгоритма

вообще говоря, переводя на язык математики - правильная типизация эквивалентна формулировке утрверждения (например, формулировке теоремы), а построение правильного алгоритма для данного типа эквивалентно докозательству утверждения (теоремы). Соотвествите Карри-Ховарда называется. https://ru.wikipedia.org/wiki/Соответствие_Карри_—_Ховарда

да, прошу прощения, перепутал названия задач, это называется SAT-solver, не smt-solver.

https://ru.wikipedia.org/wiki/Задача_выполнимости_булевых_формул

struct Resource {
    foo: u64,
    bar: u64,
}

struct LockedResource(...);

impl LockedResource {
    fn from_resource(res: &Resource) -> LockedResource { ... }
}

impl Drop for LockedResource { ... }

fn foo(b: bool) {
    let res = Resource::new();
    let mut lr = LockedResource::from_resource(&res);
    lr.do_something_with_shared_resource();
}

Ну и как бы все

Одна из вещей, отвративших меня от изучения хаскела (а я люблю покопаться во всякой там маргинальщине) это наблюдение, что во всех нормальных языках от лиспа до жабоскрипта, от сишки до паскаля спрашивают нормальные вопрос: „как подключиться к базе данных?“, „какой gui framework лучше для написания нового медиаплеера?“, „на проверочном наборе всё норм, а на реальных данных тормозит, почему?“ и только у хаскелистов „я засунул монаду в монаду, применил зигахистаморфный препроморфизм и теперь, каждый раз, когда я читаю ругань компилятора из портала появляется Гитлер и рассказывает анекдот про курочку Рябу. Помогите написать монадический трансформер, чтобы анекдот каждый раз был новый“.

Слова у любителей занырнуть поглубже в теоркат интересные. А на практике выхлоп пощупать не получается.

У вас каждый раз пользователь должен не забыть превратить Resource в LockedResource. Разве смысл был не в том, чтобы даже очень рассеянный разработчик не смог написать неправильный код?

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

Что до Кока - писателей-практиков на нём лично я не встречал. Знакомые люди пишут, но всё хобби на сколько я знаю. Основное занятие для них - доказательства.

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

Но всё таки мейнстрим вроде как для Кока - это доказательства.

У вас каждый раз пользователь должен не забыть превратить Resource в LockedResource. Разве смысл был не в том, чтобы даже очень рассеянный разработчик не смог написать неправильный код?

А ты не сможешь работать с Resource, там тупо методов нужных нет :D

слушай, я вот перечитал твоё сообщение и никак не возьму в толк, ну как можно было отвратиться от хаскеля с такими вводными-то?

„как подключиться к базе данных?“, „какой gui framework лучше для написания нового медиаплеера?“, „на проверочном наборе всё норм, а на реальных данных тормозит, почему?“

Это ж нубство и скукатища лютая просто... и, конечно, никому кроме нубов не надо (да и им самим постольку поскольку).

А вот это

„я засунул монаду в монаду, применил зигахистаморфный препроморфизм и теперь, каждый раз, когда я читаю ругань компилятора из портала появляется Гитлер и рассказывает анекдот про курочку Рябу. Помогите написать монадический трансформер, чтобы анекдот каждый раз был новый“

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

а вот такое утверждение на «жидких типах» напишется? (я думаю вряд ли)

А solve вообще что возвращает? Если булево, то у тебя же слева конкретные xs и f, а справа исчезает xs.

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

formulaDenote вычисляет формулу f на наборе переменных truth

то есть formulaDenote truth f = f truth ?

Если должен быть именно солвер, то есть вернуть для функции истина, если существует такой xs, и ложь, если не существует, то что-то вроде

{-@ solve ::f:([Bool] -> Bool) -> {r:Bool | r == solvePrim f } @-}
solve :: ([Bool] -> Bool) -> Bool

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

А в coq можно проверить, что именно правильно написан солвер?

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

Хотел было предложить запилить анализатор кода во время компиляции (метапрограммирование, но read-only, без трансформаций). Таким макаром, например, я когда-то проверял всякие условия на своём SQL eDSL в скале, которые если зашивать в систему типов, разбухла бы она до безобразия (ты ведь именно этого хочешь избежать?). Проверка во время компиляции – значит тоже статика, просто сверх того, что умеет собственно язык.

В программе имеются мьютексы m1, m2… mN.

А потом вспомнил из недавно читаного ZeroMQ Guide категорический рецепт избавления от любых проблем с многопоточностью: «just don’t share state». (Мужик конечно жжот, люблю максималистов, хотя по здравому размышлению, заменять atomic bool stopBgThread посылкой сообщения stop фоновому потоку я не готов – но твой случай явно посложнее будет.)

Хотел было предложить запилить анализатор кода во время компиляции (метапрограммирование, но read-only, без трансформаций).

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

А solve вообще что возвращает? Если булево, то у тебя же слева конкретные xs и f, а справа исчезает xs.

Не булево. Там xs лишнее, это ты верно подметил.

Верхняя обёртка типа solve (а именно {..} + {..}) — это хаскелевский Either. Значение с типом слева от знака плюс создаётся конструктором inl (от InLeft), с права inr (InRight).

Соответственно, возможны два варианта. Либо то что слева, либо то что справа от знака плюс.

В целом, тип solve'а означает, что solve - это такой алгоритм, который проверит все возможные наборы переменных. Если среди них есть такой вариант на котором формула вернёт истину, то солв вернёт этот набор (это левая часть от знака плюс, читается: существует truth такой, что formulaDenote f truth = true). Если же такого набора нет, то алгоритм вернёт некий терм, который является доказательством того что таких наборов нет (это правая часть от знака плюс, читается: для любого набора truth, выражение formulaDenote f truth равно false).

Что не совсем очевидно, но мне кажется любопытным: правым выражением можно пользоваться как функцией (если вытащить его из упаковки), т.е. можно передать ему как параметр любой список переменных и на выходе получить выражение formulaDenote f [true, false, true] = false. При этом не надо будет вычислять formulaDenote f [true, false, true], просто сразу будет известно что оно false).

Естественно, если распаковать левую часть, взять из неё truth и «скормить» formulaDenote f , то formulaDenote вернёт true.

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

Да, я понял, масло масляное: тогда нужно будет доказывать корректность solvePrim.

А в coq можно проверить, что именно правильно написан солвер?

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

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

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

ну и кажется мы нашли пример, который ты предлагал мне предъявить три года назад :)

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

ну и кажется мы нашли пример, который ты предлагал мне предъявить три года назад :)

поторопился :)

Если компиляется, то по моему оно.

Что насчёт очерёдности n мьютексов (хотя бы гипотетически)?

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

Главное – вовремя остановиться.

Что насчёт очерёдности n мьютексов (хотя бы гипотетически)?

Чтобы мьютекс требовал один из предыдущих?

Если мьютексы конкретные, то что-то вроде

class NeedLock2 a
instance NeedLock2 Lock1

LockMutex2 :: NeedLock2 a => a -> Lock2

class NeedLock3 a
instance NeedLock3 Lock1
instance NeedLock3 Lock2

LockMutex3 :: NeedLock3 a => a -> Lock3
...

Если я вообще условие понял правильно.

Мой интерес к маргинальщине вызван следующим соображением: „если делать всё то же самое, что и все, теми же самыми методами, что и все, то и результат будет такой же, как у всех, т.е. посредственный“. А вот если пойти путями нехоженными, то есть шанс резко повысить свою эффективность. Т.е. даже если в процессе ты развлекаешь себя «занимательными и позновательными» технологиями, всё равно сохраняется дольний прицел на пользу и практическое применение. А если оного применения заведомо не будет, то к чему тогда это всё?

я задачу понял так:

есть N мьютексов (пусть три, назовём 1,2,3). И есть заданный порядок их переключений. Например, лочить их можно только в порядке 1, 2, 3. А анлочить в порядке 2, 3, 1. К примеру.

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

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

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

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

например, при попытке залочить мьютекс 2 в случае если мьютекс 1 не залочен

Вроде были примеры, что пропуск возможен. Поэтому классы типов (возможные предыдущие локи). Если просто цепочка, тогда проще

LockMutex2 :: Lock1 -> Lock2
LockMutex3 :: Lock2 -> Lock3
...

а так же при попытке разлочить разлоченный.

Это я не проверял. Если так, то LockMutex2 не экспортируем, а экспортируем

withLock1 :: (Lock1 -> a) -> a
withLock2 :: Lock1 -> (Lock2 -> a) -> a

Этой ещё надо в IO же завернуть…

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

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

В программе имеются мьютексы m1, m2… mN.

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

и увеличивается падучесть

ой словно core dumped не привычная ошибка. Я её чаще вижу

тут понимаешь какая штука...

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

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

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

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

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

И вот отсюда вопрос у меня: кажется мне что надо как-то маргинальщину от маргинальщины таки отличать.

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

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

Я думаю не надо так.

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

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

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

В науке так или иначе людей задействовано меньше чем в производстве. Ну так жизнь устроена. Это не маргинальщина.

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

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

Я желаю вам всяческих успехов и сам буду рад

Спасибо большое, аналогично.

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

Гм. Ну, по формальной верификации, это, конечно, большое спасибо за вопрос :)

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

Часто люди которые не слишком углублялись в вопрос видят формальную верификацию как некую не вполне понятную альтернативу тестированию при разработке ПО. Нужно сказать, что по крайней мере на данный момент это в, целом, ошибочное мнение. Формальная верификация не заменяет тестирование и не отменяет его. Может быть когда-то в будущем подходы разовьются и получится разрабатывать верифицированный код или может быть Type Driven Development от Edwin Brady получит распространение, что [пмсм] гипотетически сильно сократит количество тестов... но это всё не сегодня.

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

Теперь мне кажется уже довольно очевидным, что из вопроса «А много ли корзин заказа которые отдавали на аудит вы видели?» и ответа на него в виде цифры ноль отнюдь не следует фраза ниже

Рад буду ошибиться, но … как будто есть фундаментальная причина, почему *провести аудит на тему* «данная булевая функция удовлетворяет таким-то критериям» получается, а для чего-нибудь полезного вроде «в корзину заказа могут попадать только имеющиеся на складе товары» — не выходит.

Отчасти просто потому на самом деле что вы не там смотрите. Попробуйте например набрать в поисковике «formal verification of smart contracts».

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

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

За вопрос - большое спасибо ещё раз :)

Инженеру, физику и математику дают задание потушить пожар. Инженер выбегает, хватает пожарный шланг и заливают огонь десятью тоннами воды. Физик рассматривает модель объекта, оценивает тепературу пламени и скорость ветра и заливает огонь минимально достаточным количеством воды. Математик смотрит на огонь, смотрит на пожарный кран, говорит: „Решение существует“ и уходит.

Собственно, на моём языке «нельяз» и «слишком дорого и сложно» это почти синонимы. Т.е. вы буквально повторили мой тезис, но своими словами. Если для Боинга проще угробить самолёт с людьми, чем воспользоваться методой, то для нас, простых смертных, вообще говорить не о чем, что полёты на Марс, что формальная верификация одинаково [не] возможны.

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

Не совсем верно на самом деле.

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

Формальная верификация тоже используется, тоже не для корзин с товарами. Ещё реже чем аудит, но тем не менее.

Что до Боинга, это вопрос довольно сложный, вы зря упрощаете. То что им [я так понимаю] проще угробить самолёт раз в N лет, чем увеличить стоимость разработки софта (условно вдвое я бы сказал) - это совсем не говорит о том что это для них неподъёмно. Разработка софта там в стоимости самолёта - не такие уж деньги, на сколько я себе представляю.

Просто для Боинга.. как бы это помягче.. ну нет убытков от того что иногда, раз там в N лет, самолёт упадёт из-за ошибки в ПО.. понимаете? Ну какой им от этого убыток? Ну упал. Ну бывает. Ну пилот ошибся. (Вон как та история с британской почтой). Если уж выяснят что действительно ПО, ну поправим. Что перестали хоть раз боинги после падения покупать? Хотя бы спрос упал? Я не слышал, может пропустил. А деньги за верификацию отдать придётся. Ну и смысл?

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

то для нас, простых смертных, вообще говорить не о чем, что полёты на Марс, что формальная верификация одинаково [не] возможны

Наверное в целом нужно иметь ввиду смену профессии. Я соглашуьс в этом смысле. Это, безусловно отдельная профессия.

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

Для ясности, я ни на чём не настаиваю, просто немного расказываю о своей точке зрения.

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

Но за интересные вопросы отдельное спасибо, серьёзно.

кто сказал, что она правильная?

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

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

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

Как в классическом анекдоте:

Заходит однажды тестировщик в бар.
Забегает в бар.
Пролезает в бар.
Танцуя, проникает в бар.
Крадется в бар.
Врывается в бар.
Прыгает в бар

и заказывает:

кружку пива,
2 кружки пива,
0 кружек пива,
999999999 кружек пива,
ящерицу в стакане,
–1 кружку пива,
qwertyuip кружек пива.

...

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

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

потому что пример с булевыми функциями - наивен.

вот другой совсем простой пример.

есть тип - «простое число произвольной длины». и есть переменная данного типа - x.

надо статически проверить корректность выражения:

var x: PrimeNumber = некое_очень_длинное_нечетное_число.

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

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

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

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

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

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