Этого треда уже нет.
Это копия, сохраненная 13 ноября 2017 года.
Скачать тред: только с превью, с превью и прикрепленными файлами.
Второй вариант может долго скачиваться. Файлы будут только в живых или недавно утонувших тредах. Подробнее
Если вам полезен архив М.Двача, пожертвуйте на оплату сервера.
Это копия, сохраненная 13 ноября 2017 года.
Скачать тред: только с превью, с превью и прикрепленными файлами.
Второй вариант может долго скачиваться. Файлы будут только в живых или недавно утонувших тредах. Подробнее
Если вам полезен архив М.Двача, пожертвуйте на оплату сервера.
53 Кб, 638x479
Сап, Программач. Расскажи мне, на каких проектах и в каких отраслях в России и остальном мире востребована на практике формальная верификация. Куда теоретически можно податься лет через 5 - 6 тому человеку, кто любит дрочить на лямбда калкулус, зависимые типы и т. д.
На каких проектах в будущем (ближайшие 10 - 30 лет) будет востребована формальная верификация? Какие языки и фрэймворки будут востребованы для этого дела? Бизнесы в целом в мире будут охотнее выделять деньги на 100% верифицированные проекты или будут еще больше жмотить, давить, стоять с кнутом, требовать аджайл, хуяк, хуяк и в продакшон? Доживем ли мы до того момента, когда каждый стек ZigBee на Си, каждое ядро ОС, каждая СУБД, каждая компьютерная игра, каждое банковское веб-приложение на (Elm + JS), каждая сраная соцсеть на Elm-Lang будет формально верифицированы так или иначе? И есть ли будущее у вот этого проекта - верифицированного Си-компилятора http://compcert.inria.fr/ как думаете?
На каких проектах в будущем (ближайшие 10 - 30 лет) будет востребована формальная верификация? Какие языки и фрэймворки будут востребованы для этого дела? Бизнесы в целом в мире будут охотнее выделять деньги на 100% верифицированные проекты или будут еще больше жмотить, давить, стоять с кнутом, требовать аджайл, хуяк, хуяк и в продакшон? Доживем ли мы до того момента, когда каждый стек ZigBee на Си, каждое ядро ОС, каждая СУБД, каждая компьютерная игра, каждое банковское веб-приложение на (Elm + JS), каждая сраная соцсеть на Elm-Lang будет формально верифицированы так или иначе? И есть ли будущее у вот этого проекта - верифицированного Си-компилятора http://compcert.inria.fr/ как думаете?
И почему сейчас многие корпорации на проектах предпочитают даже 100%-ное покрытие юнит-тестами, нежели 100%-ную формальную верификацию? Неужели тотальное покрытие юнит тестами и тест-драйвен девелопмент дешевле обходится?
Может ли 100%-ная формальная верификация вообще заметить тестирование, QA Automation и прочих QA-инженеров оставить без работы? Можно ли обойтись без тестов вообще, используя только теоремы и теорем-прувер?
Может ли 100%-ная формальная верификация вообще заметить тестирование, QA Automation и прочих QA-инженеров оставить без работы? Можно ли обойтись без тестов вообще, используя только теоремы и теорем-прувер?
>>1077629 (OP)
Нет.
Потому, что, смотреть выше.
>Может ли 100%-ная формальная верификация вообще заметить тестирование, QA Automation и прочих QA-инженеров оставить без работы? Можно ли обойтись без тестов вообще, используя только теоремы и теорем-прувер?
Нет.
>И почему сейчас многие корпорации на проектах предпочитают
Потому, что, смотреть выше.
>>1077631
Интуитивно чувствую, что не взлетит, люди такие сволочи, что не смогут составить требования, которые формально верифицируются, плюс им для удобства нравится в процессе разработки запускать недописанную программу, а тут по сути тебе сначала нужно написать все ТЗ.
Интуитивно чувствую, что не взлетит, люди такие сволочи, что не смогут составить требования, которые формально верифицируются, плюс им для удобства нравится в процессе разработки запускать недописанную программу, а тут по сути тебе сначала нужно написать все ТЗ.
>>1077629 (OP)
Не понял как можно противопоставлять формальную верификацию и аджайл. Может быть ты хочешь использовать первое как дополнение методологий второго?
Я слышал в космосе каскадами и формальными верификациями обмазываются, но это не точно.
Не понял как можно противопоставлять формальную верификацию и аджайл. Может быть ты хочешь использовать первое как дополнение методологий второго?
> в каких отраслях в России и остальном мире востребована на практике формальная верификация
Я слышал в космосе каскадами и формальными верификациями обмазываются, но это не точно.
>>1077642
А это ёбаный аджайл, который зачастую дополняется скрамом с 2-недельными спринтами с обязательным показыванием промежуточного результата и его обсуждения, еже2недельными релизами софта.
"Нет, передвиньте менюшку влево, а отображение комментов сделайте линейным!"
через 2 недели:
"Нет, меню вправо, а комменты норм! Вы, дебилы, не могли догадаться?!"
через 2 недели:
"Да меню норм, а комменты сделайте древовидными! Сволочи, за что я вам деньги плачу! Всё не так! Я иначе говорил!"
через 2 недели:
"Комменты норм, а вот меню влево давайте! Да вы меня совсем не слушаете, скоты! Я не так говорил раньше вам!"
>плюс им для удобства нравится в процессе разработки запускать недописанную программу
А это ёбаный аджайл, который зачастую дополняется скрамом с 2-недельными спринтами с обязательным показыванием промежуточного результата и его обсуждения, еже2недельными релизами софта.
"Нет, передвиньте менюшку влево, а отображение комментов сделайте линейным!"
через 2 недели:
"Нет, меню вправо, а комменты норм! Вы, дебилы, не могли догадаться?!"
через 2 недели:
"Да меню норм, а комменты сделайте древовидными! Сволочи, за что я вам деньги плачу! Всё не так! Я иначе говорил!"
через 2 недели:
"Комменты норм, а вот меню влево давайте! Да вы меня совсем не слушаете, скоты! Я не так говорил раньше вам!"
>>1077650
У вас блядь логов нет в которые вы клиентов тыкаете, или у вас там конченые дауны работают которые не могут клиентам их собственный заказ показать? Что за контора уровня "Рога и копыта"?
У вас блядь логов нет в которые вы клиентов тыкаете, или у вас там конченые дауны работают которые не могут клиентам их собственный заказ показать? Что за контора уровня "Рога и копыта"?
>>1077631
Во-первых - да, дешевле. Во-вторых - ну ты типа поработай где-нибудь хоть раз или книжку какую про разработку почитай, кроме юнит-тестов есть как бы еще много других видов тестов. В-третьих - ты, блядь, понимаешь, что ТДД - это методология разработки софта и написания кода, которая эти самые процессы ускоряет? Это, блядь, метод проектирования, к тестам как таковым оно вообще отношение имеет весьма опосредованное.
По поводу вопроса из оп-поста - ну читай штангиста, хули ты. Банки-трейдинги, машинки-самолеты, компиляторы-микропроцессоры. В ракетах, кстати, никакого лямбда-калькулюса, емнип, нет - просто там каждое байтоебство проверяется, документируется и верифицируется на бумажке десятью пиэйчди, прежде чем оно уйдет в репозиторий. На строчку кода страница документации - вот и все.
Ну и вообще, судя по твоим постам ты слабо себе представляешь, что такое формальная верификация и зачем она нужна, что такое разработка софта и как ей занимаются, что такое лябмда-калькулюс и откуда он нынче торчит и т.п.
>Неужели тотальное покрытие юнит тестами и тест-драйвен девелопмент дешевле обходится?
Во-первых - да, дешевле. Во-вторых - ну ты типа поработай где-нибудь хоть раз или книжку какую про разработку почитай, кроме юнит-тестов есть как бы еще много других видов тестов. В-третьих - ты, блядь, понимаешь, что ТДД - это методология разработки софта и написания кода, которая эти самые процессы ускоряет? Это, блядь, метод проектирования, к тестам как таковым оно вообще отношение имеет весьма опосредованное.
По поводу вопроса из оп-поста - ну читай штангиста, хули ты. Банки-трейдинги, машинки-самолеты, компиляторы-микропроцессоры. В ракетах, кстати, никакого лямбда-калькулюса, емнип, нет - просто там каждое байтоебство проверяется, документируется и верифицируется на бумажке десятью пиэйчди, прежде чем оно уйдет в репозиторий. На строчку кода страница документации - вот и все.
Ну и вообще, судя по твоим постам ты слабо себе представляешь, что такое формальная верификация и зачем она нужна, что такое разработка софта и как ей занимаются, что такое лябмда-калькулюс и откуда он нынче торчит и т.п.
>>1077655
Объясни, если в теме, плз.
>Ну и вообще, судя по твоим постам ты слабо себе представляешь, что такое формальная верификация и зачем она нужна, что такое разработка софта и как ей занимаются, что такое лябмда-калькулюс и откуда он нынче торчит и т.п.
Объясни, если в теме, плз.
>>1077653
Логи есть. Но когда в них тыкаешь клиента, он все равно говорит, что ВИНОВАТЫ МЫ, потому что медленно делали (хотя спринт закрыли вовремя), не догадались, тупим сидим, и вообще рейты надо понизить. Знакомо?
>У вас блядь логов нет в которые вы клиентов тыкаете
Логи есть. Но когда в них тыкаешь клиента, он все равно говорит, что ВИНОВАТЫ МЫ, потому что медленно делали (хотя спринт закрыли вовремя), не догадались, тупим сидим, и вообще рейты надо понизить. Знакомо?
>>1077650
Нет не аджайл, просто в любой разработке итерации, я хочу, чтобы программа запускалась и хоть часть окон в ней работала, я ебал как то работать над одним проектом, где месяц надо было писать код считай в уме, вслепую, не зная заработает ли потом все вместе.
Нет не аджайл, просто в любой разработке итерации, я хочу, чтобы программа запускалась и хоть часть окон в ней работала, я ебал как то работать над одним проектом, где месяц надо было писать код считай в уме, вслепую, не зная заработает ли потом все вместе.
>>1077657
Методология разработки, в нынешнее время немножко мертвая, т.к. обычному бизнесу нужен фидбек чуть чаще чем раз в джгод, полджгода (ему нужно каждые две недели формочки перетаскивать, ага).
Методология разработки, в нынешнее время немножко мертвая, т.к. обычному бизнесу нужен фидбек чуть чаще чем раз в джгод, полджгода (ему нужно каждые две недели формочки перетаскивать, ага).
>>1077655
А что там понимать? Жиды придумали новый способ, как заставить писать в три раза больше кода за ту же зарплату. (В два раза больше было с тестами). А ты становись ДевОпсом, сука.
А что там понимать? Жиды придумали новый способ, как заставить писать в три раза больше кода за ту же зарплату. (В два раза больше было с тестами). А ты становись ДевОпсом, сука.
>>1077666
а, вотэрфолл! так бы и сказал!
а, вотэрфолл! так бы и сказал!
>>1077629 (OP)
Расскажи, далеко продвинулся? Куда дальше?
Спрашиваю без всякого подвоха или критики. Просто, в самом деле интересно.
>человеку, кто любит дрочить на лямбда калкулус, зависимые типы и т. д.
Расскажи, далеко продвинулся? Куда дальше?
Спрашиваю без всякого подвоха или критики. Просто, в самом деле интересно.
>>1077629 (OP)
Что пипл схавает, на то и выделят.
Потому что это разные вещи.
Если не считать того, что спецификацию с их помощью ты не проверишь и что верифицированных конкрунтоспособных процессоров (не говорю уже про компиляторы. По ссылке - компилятор для C90) нет и что самонепротиворечивость не для всех языков доказуема - МОЖНО.
>Бизнесы в целом в мире будут охотнее выделять деньги на 100% верифицированные проекты или будут еще больше жмотить, давить, стоять с кнутом, требовать аджайл, хуяк, хуяк и в продакшон?
Что пипл схавает, на то и выделят.
>И почему сейчас многие корпорации на проектах предпочитают даже 100%-ное покрытие юнит-тестами, нежели 100%-ную формальную верификацию? Неужели тотальное покрытие юнит тестами и тест-драйвен девелопмент дешевле обходится?
Потому что это разные вещи.
>Может ли 100%-ная формальная верификация вообще заметить тестирование, QA Automation и прочих QA-инженеров оставить без работы? Можно ли обойтись без тестов вообще, используя только теоремы и теорем-прувер?
Если не считать того, что спецификацию с их помощью ты не проверишь и что верифицированных конкрунтоспособных процессоров (не говорю уже про компиляторы. По ссылке - компилятор для C90) нет и что самонепротиворечивость не для всех языков доказуема - МОЖНО.
>>1077680
Приведи пример (гипотетический), когда 100% верифицированная программа упадет на любом юнит-тесте.
>Потому что это разные вещи.
Приведи пример (гипотетический), когда 100% верифицированная программа упадет на любом юнит-тесте.
>>1077681
Желаемое поведение не всегда описывается не на верифицируемом языке (тот же ГУЙ, например). Если есть ошибка/неточность в спецификациях, верифицирование тебе не поможет.
Желаемое поведение не всегда описывается не на верифицируемом языке (тот же ГУЙ, например). Если есть ошибка/неточность в спецификациях, верифицирование тебе не поможет.
>>1077686
тестирование тоже. ибо проект делают по спеке
>Если есть ошибка/неточность в спецификациях, верифицирование тебе не поможет
тестирование тоже. ибо проект делают по спеке
То есть, предполагается, что заказчик (в широком смысле слова) в некоторых случаях может судить о корректности программы по юнит-тестам (и не только таким тестам) лучше, чем по формальному описанию.
>>1077686
Надо различать верификацию и валидацию.
>Желаемое поведение не всегда описывается не на верифицируемом языке
Надо различать верификацию и валидацию.
>>1077690
Мой пост как раз об этом - о том, что задачи тестирования отличаются от задач верификациию
Мой пост как раз об этом - о том, что задачи тестирования отличаются от задач верификациию
>>1077694
Цель тестирования софта - найти бОльшую часть багов.
Цель формальной верификации с автоматизированным теоремпрувером - математически доказать, что программа будет корректно работать с абсолютно любых условиях с абсолютно любыми комбинациями любых входных данных. Даже 100% покрытие юнит тестами не гарантирует этого. А вот если Why3 прувер напишет, что все теоремы доказаны, тогда можно радоваться - гарантия есть.
Цель тестирования софта - найти бОльшую часть багов.
Цель формальной верификации с автоматизированным теоремпрувером - математически доказать, что программа будет корректно работать с абсолютно любых условиях с абсолютно любыми комбинациями любых входных данных. Даже 100% покрытие юнит тестами не гарантирует этого. А вот если Why3 прувер напишет, что все теоремы доказаны, тогда можно радоваться - гарантия есть.
>>1077694
Если смотреть на программирование с точки зрения "заказчик-исполнитель", то цели очевидны - проверить соответствия исполнения заказу ИЛИ желаниям покупателя (в зависимости от того, насколько ТЗ хреновое).
Если смотреть на программирование с точки зрения "заказчик-исполнитель", то цели очевидны - проверить соответствия исполнения заказу ИЛИ желаниям покупателя (в зависимости от того, насколько ТЗ хреновое).
>>1077695
То есть для борьбы с программными дефектами есть две альтернативы:
1. (верификация) составлять сразу корректную программу.
2. (тестирование) изнурительно проверять готовую программу без всяких гарантий обнаружения всех дефектов, или хотя бы бОльшей их части, или даже хотя бы одного.
То есть для борьбы с программными дефектами есть две альтернативы:
1. (верификация) составлять сразу корректную программу.
2. (тестирование) изнурительно проверять готовую программу без всяких гарантий обнаружения всех дефектов, или хотя бы бОльшей их части, или даже хотя бы одного.
>>1077695
И ещё, тестирование к валидации, в общем то, не имеет отношения.
И ещё, тестирование к валидации, в общем то, не имеет отношения.
>>1077697
Думаю, нет. Проверяют же соответствие требованиям.
>проверить соответствия исполнения заказу ИЛИ желаниям покупателя
Думаю, нет. Проверяют же соответствие требованиям.
>>1077709
Ты путаешь реальность и идеалы. В реальности требованиями обладает ТОЛЬКО заказчик, а исполнителю достаётся пережёванная версия, и тестирование это несоответствие может обнажить и побудить заказчика к жалобам.
Ты путаешь реальность и идеалы. В реальности требованиями обладает ТОЛЬКО заказчик, а исполнителю достаётся пережёванная версия, и тестирование это несоответствие может обнажить и побудить заказчика к жалобам.
>>1077713
Но тестирующий разве не строго по требованиям работает? Как же он тесты будет составлять, не имея требований? Если требованиями обладает только заказчик, значит только он и может обнаружить несоответствие программы требованиям.
>требованиями обладает ТОЛЬКО заказчик
Но тестирующий разве не строго по требованиям работает? Как же он тесты будет составлять, не имея требований? Если требованиями обладает только заказчик, значит только он и может обнаружить несоответствие программы требованиям.
>>1077702
Нет, не сразу. Можно написать некорректную, потом запустить прувер, глянуть на ошибки и исправить их.
Да. Причем тесты бывают регрессионными, например, то есть совокупные затраты на все тесты в течение всего времени жизни проекта могут превысить затраты на лямбдоёбство и использование Why3 прувера
>1. (верификация) составлять сразу корректную программу.
Нет, не сразу. Можно написать некорректную, потом запустить прувер, глянуть на ошибки и исправить их.
>2. (тестирование) изнурительно проверять готовую программу без всяких гарантий обнаружения всех дефектов, или хотя бы бОльшей их части, или даже хотя бы одного.
Да. Причем тесты бывают регрессионными, например, то есть совокупные затраты на все тесты в течение всего времени жизни проекта могут превысить затраты на лямбдоёбство и использование Why3 прувера
>>1077715
Бинго! Бывает почти идеальное взаимодействие, бывает неидеальное. Тестирование - это не только проверка соответствия формальным требованиям, но и вид взаимодействия (хотя, ОП спрашивал про юнит-тестирование).
Бинго! Бывает почти идеальное взаимодействие, бывает неидеальное. Тестирование - это не только проверка соответствия формальным требованиям, но и вид взаимодействия (хотя, ОП спрашивал про юнит-тестирование).
>>1077715
Только в том случае, если теорем-прувер докажет, что код верен.
>Если требованиями обладает только заказчик, значит только он и может обнаружить несоответствие программы требованиям.
Только в том случае, если теорем-прувер докажет, что код верен.
>>1077717
Имеется в виду, что готовая программа корректна сразу после компиляции.
>Нет, не сразу. Можно написать некорректную, потом запустить прувер, глянуть на ошибки и исправить их.
Имеется в виду, что готовая программа корректна сразу после компиляции.
>>1077709
Во-первых, сами требования могут оказаться неформализуемыми (хочу, чтобы интерфейс был красивым)
Во-вторых, если тестировщик не аутист, он может находить дефекты и сам, без требований (вот на этом экране есть кнопка отмены, а на этом стелочка назад, неконсистентно и приличные компании так не делают)
Во-первых, сами требования могут оказаться неформализуемыми (хочу, чтобы интерфейс был красивым)
Во-вторых, если тестировщик не аутист, он может находить дефекты и сам, без требований (вот на этом экране есть кнопка отмены, а на этом стелочка назад, неконсистентно и приличные компании так не делают)
>>1077723
Можно как с тестами, сначала писать программу, а потом покрывать пред/пост условиями?
Можно как с тестами, сначала писать программу, а потом покрывать пред/пост условиями?
>>1077629 (OP)
Про какую именно формальную верификацию идёт речь? Formal Property Checking? Или может какой-нибудь Model Checking?
Про какую именно формальную верификацию идёт речь? Formal Property Checking? Или может какой-нибудь Model Checking?
>>1077629 (OP)
)))
За границу, без шуток. Хоть покушать будет на что, не будешь Перельманом сидеть в пустой хрущобе.
>в России
)))
>Куда теоретически можно податься лет через 5 - 6 тому человеку, кто любит дрочить на лямбда калкулус, зависимые типы и т. д.
За границу, без шуток. Хоть покушать будет на что, не будешь Перельманом сидеть в пустой хрущобе.
>>1077692
Был пример - с помощью формальных методов вели разработку одной из подсистем самолета - шасси. Верифицировали да не выверифицировали. На полетном испытании при посадке самолет чуть не выехал за взлетную полосу - модель была корректная, но она предполагала включение тормозов, после прокрутки колес. Как назло при испытании ВПП была мокрой после дождя и тормоза сработали с задержкой. Такая вот прохладная история. Само определение ВАЛИДАЦИИ намекает.
https://blog.regehr.org/archives/742
Был пример - с помощью формальных методов вели разработку одной из подсистем самолета - шасси. Верифицировали да не выверифицировали. На полетном испытании при посадке самолет чуть не выехал за взлетную полосу - модель была корректная, но она предполагала включение тормозов, после прокрутки колес. Как назло при испытании ВПП была мокрой после дождя и тормоза сработали с задержкой. Такая вот прохладная история. Само определение ВАЛИДАЦИИ намекает.
https://blog.regehr.org/archives/742
>>1077629 (OP)
Нахуй не нужна. Так как формальная верификация по определению верифицирует то, что уже формализовано. Тогда как сложность программирования (и где собственно делаются все ошибки) происходит на этапе формализации, составлении алгоритма.
Нахуй не нужна. Так как формальная верификация по определению верифицирует то, что уже формализовано. Тогда как сложность программирования (и где собственно делаются все ошибки) происходит на этапе формализации, составлении алгоритма.
>Куда теоретически можно податься лет через 5 - 6 тому человеку, кто любит дрочить на лямбда калкулус, зависимые типы и т. д.
В любую функо-парашу, на jvm'е их высыпало как грибов после дождя.
>>1077629 (OP)
>На каких проектах в будущем (ближайшие 10 - 30 лет) будет востребована формальная верификация?
В любительских.
>Доживем ли мы до того момента, когда каждый стек ZigBee на Си, каждое ядро ОС, каждая СУБД, каждая компьютерная игра, каждое банковское веб-приложение на (Elm + JS), каждая сраная соцсеть на Elm-Lang будет формально верифицированы так или иначе?
Нет, это промежуточная сырая стадия развития, на ее развитие уйдет больше чем на принципиальное обновление общей идеологии ПО.
>И есть ли будущее у вот этого проекта - верифицированного Си-компилятора http://compcert.inria.fr/ как думаете?
Нет, ведь код написанный для этого компилятора не будет верифицирован, доля ошибок самого компилятора в том же gcc ничтожно мала.
>>1077927
А что там еще можно придумать? Новые методолгии управления проектами, чтобы не было говнокода? Новые IDE? Новые языки?
>Нет, это промежуточная сырая стадия развития, на ее развитие уйдет больше чем на принципиальное обновление общей идеологии ПО.
А что там еще можно придумать? Новые методолгии управления проектами, чтобы не было говнокода? Новые IDE? Новые языки?
>>1077927
Вообще-то он там верифицируется на Петухе (Coq Gallina).
>код написанный для этого компилятора не будет верифицирован
Вообще-то он там верифицируется на Петухе (Coq Gallina).
>>1077770
model checking?
model checking?
>>1077769
Тестирование для этого не подходит.
>Во-первых, сами требования могут оказаться неформализуемыми (хочу, чтобы интерфейс был красивым)
Тестирование для этого не подходит.
>>1077781
LOL
LOL
>>1077781
Не имеет отношения к верификации.
Для верификации применим proof checking (via typing), который в перспективе выводит далеко за рамки только лишь верификации, а именно к подходу correctness by construction в программировании.
Разница в том, что proof checker проверяет предъявленное ему доказательство пропозиции, в то время как theorem prover сам дедуктивно его находит или не находит.
>Automated theorem proving
Не имеет отношения к верификации.
Для верификации применим proof checking (via typing), который в перспективе выводит далеко за рамки только лишь верификации, а именно к подходу correctness by construction в программировании.
Разница в том, что proof checker проверяет предъявленное ему доказательство пропозиции, в то время как theorem prover сам дедуктивно его находит или не находит.
>>1078082
spark в Ada использует пруф чекинг или тиорим прувинг?
spark в Ada использует пруф чекинг или тиорим прувинг?
Кто знает, расскажите про статический анализ кода. Он ближе к верификации или к юнит-тестированию?
>>1078161
Верификация это вот что: код на высокоуровневом языке программирования экстрактится в язык, понятный теорем-пруверу (Lean, Coq, Why3), затем пишется несколько теорем (вручную) и они проверяются (автоматически).
Верификация это вот что: код на высокоуровневом языке программирования экстрактится в язык, понятный теорем-пруверу (Lean, Coq, Why3), затем пишется несколько теорем (вручную) и они проверяются (автоматически).
>>1077629 (OP)
Что такое верификация? Чем она отличается от доказательства?
Что такое верификация? Чем она отличается от доказательства?
>>1077629 (OP)
Ни в каких
На майлист хаскеоьёбов подпишись, там иногда проскакивают вакансии с требованиями знания формальных методов. Но крайне редко. Во этим https://galois.com иногда надо.
>Сап, Программач. Расскажи мне, на каких проектах и в каких отраслях в России
Ни в каких
>остальном мире
На майлист хаскеоьёбов подпишись, там иногда проскакивают вакансии с требованиями знания формальных методов. Но крайне редко. Во этим https://galois.com иногда надо.
>>1078683
Объясните, что это вообще такое? Почему на этом так акцентируются? Откуда такое дегенератское название?
>бизнес логику
Объясните, что это вообще такое? Почему на этом так акцентируются? Откуда такое дегенератское название?
>>1078679
Не знаешь - не умничай.
Не знаешь - не умничай.
Hello, OP KHUY!
Galois is growing again! We're looking for researchers, principal investigators, software engineers, students and mamkin's byblocoders including those with expertise in functional programming, formal methods, machine learning, embedded systems, computer security, or networking. For the exact available positions, please have a look at our website: http://galois.com/careers
We now have three locations: Portland, Ore.; Arlington, Va.; and Dayton, Ohio. There are positions available at all locations.
We are looking for people to work on-site, not remotely. Mostly, we are looking for candidates who are already authorized to work in the US, but in exceptional situations we can work with the candidate to obtain the necessary documentation.
If you are interested, please apply through the web site. If you have questions about working at Galois, you're welcome to contact me directly.
Best regards,
Nikita Sadkov
Galois is growing again! We're looking for researchers, principal investigators, software engineers, students and mamkin's byblocoders including those with expertise in functional programming, formal methods, machine learning, embedded systems, computer security, or networking. For the exact available positions, please have a look at our website: http://galois.com/careers
We now have three locations: Portland, Ore.; Arlington, Va.; and Dayton, Ohio. There are positions available at all locations.
We are looking for people to work on-site, not remotely. Mostly, we are looking for candidates who are already authorized to work in the US, but in exceptional situations we can work with the candidate to obtain the necessary documentation.
If you are interested, please apply through the web site. If you have questions about working at Galois, you're welcome to contact me directly.
Best regards,
Nikita Sadkov
>>1078696
ПО решает какую-то проблему бизнеса (а бизнес решает какую-то проблему клиента), поэтому и бизнес логика. Ты можешь верифицировать, что код складывает помидоры с огурцами, но невозможно верифицировать, что бизнесу надо было их скаладывать, а не огурцы с арбузами, например.
ПО решает какую-то проблему бизнеса (а бизнес решает какую-то проблему клиента), поэтому и бизнес логика. Ты можешь верифицировать, что код складывает помидоры с огурцами, но невозможно верифицировать, что бизнесу надо было их скаладывать, а не огурцы с арбузами, например.
>>1078769
Спасает валидация в таком случае.
Спасает валидация в таком случае.
>>1078805
Два чаю. Никогда не согласился бы на он-сайт.
Два чаю. Никогда не согласился бы на он-сайт.
Кто-нибудь в курсе по поводу статуса альтернативного синтаксиса в Coq (того который начинается с команды proof)? Почему то из мануала убрали целую главу про него и заменили на ssreflect.
>>1078871
Я не жалуюсь, мне норм.
Я не жалуюсь, мне норм.
>>1077982
240 килограммов чистого железа!!111
240 килограммов чистого железа!!111
>>1077982
Овуляха, дрочащая на мраморную говядину, приседания с нагрузкой и чрезмерное чсв, выражающееся в "программировании" конечных автоматов на хачкиле О БОЖЕ На хачкиле в середине проебанных нулевых. Что мы там забыли?
Овуляха, дрочащая на мраморную говядину, приседания с нагрузкой и чрезмерное чсв, выражающееся в "программировании" конечных автоматов на хачкиле О БОЖЕ На хачкиле в середине проебанных нулевых. Что мы там забыли?
>>1079140
Из всего FP-community в жж это самое мерзкое и твердолобое хамло, хуже максимки, хуже вообще всего.
Из всего FP-community в жж это самое мерзкое и твердолобое хамло, хуже максимки, хуже вообще всего.
>>1079570
Он написал больше кода чем ты напишешь за всю жизнь. И не на джаве какой-нибудь, а на эрланге.
Он написал больше кода чем ты напишешь за всю жизнь. И не на джаве какой-нибудь, а на эрланге.
>>1079642
Так это как раз валидация. Тестирование здесь ни при чём. Тестирование призвано проверить формализованные требования.
>Вот этим
Так это как раз валидация. Тестирование здесь ни при чём. Тестирование призвано проверить формализованные требования.
>>1079775
Максим-петух (и пропессор-петух) ничего не добились ни в функциональном программировании, ни в om/exe, ни в монетизации своего "доказательного программирования". Лохи и чмыри.
>Он написал больше кода чем ты напишешь за всю жизнь. И не на джаве какой-нибудь, а на эрланге.
Максим-петух (и пропессор-петух) ничего не добились ни в функциональном программировании, ни в om/exe, ни в монетизации своего "доказательного программирования". Лохи и чмыри.
>>1079882
Максим зарабатывает программированием не работая ни на кого, и используя только Эрланг. Среди его клиентов ПриватБанк. Так чего он там не добился? И чего добился ты?
Максим зарабатывает программированием не работая ни на кого, и используя только Эрланг. Среди его клиентов ПриватБанк. Так чего он там не добился? И чего добился ты?
>>1079902
Зефиров в блоге общается очень корректно со всеми, и с других требует того же. По крайней мере я не замечал. Это у какого-то завистника подгорело.
Зефиров в блоге общается очень корректно со всеми, и с других требует того же. По крайней мере я не замечал. Это у какого-то завистника подгорело.
>>1079913
1. намдак тонпа не зарабатывает деньги. он в долгах сейчас, как в шелках
2. турки его кинули (причем дважды)
3. приватбанк всё.
4. его эрланг-консалтинг никто не покупает. раньше покупали его Java консалтинг, потом нашли людей посговорчивее.
5. у него не осталось клиентов.
1. намдак тонпа не зарабатывает деньги. он в долгах сейчас, как в шелках
2. турки его кинули (причем дважды)
3. приватбанк всё.
4. его эрланг-консалтинг никто не покупает. раньше покупали его Java консалтинг, потом нашли людей посговорчивее.
5. у него не осталось клиентов.
195 Кб, 400x400
Почему любой тред про функциональное программирование на этой параше непременно скатывается в срач про максимку?
>>1079945
Мне плевать что сейчас. Он заработал, продвинулся, протолкал тему. Запилил свой фреймворк, и не какое-то МВЦ-поделие. Так чего он не добился? И чего добился ты? Смотрю ты за слова не отвечаешь совсем. Значит балабол. С чего бы тебя воспринимать вообще как полноценного. И еще, откуда тебе все про него известно? Нравится считать чужие деньги? Походу сам ты на пособии, и только желчью брызшешь на других. Завистник короче.
Мне плевать что сейчас. Он заработал, продвинулся, протолкал тему. Запилил свой фреймворк, и не какое-то МВЦ-поделие. Так чего он не добился? И чего добился ты? Смотрю ты за слова не отвечаешь совсем. Значит балабол. С чего бы тебя воспринимать вообще как полноценного. И еще, откуда тебе все про него известно? Нравится считать чужие деньги? Походу сам ты на пособии, и только желчью брызшешь на других. Завистник короче.
>>1079913 Довелось общаться с инсайдерами.
Вот здесь жирный такой пиздеж - преувеличение.
>Среди его клиентов ПриватБанк
Вот здесь жирный такой пиздеж - преувеличение.
Скандалы, интриги, расследования!
>>1079962
Но это же только плюс. Кому нужны 3д
Но это же только плюс. Кому нужны 3д
>>1080133
Ньет, не Павлом. Не впутывайте меня в ваши разборки.
Ньет, не Павлом. Не впутывайте меня в ваши разборки.
>>1079952
N2O - это параша, которую даже в Erlang-комьюнити никто не использует. Или там у него ещё что-то было?
>Запилил свой фреймворк
N2O - это параша, которую даже в Erlang-комьюнити никто не использует. Или там у него ещё что-то было?
https://maxim.livejournal.com/329076.html?thread=1436020#t1436020
Пришел с работы лег спать, говорю жене, перестань шибуршать дай поспать. Тут все и началось: ах тебе спасть, я с ребенком зашиваюсь а тебе спать, хуй тебе а не спать. Я говорю: если ты не успокоишься и не даш мне уснуть, то я тебе скажу такое после чего ты будешь плакать. Заплакала и расцарапала мне ебало (при ребенке). Ходил как лох с поцарапаным ебалом, ну ладно. Отвезла ребенка в каменец и опять начинает выйобываться. Я говорю, жена, прекрати, тут ребенка нету могу и здачи дать. После щелбана (юридическая формулировка: "бил по голове"), опять пыталась расцарапать ебало, дал подсрачника и плюнул в лицо. Ну а дальше пошли заявы, бульбуляторы, родители, брат, сват, хуй, пизда.
Пришел с работы лег спать, говорю жене, перестань шибуршать дай поспать. Тут все и началось: ах тебе спасть, я с ребенком зашиваюсь а тебе спать, хуй тебе а не спать. Я говорю: если ты не успокоишься и не даш мне уснуть, то я тебе скажу такое после чего ты будешь плакать. Заплакала и расцарапала мне ебало (при ребенке). Ходил как лох с поцарапаным ебалом, ну ладно. Отвезла ребенка в каменец и опять начинает выйобываться. Я говорю, жена, прекрати, тут ребенка нету могу и здачи дать. После щелбана (юридическая формулировка: "бил по голове"), опять пыталась расцарапать ебало, дал подсрачника и плюнул в лицо. Ну а дальше пошли заявы, бульбуляторы, родители, брат, сват, хуй, пизда.
Но это была прежняя жена - Лена, которой он заделал ребенка, развелся и не платит алименты годами. Новая жена - Мария, вот с ней тоже собрался расставаться. Запасайтесь попкорном, эрлангисты!
>>1080207
Чет в голос с успешной работы, после которой можно только приползти и отсыпаться. И денег на лименты не хватает. Успех.
Чет в голос с успешной работы, после которой можно только приползти и отсыпаться. И денег на лименты не хватает. Успех.
>>1080232
А что такого? Иногда хочется просто прийти домой и лечь спать, если допоздна сидел, например. Вполне нормальное желание, тем более в описанном контексте.
А что такого? Иногда хочется просто прийти домой и лечь спать, если допоздна сидел, например. Вполне нормальное желание, тем более в описанном контексте.
>>1080236
Сидение допоздна - переработки, которые у меня мало ассоциируются с работой мечты.
Сидение допоздна - переработки, которые у меня мало ассоциируются с работой мечты.
>>1080243
Вовсе нет - график же свободный. Я, бывало, часто приходил после обеда и сидел до ночи, например.
> Сидение допоздна - переработки
Вовсе нет - график же свободный. Я, бывало, часто приходил после обеда и сидел до ночи, например.
>>1080352
Ну, он как бы один конкретный случай описывал, а не каждый день\вечер.
Ну, он как бы один конкретный случай описывал, а не каждый день\вечер.
>>1080150
Можно подумать ты имеешь отношение к Эрланг сообществу. Если чё у N2O больше звезд на гитхабе чем у любого фреймворка на Эрланге. Если мне не изменяет память N2O в десятке крупнейших эрланг проектов. На Эрланге же больше ничего никто не написал.
>>1080174
Да, твое мнение конечно же авторитетное, ты всё знаешь. А если серьезно, то откуда тебе знать?
Можно подумать ты имеешь отношение к Эрланг сообществу. Если чё у N2O больше звезд на гитхабе чем у любого фреймворка на Эрланге. Если мне не изменяет память N2O в десятке крупнейших эрланг проектов. На Эрланге же больше ничего никто не написал.
>>1080174
>Да. И приватбанк не использует ничего из его эрланг говна.
Да, твое мнение конечно же авторитетное, ты всё знаешь. А если серьезно, то откуда тебе знать?
>>1080232
Это Эрланг, детка. Впрочем, может, и хватает, просто зол на жену и не платит алименты.
>И денег на лименты не хватает.
Это Эрланг, детка. Впрочем, может, и хватает, просто зол на жену и не платит алименты.
>>1080389
Павел много чего рассказывал и про Макса, и про семью, и про поделки Макса в приватбанке.
>А если серьезно, то откуда тебе знать?
Павел много чего рассказывал и про Макса, и про семью, и про поделки Макса в приватбанке.
590 Кб, webm, 640x360, 0:06
Напомните мне что значит сладкий хлебушек и золотце? Давно тут не был.
Алсо кто такой максимка, чем знаменит? Нашел только как он срется с каким-то чуваком которому шкуры не дают и распечатал КОК на буамаге.
Алсо кто такой максимка, чем знаменит? Нашел только как он срется с каким-то чуваком которому шкуры не дают и распечатал КОК на буамаге.
>>1080519
Не знаю Павла. Не знаю лично Максима, хотя переписывался с ним по одному делу. К слову он был очень честен. Хотя меня раздражает его поведение в блоге, маты, оскорбления, напыщенность.
Не хочу лезть в чужую жизнь. Что и тебе советую. Ты только себе хуже делаешь. Развиваешь в себе ненависть, зависть, все негативные качества. Потом мучиться будешь от себя самого.
Не знаю Павла. Не знаю лично Максима, хотя переписывался с ним по одному делу. К слову он был очень честен. Хотя меня раздражает его поведение в блоге, маты, оскорбления, напыщенность.
Не хочу лезть в чужую жизнь. Что и тебе советую. Ты только себе хуже делаешь. Развиваешь в себе ненависть, зависть, все негативные качества. Потом мучиться будешь от себя самого.
>>1080207
Перечитав вот это, я понял, что никогда не буду жениться. И всем программистам буду советовать никогда не жениться, давая ссылку на тот коммент Максима.
> Пришел с работы лег спать, говорю жене, перестань шибуршать дай поспать. Тут все и началось: ах тебе спасть, я с ребенком зашиваюсь а тебе спать, хуй тебе а не спать. Я говорю: если ты не успокоишься и не даш мне уснуть, то я тебе скажу такое после чего ты будешь плакать. Заплакала и расцарапала мне ебало (при ребенке). Ходил как лох с поцарапаным ебалом, ну ладно. Отвезла ребенка в каменец и опять начинает выйобываться. Я говорю, жена, прекрати, тут ребенка нету могу и здачи дать. После щелбана (юридическая формулировка: "бил по голове"), опять пыталась расцарапать ебало, дал подсрачника и плюнул в лицо. Ну а дальше пошли заявы, бульбуляторы, родители, брат, сват, хуй, пизда.
Перечитав вот это, я понял, что никогда не буду жениться. И всем программистам буду советовать никогда не жениться, давая ссылку на тот коммент Максима.
>>1080567
Ведь это жены виноваты в том, что вышли замуж за тупого агрессивного детсадовца.
>Перечитав вот это, я понял, что никогда не буду жениться
Ведь это жены виноваты в том, что вышли замуж за тупого агрессивного детсадовца.
>>1080207
Потому что мало кто понимает, что отношения это не работа, а аскеза.
>Сначала прошла любовь, потом начало пропадать и сотрудничество.
Потому что мало кто понимает, что отношения это не работа, а аскеза.
>>1080569
Сложно сказать, кто виноват.
Максим, якобы "самый лучший Erlang-программист Украины, звезда":
https://www.facebook.com/namdak.tonpa
Вроде не детсадовец и не агрессор, а буддист:
https://www.youtube.com/watch?v=E_at53wDH1w
https://www.youtube.com/watch?v=mm7m3JOiSt8
https://www.youtube.com/watch?v=vnymtEeYTjE
https://www.youtube.com/watch?v=UjjuCRlS-bA
Вот ты можешь представить, чтобы он ударил жену первой?
Его текущая тян Маша:
https://www.facebook.com/mariya.korobetska
Прошлая жена - Лена (которая расцарапала ему лицо), от Максима у нее 14-летняя дочка, которой он не платил и не платит алименты. Найти прошлую жену в Facebook не смог, но, скорее всего, вот она из КаменцаПодольского: https://www.facebook.com/profile.php?id=100009636430348
Кто виноват, прошлая жена или он, сказать сложно.
>Ведь это жены виноваты в том, что вышли замуж за тупого агрессивного детсадовца.
Сложно сказать, кто виноват.
Максим, якобы "самый лучший Erlang-программист Украины, звезда":
https://www.facebook.com/namdak.tonpa
Вроде не детсадовец и не агрессор, а буддист:
https://www.youtube.com/watch?v=E_at53wDH1w
https://www.youtube.com/watch?v=mm7m3JOiSt8
https://www.youtube.com/watch?v=vnymtEeYTjE
https://www.youtube.com/watch?v=UjjuCRlS-bA
Вот ты можешь представить, чтобы он ударил жену первой?
Его текущая тян Маша:
https://www.facebook.com/mariya.korobetska
Прошлая жена - Лена (которая расцарапала ему лицо), от Максима у нее 14-летняя дочка, которой он не платил и не платит алименты. Найти прошлую жену в Facebook не смог, но, скорее всего, вот она из КаменцаПодольского: https://www.facebook.com/profile.php?id=100009636430348
Кто виноват, прошлая жена или он, сказать сложно.
>>1080410
Опенсорс, известность и резюме - это "олимпиада для дебилов"? Иди уроки делай.
>Если ты победил в олимпиаде для дебилов
Опенсорс, известность и резюме - это "олимпиада для дебилов"? Иди уроки делай.
>>1080577
На самом деле вопрос уровня "вот ты можешь представить, чтобы эта ламповая няша сосала нигерские хуи на камеру?", ну ты понял.
Но вообще это все домдва какой-то, меня пиздец как бесят все эти ебаные тусовочки, жжешечки, кто с кем ебется, кто кого пиздит, фу блядь, пиздец. Вот почему я могу следить за кучей англоязычных пиплов и знать, над чем они работают, где живут, где учатся и все такое, плюс в исключительных случаях знать их позиции по каким-то политическим\общественным вопросам, но при этом я ни разу, ни разу блядь никакой подобной хуйни не слышал и не читал, почему блядь
славщит ебаный
>Вот ты можешь представить, чтобы он ударил жену первой?
На самом деле вопрос уровня "вот ты можешь представить, чтобы эта ламповая няша сосала нигерские хуи на камеру?", ну ты понял.
Но вообще это все домдва какой-то, меня пиздец как бесят все эти ебаные тусовочки, жжешечки, кто с кем ебется, кто кого пиздит, фу блядь, пиздец. Вот почему я могу следить за кучей англоязычных пиплов и знать, над чем они работают, где живут, где учатся и все такое, плюс в исключительных случаях знать их позиции по каким-то политическим\общественным вопросам, но при этом я ни разу, ни разу блядь никакой подобной хуйни не слышал и не читал, почему блядь
славщит ебаный
>>1080389
Tоповые попенсорс эрланг проекты это
cowboy
rabbitmq-server
couchdb
ejabberd
mongoose
hackney/ibrowse
lager
ranch
amoveo
и т.д.
и н2о параши в заисимостях у них нет
Насчет закрытых проектов типа вотсапа я не знаю, но например в basho никакой н2о не используется.
OCHE TOLSTO
В эрланге действительно никогда не было нормального веб-фреймворка (чикакогобосс и прочие мочивебы - говно же), что обясняется тем, что в мире эрланга они вообще не нужны, потому что там таким не занимаются. Так что на безрыбьи у махимки действительно был шанс, который он успешно просрал.
Tоповые попенсорс эрланг проекты это
cowboy
rabbitmq-server
couchdb
ejabberd
mongoose
hackney/ibrowse
lager
ranch
amoveo
и т.д.
и н2о параши в заисимостях у них нет
Насчет закрытых проектов типа вотсапа я не знаю, но например в basho никакой н2о не используется.
>На Эрланге же больше ничего никто не написал
OCHE TOLSTO
В эрланге действительно никогда не было нормального веб-фреймворка (чикакогобосс и прочие мочивебы - говно же), что обясняется тем, что в мире эрланга они вообще не нужны, потому что там таким не занимаются. Так что на безрыбьи у махимки действительно был шанс, который он успешно просрал.
>>1080601
Нитроген по популярности он таки обошел. Идеология N2O как и Нитрогена интересная, но с доками беда. Нитроген кажется древним, да и не поддерживается вроде уже давно. N2O хотел потрогать, но ничего не понял, а спрашивать в их гиттере бесполезно. Там 2,5 программиста, и те не особо дружелюбны.
Нитроген по популярности он таки обошел. Идеология N2O как и Нитрогена интересная, но с доками беда. Нитроген кажется древним, да и не поддерживается вроде уже давно. N2O хотел потрогать, но ничего не понял, а спрашивать в их гиттере бесполезно. Там 2,5 программиста, и те не особо дружелюбны.
>>1080587
Проиграл. Я тут недавно решил подписаться на твиттеры всех топ программеров и экспертов (Скит, Буч и т.п.). Думал буду читать умные мысли по программированию - хуй там! Оказалось все их твиты состоять чуть более чем полностью про плохого трампа, феминизм, и угнетённых черножопых нелегалов.
>плюс в исключительных случаях знать их позиции по каким-то политическим\общественным вопросам
Проиграл. Я тут недавно решил подписаться на твиттеры всех топ программеров и экспертов (Скит, Буч и т.п.). Думал буду читать умные мысли по программированию - хуй там! Оказалось все их твиты состоять чуть более чем полностью про плохого трампа, феминизм, и угнетённых черножопых нелегалов.
>>1080601
V erlange teper' est' odin normalnij web-framewok i on nazivaetsya Phoenix.
V erlange teper' est' odin normalnij web-framewok i on nazivaetsya Phoenix.
>>1080389
https://github.com/search?o=desc&q=language:+erlang&s=stars&type=Repositories&utf8=✓
Я говорил что Макс- пиздабол? Походу и группи у него такие же.
https://github.com/search?o=desc&q=language:+erlang&s=stars&type=Repositories&utf8=✓
Я говорил что Макс- пиздабол? Походу и группи у него такие же.
>>1080714
Что это? Там же всё мертвое. А чё всего 242 репа? Значит правда на Эрланге никто не пишет.
Что это? Там же всё мертвое. А чё всего 242 репа? Значит правда на Эрланге никто не пишет.
>>1080714
Ты не понял, мне нравится Эрланг. Но почему на нем никто не пишет? Почему нет проектов, сообщества, инфы? Проще Эликсир заюзать, хоть он мне и не нравится.
Ты не понял, мне нравится Эрланг. Но почему на нем никто не пишет? Почему нет проектов, сообщества, инфы? Проще Эликсир заюзать, хоть он мне и не нравится.
Elita - Huita.
>>1080892
Как будто хаскель или лисп не ученые писали.
Как будто хаскель или лисп не ученые писали.
>>1080577
Они там просто все высокопримативные ЧСВшные пидорасы.
Мы с моей тянкой хоть и спорим, бывает, но я не настаиваю ни на чем и занимаю примирительную позицию, ведь все тлен, и когда мы сдохнем, не будет иметь значения, кто как жил и какую точку зрения защищал.
>У меня бывает, что я спорю, ругаюсь (в определенной степени), но потом быстро отхожу и могу понять, что продолжал защищать свою точку зрения или поступок, просто потому что не хотел отступать ("проиграть") - хотя и был не прав.
Они там просто все высокопримативные ЧСВшные пидорасы.
Мы с моей тянкой хоть и спорим, бывает, но я не настаиваю ни на чем и занимаю примирительную позицию, ведь все тлен, и когда мы сдохнем, не будет иметь значения, кто как жил и какую точку зрения защищал.
>>1080577
ЛОЛ.
Ответ очевиден.
Ситуация непросто тепична.
Она АРХИТИПИЧНА.
Ты бы себе на ус намотал, на будущее пригодится.
Дабы таких глупых ошибок не совершать.
Посмотри сколько у нас "матерей одиночек", ты думаешь это все плохое стечение обстоятельств?
С этими животными вменяемый человек дел иметь не станет.
>Кто виноват, прошлая жена или он, сказать сложно.
ЛОЛ.
Ответ очевиден.
Ситуация непросто тепична.
Она АРХИТИПИЧНА.
Ты бы себе на ус намотал, на будущее пригодится.
Дабы таких глупых ошибок не совершать.
Посмотри сколько у нас "матерей одиночек", ты думаешь это все плохое стечение обстоятельств?
С этими животными вменяемый человек дел иметь не станет.
>>1080946
У бабы "любовь прошла", завяли цветочки, она стала подсирать своему мужу. Предавать на регулярной основе, вероятно и любовника завела.
Ну и включила режим выведения мужика из себя, чтобы свалить на него ответственность - мол это он сам захотел расстаться, это ОН все виноват.
Это тип не очевидно?
Но муж, несмотря на то, что лох знатный, оказался все-же не доконца лохом, и включил пофигизм - "отьебись женщина, не до тебя", что выбивалось из планов жены, ей нужно было стать жертвой, отсюда неадекватность реакции, она заранее спланировала что и как будет делать.
Касательно ребенка, я так понял, муж его никогда не хотел, значит это было решение жены - сознательно залетела. Или они на этой почве женились - и муж редкий лох.
Или она его в процессе завела, то-же не очень понятно.
А может ребенок и не мужа даже.
Ну и классически жена использует ребенка для шантажа мужчины.
Задай себе такой вопрос, если ребенок это так тяжело и затратно, почему ни в данном случае, ни вообще во всей истории совка, нет случая, чтобы женщина САМА пыталась спихнуть опекунство на мужчину?
Не алименты требовать, не совместное воспитание, и прочую дичь, а просто скинуть ребенка со своей шеи?
Как же можно, любовь материнство, ага, лол.
А максимка этот, просто слишком большой пофигист, плывет по течению так сказать, "буддист".
Сам он считает конечно, что его никогда ничто не заденет, но на самом деле, дела обстоят иначе, и подобная жена подобного мужа легко сводит в могилу, как семечку щелкнуть.
Мужик уже с раком лежит в операционной, и все думает какой, он классный пофигист и как его ничего не волнует.
>Так в чем причина драмы и кто из них животное?
У бабы "любовь прошла", завяли цветочки, она стала подсирать своему мужу. Предавать на регулярной основе, вероятно и любовника завела.
Ну и включила режим выведения мужика из себя, чтобы свалить на него ответственность - мол это он сам захотел расстаться, это ОН все виноват.
Это тип не очевидно?
Но муж, несмотря на то, что лох знатный, оказался все-же не доконца лохом, и включил пофигизм - "отьебись женщина, не до тебя", что выбивалось из планов жены, ей нужно было стать жертвой, отсюда неадекватность реакции, она заранее спланировала что и как будет делать.
Касательно ребенка, я так понял, муж его никогда не хотел, значит это было решение жены - сознательно залетела. Или они на этой почве женились - и муж редкий лох.
Или она его в процессе завела, то-же не очень понятно.
А может ребенок и не мужа даже.
Ну и классически жена использует ребенка для шантажа мужчины.
Задай себе такой вопрос, если ребенок это так тяжело и затратно, почему ни в данном случае, ни вообще во всей истории совка, нет случая, чтобы женщина САМА пыталась спихнуть опекунство на мужчину?
Не алименты требовать, не совместное воспитание, и прочую дичь, а просто скинуть ребенка со своей шеи?
Как же можно, любовь материнство, ага, лол.
А максимка этот, просто слишком большой пофигист, плывет по течению так сказать, "буддист".
Сам он считает конечно, что его никогда ничто не заденет, но на самом деле, дела обстоят иначе, и подобная жена подобного мужа легко сводит в могилу, как семечку щелкнуть.
Мужик уже с раком лежит в операционной, и все думает какой, он классный пофигист и как его ничего не волнует.
>>1080916
Подсрачник даёшь, плюёшь в лицо, когда шибуршит и не даёт поспать после работы?
>Мы с моей тянкой
Подсрачник даёшь, плюёшь в лицо, когда шибуршит и не даёт поспать после работы?
>>1080918
Так объясни нам, почему их так много.
То есть женщинам в Украине нравится делать детей от одного (Максима-буддиста), а потом разводиться и искать другого мужа?
>Посмотри сколько у нас "матерей одиночек", ты думаешь это все плохое стечение обстоятельств?
Так объясни нам, почему их так много.
>С этими животными вменяемый человек дел иметь не станет.
То есть женщинам в Украине нравится делать детей от одного (Максима-буддиста), а потом разводиться и искать другого мужа?
>>1080953
Нет.
>>1080952
Да его жена изначально была жабой. Видел ее фото с ним на фоне машины. Это, конечно, субъективно, но мне она показалась очень ЧСВшной и эгоистичной. Наверно, истеричная, яркая, не на помойке себя нашла. Такие как она сжирают мужиков. Лучше бы нашел себе няшу-скромняшу, социофобную хикку, комнатную плесень и любил ее.
Нет.
>>1080952
Да его жена изначально была жабой. Видел ее фото с ним на фоне машины. Это, конечно, субъективно, но мне она показалась очень ЧСВшной и эгоистичной. Наверно, истеричная, яркая, не на помойке себя нашла. Такие как она сжирают мужиков. Лучше бы нашел себе няшу-скромняшу, социофобную хикку, комнатную плесень и любил ее.
>>1081049
В США было исследованные, и там оказалось, что ок 70% детей не от мужей в амер семьях.
Может для сливок это совсем другое соотношения, но для комон пьюпел, считай было, реальная фигура.
>>1081047
Потому, что с прожженным конченными мразями никто не хочет иметь дел, и тем более совместно жить.
Потому, что архаичный институт семьи на развалинах РИ разрушен до основания, и никаких альтернатив населению не представлено.
Потому, что эмансипация женщин даже не начиналась, и не только у нас, это проблема мировая, но у нас это особая проблема в свете жесткого социального и экономического кризиса.
В РФ то-же самое.
Другого "мужа" может и не найдет.
Нужно понимать, что ребенок это не только повод для шантажа мужчины.
Это еще социальные выплаты, и персональный раб(как это видит женщина).
Женщины стремительно стареют, особенно наши, прожженные и пропитые. И после 30 лет они уже становятся неходовым товаром. Плюс начинаются возрастные изменения, справляться с которыми они и не умеют(маменька сказала нужно рожать)
Вот и заводят детей хоть от кого, если уж мужика не нашла, так хоть ребенок о ней в старости (когда она станет отвратительной мерзкой старухой) позаботится.
Нужно понимать, что женщина ни на секунду не верит в любовь и прочую романтическую дичь, это ее социальное оружие. Ну, то есть сама себя она даже может убедить, ведь хороший лжец должен и сам в свою лож поверить, чтобы обмануть других.
Вот коли есть у нас плюмбем-фурундум, так я тебе отдам тыщу баксов. А что такое плюмбем-фурундум? Ну это брат такая тонкая материя, я ее в общем чувствую. Вот если не отдам тыщу баксов, явный признак того, что плюмбем-фурундум нету.
>То есть он не в курсе даже?! Вот это обман.
В США было исследованные, и там оказалось, что ок 70% детей не от мужей в амер семьях.
Может для сливок это совсем другое соотношения, но для комон пьюпел, считай было, реальная фигура.
>>1081047
>Так объясни нам, почему их так много.
Потому, что с прожженным конченными мразями никто не хочет иметь дел, и тем более совместно жить.
Потому, что архаичный институт семьи на развалинах РИ разрушен до основания, и никаких альтернатив населению не представлено.
Потому, что эмансипация женщин даже не начиналась, и не только у нас, это проблема мировая, но у нас это особая проблема в свете жесткого социального и экономического кризиса.
>То есть женщинам в Украине нравится делать детей от одного (Максима-буддиста), а потом разводиться и искать другого мужа?
В РФ то-же самое.
Другого "мужа" может и не найдет.
Нужно понимать, что ребенок это не только повод для шантажа мужчины.
Это еще социальные выплаты, и персональный раб(как это видит женщина).
Женщины стремительно стареют, особенно наши, прожженные и пропитые. И после 30 лет они уже становятся неходовым товаром. Плюс начинаются возрастные изменения, справляться с которыми они и не умеют(маменька сказала нужно рожать)
Вот и заводят детей хоть от кого, если уж мужика не нашла, так хоть ребенок о ней в старости (когда она станет отвратительной мерзкой старухой) позаботится.
Нужно понимать, что женщина ни на секунду не верит в любовь и прочую романтическую дичь, это ее социальное оружие. Ну, то есть сама себя она даже может убедить, ведь хороший лжец должен и сам в свою лож поверить, чтобы обмануть других.
Вот коли есть у нас плюмбем-фурундум, так я тебе отдам тыщу баксов. А что такое плюмбем-фурундум? Ну это брат такая тонкая материя, я ее в общем чувствую. Вот если не отдам тыщу баксов, явный признак того, что плюмбем-фурундум нету.
>>1081179
Мужчина в свою очередь, с возрастом только приобретает ценность.
Поэтому чем хуевее баба, там более в раннем возрасте более молодого\неопытного мужика она пытается поймать.
Стратегия для мужчины должна быть обратной.
Пока молодой ебись, но никаких семей и прочих сожительств.
>Женщины стремительно стареют, особенно наши, прожженные и пропитые. И после 30 лет они уже становятся неходовым товаром. Плюс начинаются возрастные изменения, справляться с которыми они и не умеют(маменька сказала нужно рожать)
Мужчина в свою очередь, с возрастом только приобретает ценность.
Поэтому чем хуевее баба, там более в раннем возрасте более молодого\неопытного мужика она пытается поймать.
Стратегия для мужчины должна быть обратной.
Пока молодой ебись, но никаких семей и прочих сожительств.
>>1081177
Это же ОКСИМИРОН. Скромные бабы это уродки или как минимум стремные, потому и скромные что при таких внешних данных предложить им нечего.
А максимку видно что гламурных кисок тянет (я тоже не удержался и посмотрел на его баб в фб).
>Лучше бы нашел себе няшу-скромняшу
Это же ОКСИМИРОН. Скромные бабы это уродки или как минимум стремные, потому и скромные что при таких внешних данных предложить им нечего.
А максимку видно что гламурных кисок тянет (я тоже не удержался и посмотрел на его баб в фб).
>>1081046
Диванный.
Диванный.
>>1081179
Кстати не только поэтому, у баб после родов вообще старение ускоряется, это как-то гормонами регулируется, не помню уже точно.
>Женщины стремительно стареют, особенно наши, прожженные и пропитые. И после 30 лет они уже становятся неходовым товаром.
Кстати не только поэтому, у баб после родов вообще старение ускоряется, это как-то гормонами регулируется, не помню уже точно.
>>1081185
Нихуя. Ну или как минимум это сильно преувиличено до уровня что если ты миллиардер то будть ты хоть орком но бабам понравишся.
>Мужчина в свою очередь, с возрастом только приобретает ценность.
Нихуя. Ну или как минимум это сильно преувиличено до уровня что если ты миллиардер то будть ты хоть орком но бабам понравишся.
>>1081216
Нет, конечно, если зять - нехуй взять, то он и в 20 нехуй взять, и в 30, и в 40, и в 50.
А так то у людей к 30 как раз своя квартира появляется, карьера складывается, бизнес открывается.
Да и мозгов до 30 в общем-то нет.
>Нихуя
Нет, конечно, если зять - нехуй взять, то он и в 20 нехуй взять, и в 30, и в 40, и в 50.
А так то у людей к 30 как раз своя квартира появляется, карьера складывается, бизнес открывается.
Да и мозгов до 30 в общем-то нет.
>>1081210
А ви загчем интересетесь?
Я таки за то, чтобы воспитывать женщин так же как и мужчин, полноценными людьми, а не - математика не для девочек, спорт не для девочек, армия не для девочек, девочки слабые, девочки играют в куклы, нужно рожать, наносить на себя килограммы косметики и каблуки и вырез до пупка, ты же товар, демонстрируй себя. И прочее прочее говно.
А ви загчем интересетесь?
Я таки за то, чтобы воспитывать женщин так же как и мужчин, полноценными людьми, а не - математика не для девочек, спорт не для девочек, армия не для девочек, девочки слабые, девочки играют в куклы, нужно рожать, наносить на себя килограммы косметики и каблуки и вырез до пупка, ты же товар, демонстрируй себя. И прочее прочее говно.
>>1081225
Я о том и говорю, у тебя слишком бинарно - или нехуй взять или бизнес на миллионы. Даже для толковых прогеров потолок тыщ 200 по текущему курсу. Такими доходами ты нихуя не будешь выделяться среди ерох, который на своем заводе, пусть не за пару лет, но за 5 такую же тачку купят. Но у тебя при этом как был, так и останется жирный минус в глазах баб - ты не ероха.
Я о том и говорю, у тебя слишком бинарно - или нехуй взять или бизнес на миллионы. Даже для толковых прогеров потолок тыщ 200 по текущему курсу. Такими доходами ты нихуя не будешь выделяться среди ерох, который на своем заводе, пусть не за пару лет, но за 5 такую же тачку купят. Но у тебя при этом как был, так и останется жирный минус в глазах баб - ты не ероха.
>>1081229
Так и есть. От недостатка тестостерона они не могут в мышечную массу.
>спорт не для девочек, армия не для девочек, девочки слабые
Так и есть. От недостатка тестостерона они не могут в мышечную массу.
>>1081229
Так это щас всё и происходит, только за счет квот, предоставления необоснованных преференций и запрета на критику баб.
Так это щас всё и происходит, только за счет квот, предоставления необоснованных преференций и запрета на критику баб.
>>1081233
Это У МЕНЯ бинарно? Охуеть.
А в твоем НЕ БИНАРНОМ мозге умещается бизнес на тысячи?
Или зп в 3K$? Мы тут как бы программаче, не?
Тебе лет 15?
Тут именно у тебя бинарное мышление загнанное в узкие рамки скотских стереотипов, в совокупности с обидой на весь мир.
>Я о том и говорю, у тебя слишком бинарно - или нехуй взять или бизнес на миллионы.
Это У МЕНЯ бинарно? Охуеть.
А в твоем НЕ БИНАРНОМ мозге умещается бизнес на тысячи?
Или зп в 3K$? Мы тут как бы программаче, не?
>ерох
>останется жирный минус в глазах баб - ты не ероха.
Тебе лет 15?
Тут именно у тебя бинарное мышление загнанное в узкие рамки скотских стереотипов, в совокупности с обидой на весь мир.
>>1081234
Да все они могут.
https://www.youtube.com/watch?v=llHhiiNnIjY
Ты еще скажи что женщины никогда не стирали и не убирали в доме, не пользовали чугунные сковородки.
Это нихуя не легкая нагрузка знаешь ли.
>Так и есть. От недостатка тестостерона они не могут в мышечную массу.
Да все они могут.
https://www.youtube.com/watch?v=llHhiiNnIjY
Ты еще скажи что женщины никогда не стирали и не убирали в доме, не пользовали чугунные сковородки.
Это нихуя не легкая нагрузка знаешь ли.
>>1081236
Нет, не происходит.
Происходит создание видимости, и превращение мерзких животных в еще более мерзких животных.
То же самое что выплачивать безработным нигерам пособие, вместо того чтобы делать из них приличных членов общества.
Об этом Трамп на дебатах говорил, мол мы за то, чтобы дать людям работу, а не использовать их бедность и бичовость для создания себе электората неполноценных уродов.
>Так это щас всё и происходит, только за счет квот, предоставления необоснованных преференций и запрета на критику баб.
Нет, не происходит.
Происходит создание видимости, и превращение мерзких животных в еще более мерзких животных.
>преференций и запрета на критику баб
То же самое что выплачивать безработным нигерам пособие, вместо того чтобы делать из них приличных членов общества.
Об этом Трамп на дебатах говорил, мол мы за то, чтобы дать людям работу, а не использовать их бедность и бичовость для создания себе электората неполноценных уродов.
>>1081245
В какой такой "настоящей" европе? Ты можешь прямо ответить на вопрос, в какой стране ты живешь?
В какой такой "настоящей" европе? Ты можешь прямо ответить на вопрос, в какой стране ты живешь?
>>1081254
Человечеству нужно меняться, но 90% населения жестко этому сопротивляется.
Все эти феминистки не одевающие прокладок во время течки - не фемистки, а ебнутые не эмансипированные стервы.
И чем сильнее и стремительнее мир меняется, тем более жуткие и массовые формы будет принимать безумие неспособных к изменению масс.
В ближайшие 100 лет есть около 70% вероятности того, что человечество если не погибнет, то вернется в темные века.
>>Так это щас всё и происходит, только за счет квот, предоставления необоснованных преференций и запрета на критику баб.
>Нет, не происходит.
Человечеству нужно меняться, но 90% населения жестко этому сопротивляется.
Все эти феминистки не одевающие прокладок во время течки - не фемистки, а ебнутые не эмансипированные стервы.
И чем сильнее и стремительнее мир меняется, тем более жуткие и массовые формы будет принимать безумие неспособных к изменению масс.
В ближайшие 100 лет есть около 70% вероятности того, что человечество если не погибнет, то вернется в темные века.
>>1081240
Ебанько, учись читать или не пытайся подменять смысл. Я в сообщении явно указал к чему оно относится.
Когда говорят бизнес, естественно имеется ввиду масштаб дохода значительно превышающий работу на дядю. Иди блять клеить тянучек зарегав ИП и имея случайный заработок на пару десятков тыщ р в месяц каким нибудь вольным стрелком на 1С например. Все только будут проигрывать с такого бизнесмена.
3к баксов это меньше 200к р и хули ты этим высказыанием пытаешься опроврегнуть, когда я выше писал что до 200к р ты ничем особо не будешь выделяться, особенно в крупных городах.
Когда мне было 15, я мог ебсти твою мамку-шлюху а ты еще не родился.
На моей стороне опыт (выборка более чем репрезентативна), масштабные эксперименты на дейтингах, плюс наблюдение за большим числом коллег из нашей индустрии. И везде мои тезисы ПОЛНОСТЬЮ подтверждаются.
> то У МЕНЯ бинарно? Охуеть. А в твоем НЕ БИНАРНОМ мозге умещается бизнес на тысячи?Или зп в 3K$? Мы тут как бы программаче, не?
Ебанько, учись читать или не пытайся подменять смысл. Я в сообщении явно указал к чему оно относится.
Когда говорят бизнес, естественно имеется ввиду масштаб дохода значительно превышающий работу на дядю. Иди блять клеить тянучек зарегав ИП и имея случайный заработок на пару десятков тыщ р в месяц каким нибудь вольным стрелком на 1С например. Все только будут проигрывать с такого бизнесмена.
3к баксов это меньше 200к р и хули ты этим высказыанием пытаешься опроврегнуть, когда я выше писал что до 200к р ты ничем особо не будешь выделяться, особенно в крупных городах.
> Тебе лет 15? Тут именно у тебя бинарное мышление загнанное в узкие рамки скотских стереотипов, в совокупности с обидой на весь мир.
Когда мне было 15, я мог ебсти твою мамку-шлюху а ты еще не родился.
На моей стороне опыт (выборка более чем репрезентативна), масштабные эксперименты на дейтингах, плюс наблюдение за большим числом коллег из нашей индустрии. И везде мои тезисы ПОЛНОСТЬЮ подтверждаются.
>>1081255
Ебать дебил. Ну в википедии прочитай список стран действительных членов ЕС.
США туда же можешь добавить.
Ебать дебил. Ну в википедии прочитай список стран действительных членов ЕС.
США туда же можешь добавить.
>>1081267
Нет.
Ок.
>Когда говорят бизнес, естественно имеется ввиду масштаб дохода значительно превышающий работу на дядю.
Нет.
>Ебанько
>проигрывать
>ебсти твою мамку-шлюху
>масштабные эксперименты на дейтингах
>Мне не 15
Ок.
>>1081179
Так почему власть в США не введет обязательные тесты ДНК детей в роддомах?
>В США было исследованные, и там оказалось, что ок 70% детей не от мужей в амер семьях.
Так почему власть в США не введет обязательные тесты ДНК детей в роддомах?
>>1081068
Аргументируй. Желательно в контексте существования https://github.com/lukecheeseman/ponyta , если возвращаться от обсуждения избиения чужих жен к топику.
Аргументируй. Желательно в контексте существования https://github.com/lukecheeseman/ponyta , если возвращаться от обсуждения избиения чужих жен к топику.
>>1081179
Поясни, что за изменения и как можно справиться.
>Плюс начинаются возрастные изменения, справляться с которыми они и не умеют
Поясни, что за изменения и как можно справиться.
>>1081233
Не обязательно на Россию работать
>Даже для толковых прогеров потолок тыщ 200 по текущему курсу
Не обязательно на Россию работать
>>1081323
Так ты диванный. Ясно.
Так ты диванный. Ясно.
>>1081319
https://ru.wikipedia.org/wiki/Климакс_(физиология)
Климакс (от греч. κλῖμαξ — лестница) — период в жизни биологической особи, характеризующийся инволюцией, угасанием функции половой системы, происходящим в связи с возрастными изменениями. По отношению к женщинам также употребляют термин менопауза.
У женщин прекращается возможность иметь детей, характеризуется нерегулярностью или полным прекращением менструаций. В среднем наступает примерно в 50 лет, но это время может сильно варьироваться. Обычно протекает спокойно, но некоторые женщины переносят климакс очень тяжело, с нарушением кровяного давления, нервными расстройствами и др. С 1950-х годов стала применяться заместительная гормональная терапия, при которой используют эстроген отдельно или вместе с прогестероном, которые помогают противостоять этому состоянию
Климакс у женщин – это особый период в жизни каждой женщины, обычно в 48 ± 3 лет, сопровождается снижением уровня половых гормонов и постепенной утратой репродуктивной функции. В медицине, климакс – это цепочка физиологических событий растянутых во времени.
В разных источниках, климактерическая перестройка, длится до 10 лет. Правильная организация жизни, специальная диета, психологическая помощь, в отдельных случаях медикаментозная терапия, создают достойное качество жизни женщины, испытывающей временные трудности.
Первая проблема с которой сталкивается женщина – психологическая. В этот период замечены перемены в характере, проявляемые чрезмерной раздражительностью, мнительностью и ранимостью. Психологи единодушно признают критический возраст проблемой ближнего круга (муж, дети, внуки, коллеги). Доброжелательная, спокойная обстановка в семье, на работе, облегчает сосуществование.
>Поясни, что за изменения и как можно справиться.
https://ru.wikipedia.org/wiki/Климакс_(физиология)
Климакс (от греч. κλῖμαξ — лестница) — период в жизни биологической особи, характеризующийся инволюцией, угасанием функции половой системы, происходящим в связи с возрастными изменениями. По отношению к женщинам также употребляют термин менопауза.
У женщин прекращается возможность иметь детей, характеризуется нерегулярностью или полным прекращением менструаций. В среднем наступает примерно в 50 лет, но это время может сильно варьироваться. Обычно протекает спокойно, но некоторые женщины переносят климакс очень тяжело, с нарушением кровяного давления, нервными расстройствами и др. С 1950-х годов стала применяться заместительная гормональная терапия, при которой используют эстроген отдельно или вместе с прогестероном, которые помогают противостоять этому состоянию
Климакс у женщин – это особый период в жизни каждой женщины, обычно в 48 ± 3 лет, сопровождается снижением уровня половых гормонов и постепенной утратой репродуктивной функции. В медицине, климакс – это цепочка физиологических событий растянутых во времени.
В разных источниках, климактерическая перестройка, длится до 10 лет. Правильная организация жизни, специальная диета, психологическая помощь, в отдельных случаях медикаментозная терапия, создают достойное качество жизни женщины, испытывающей временные трудности.
Первая проблема с которой сталкивается женщина – психологическая. В этот период замечены перемены в характере, проявляемые чрезмерной раздражительностью, мнительностью и ранимостью. Психологи единодушно признают критический возраст проблемой ближнего круга (муж, дети, внуки, коллеги). Доброжелательная, спокойная обстановка в семье, на работе, облегчает сосуществование.
>>1081315
Это было бы что-то уровня конца света\избрания Хиллари Клинтон президентом.
>Так почему власть в США не введет обязательные тесты ДНК детей в роддомах?
Это было бы что-то уровня конца света\избрания Хиллари Клинтон президентом.
>>1081331
Бодипозитив.
Ну тип идешь такая, а из под юбки кровь течет, тип так природно, а прокладки придумали мужчины чтобы порабощать женщин.
>где логика? в чем прикол? смысл?
Бодипозитив.
Ну тип идешь такая, а из под юбки кровь течет, тип так природно, а прокладки придумали мужчины чтобы порабощать женщин.
>>1081336
И вот, кстати, боди-позитив-женщины являются ЛЮТЫМИ лукистками по отношению к мужчинам.
>Бодипозитив.
И вот, кстати, боди-позитив-женщины являются ЛЮТЫМИ лукистками по отношению к мужчинам.
>>1081266
Прототипы уже строят. А что?
Прототипы уже строят. А что?
>>1081318
Хули аргументировать, там такая же система типов как в Go, если ты не заметил. При том что на сайте заявлено Really type safe. На этом можно закончить.
Хули аргументировать, там такая же система типов как в Go, если ты не заметил. При том что на сайте заявлено Really type safe. На этом можно закончить.
>>1082922
Там хоть вывод типов есть? Обычно в сабтапинг-парашах худо с этим.
Там хоть вывод типов есть? Обычно в сабтапинг-парашах худо с этим.
>>1084030
Как же ты отвратителен.
Как же ты отвратителен.
Петух Пропессор, лучший друг Максима, открыл для себя Аду:
https://nponeccop.livejournal.com/580774.html
Спешите потроллеть.
https://nponeccop.livejournal.com/580774.html
Спешите потроллеть.
Тут из альтернативной вселенной http://www.spark-2014.org/about сообщают, что завтипы говно и не нужны.
Вместо этого берете язык с простыми типами и контрактами в стиле Eiffel https://www.eiffel.com/values/design-by-contract/introduction/ и скармливаете статик ассерты в http://why3.lri.fr/#users которая дальше их скармливает пруверам из списка http://why3.lri.fr/#provers
Оно и в кок конечно умеет скармливать, но пруверы для конечных теорий (типа SMT FixedSizeBitVectors) по понятным причинам и работают лучше, и точнее моделируют машинное представление.
Вместо этого берете язык с простыми типами и контрактами в стиле Eiffel https://www.eiffel.com/values/design-by-contract/introduction/ и скармливаете статик ассерты в http://why3.lri.fr/#users которая дальше их скармливает пруверам из списка http://why3.lri.fr/#provers
Оно и в кок конечно умеет скармливать, но пруверы для конечных теорий (типа SMT FixedSizeBitVectors) по понятным причинам и работают лучше, и точнее моделируют машинное представление.
>>1084313
В clojure примерно так и делают, только из коробки и библиотеками, а не экстернал хуётами.
>Вместо этого берете язык с простыми типами и контрактами в стиле Eiffel https://www.eiffel.com/values/design-by-contract/introduction/ и скармливаете статик ассерты в http://why3.lri.fr/#users которая дальше их скармливает пруверам из списка http://why3.lri.fr/#provers
В clojure примерно так и делают, только из коробки и библиотеками, а не экстернал хуётами.
>>1084346
И это чем лучше пруверов для конечны теорий? Чем лучше HoTT пруверов?
И это чем лучше пруверов для конечны теорий? Чем лучше HoTT пруверов?
бамп
>>1080750
Это нишевый тырпрайзный язык.
Это нишевый тырпрайзный язык.
>>1077629 (OP)
Ну я для себя сделал простой вывод, когда почитал статейку от автора то ли Dafny, то ли F*, в которой он строил доказательство для чего-то простого, сортировки что-ли. В статье прямым текстом говорилось - то да сё, задача сложная, я потратил несколько вечеров, положим хуй.
Ну я для себя сделал простой вывод, когда почитал статейку от автора то ли Dafny, то ли F*, в которой он строил доказательство для чего-то простого, сортировки что-ли. В статье прямым текстом говорилось - то да сё, задача сложная, я потратил несколько вечеров, положим хуй.
>>1084668
Не, походу сгустил краски, автор таки добился решения, просто то время которое ему потребовалось и то количество кода/аннотаций были просто удручающими. Если уж авторы языка столько проебались, что говорить о простых смертных.
Не, походу сгустил краски, автор таки добился решения, просто то время которое ему потребовалось и то количество кода/аннотаций были просто удручающими. Если уж авторы языка столько проебались, что говорить о простых смертных.
Мудак Тонпа.
Тред утонул или удален.
Это копия, сохраненная 13 ноября 2017 года.
Скачать тред: только с превью, с превью и прикрепленными файлами.
Второй вариант может долго скачиваться. Файлы будут только в живых или недавно утонувших тредах. Подробнее
Если вам полезен архив М.Двача, пожертвуйте на оплату сервера.
Это копия, сохраненная 13 ноября 2017 года.
Скачать тред: только с превью, с превью и прикрепленными файлами.
Второй вариант может долго скачиваться. Файлы будут только в живых или недавно утонувших тредах. Подробнее
Если вам полезен архив М.Двача, пожертвуйте на оплату сервера.