Согласитесь, что это очень незначительная по сложности функция в общей задаче.
Проверка мата это только как пример. Думается, там достаточно много разной интересной теории можно прикрутить типа всяких цепочек шагов и каких-то теорем для них, но тут скорее вопрос в целесообразности верификации для шахмат
И если не беспокоиться об эффективности, то написать её очень легко, просто перебрать все поля под боем и всё ходы короля.
Этого недостаточно. Вот пример позиции в которой любой ход короля оставляет его под шахом, но при этом мата нет, поскольку конём можно снять ладью
Ада не является языком в котором внутри которого можно выражать теоремы. Это, судя по всему, модифицированный паскаль, и система типов у неё по сравнению с haskell или agda довольно слабая. Плюс в Ариан-5 была отключена часть проверок:
...led to four variables being protected with a handler while three others, including the horizontal bias variable, were left unprotected because it was thought that they were "physically limited or that there was a large margin of safety".
при том, что в первом случае он (бизнес) получает вполне качественный результат
Очень качественный, Ariane-5, The DAO и Therac-25 передают привет. И это только из известных. Из менее известных -- откройте любой более-менее крупный проект и посмотрите сколько там багов. Вот вам для примера linux и llvm
и потому математики сбиваются в секту, которая пытается мешать всем жить.
Удобно бросаться громкими тезисами, особенно если сливаться каждый раз, когда вам указывают на их ошибочность. Вы там в соседнем посте говорили, что функциональщина на понятии "греховность" строится. Уже смогли подтвердить свои слова какой-то статьёй, или хотя бы ссылкой на википедию? Кстати, про википедию и её авторитетность. Получилось разобраться с мутабельностью в эрланге или хотя бы с тем есть ли в ФП переменные? У вас там в ещё соседней ветке спрашивают как так получается, что типы ограничивают творчество и гениальность, а тесты нет.
Вы демострируете просто поражающий уровень слепоты ко всему, что не укладывается в вашу картину мира. А то, с каким упорством вы называете остальных сектантами это отличный пример для пословицы про соринку и бревно (ну или про камни и стеклянный дом)
Например, функция проверки того, произошёл ли мат хороший кандидат на верификацию. Думается, с первого раза её трудно будет правильно написать, но если тип будет требовать доказательств, то можно не беспокоиться о том, что какой-то ход остался неучтённым
Валидация json внешняя к языку? Достаточно открыть сайт json-schema и убедиться, что подавляющее большинство валидаторов это просто библиотеки и используются внутри языка
а что если пришедшая строка прошла валидацию через jsonschema/иной вариант валидаторов входных данных? Де-факто это, между прочим, сейчас индустриальный архитектурный стандарт.
Ну то есть через бюрократический и душащий свободу аналог .parse().unwrap()?
Ещё раз: функциональный стиль программирования потому и сектантский, что базируется на понятиях "чистый" и "греховный", а греховность она именно от мутабельности
А можно статью какую-то про греховность в ФП? Я просто не очень шарю, хочу в своём пет-проекте по подсчёту факториала с помощью зигохистоморфного препроморфизма использовать
Функциональное программирование предполагает обходиться вычислением результатов функций от исходных данных и результатов других функций, и не предполагает явного хранения состояния программы.
Эта статья про лямбда-исчисление, не про то, как нужно писать на лиспе. С тем же успехом можно взять любую статью про пи-исчисление и натягивать тезис, что в языках с многопоточностью программисты всё переусложняют
Это ответ аналогичный по абсурдности предложению @Alexsey. Я-то считаю, что если ютуб закроется (реально закроется, глобально, а не "сервера деградируют"), то достаточно быстро появится другая площадка, поэтому не особо переживаю. Если говорить про сам контент, то за бесполезными видео скучать не буду, а полезные (в моём случае различные лекции/доклады), обычно, где-то дублируют
а у тех кто блокирует рекламу на youtube и возмущается насчет нее не возникает никакого диссонанса где-то на подкорке что за хранение и передачу всего этого контента гуглу надо платить неимоверные деньги и их надо откуда-то брать
А в чём должен возникать диссонанс? Если гугл выбрал бизнес-модель такую, что ютуб без рекламы/премиума не окупается, а с рекламой его смотреть не хотят, то проблема не в пользователях, а в гугле.
Наверное, если вам не нравится количество рекламы которое гугл пихает на ютуб, вам надо перестать пользоваться ютубом
Наверное, если гуглу не нравится, что люди блокируют рекламу, им стоит закрыть ютуб в целом
Борьба с халявщиками, которые приносят компании убытки, это же абсолютно нормальное поведение любой компании.
Как и борьба с рекламой, которую компании пихают во все места, это нормальное поведение любого пользователя
У меня TAPL с похожей скоростью проходился (хоть и с меньшим постоянством чем хотелось бы) и Elements of Set Theory Эндертона где-то как у вас книга Рилевской.
Совмещать с работой — ну как, есть же вечера и выходные.
У меня work-life balance в сторону работы перекошен немного. Вы, емнип, в довольно жёстких и интересных местах работали типа стартапов и HFT. Там не было такого, что какие-то сложные задачи вытесняли всё остальное?
Лямбды, по-хорошему, должны быть настолько же мощными, насколько обычные функции. В питоновских лямбдах можно писать выражения, но нельзя, в отличие от функций, циклы
Неплохо бы проверить что он выдает тот же результат что и исходный, как вам тут поможет функциональное программирование, интересно?
Тут на функциональном ЯП проверяют разные свойства сложения, тут используется система доказательств на основе теории типов для проверки того, что оптимизация не ломает код. С помощью типов можно проверять такие вещи, это просто пока очень далеко от мейнстрима
А другой AI будет проводить верификацию(доказательство) и соответствие машинного кода описанию в техзадании.Ну и, конечно, нужны будут люди, чтобы следили за такими системами.
они будут делать немного другое, что делают сейчас.
Даже просто проверить, что тех.задание формализовано правильно -- уже достаточно неподъёмная задача, кратно сложнее средних задач программиста. По сути это даже не программирование, а скорее переквалификация в математика. В качестве подтверждения своих слов, я предлагаю вам посмотреть Iris Tutorial, в частности, формальную спецификацию ticket lock и попытаться понять что там написано (всё что между Proof и Qed это доказательства, их можно пропустить). Отдельно отмечу, что на данный момент Iris это самый продвинутый фреймворк для верификации программ, то есть описывать спецификации проще пока никто не умеет
Проверка мата это только как пример. Думается, там достаточно много разной интересной теории можно прикрутить типа всяких цепочек шагов и каких-то теорем для них, но тут скорее вопрос в целесообразности верификации для шахмат
Этого недостаточно. Вот пример позиции в которой любой ход короля оставляет его под шахом, но при этом мата нет, поскольку конём можно снять ладью
Ада не является языком в котором внутри которого можно выражать теоремы. Это, судя по всему, модифицированный паскаль, и система типов у неё по сравнению с haskell или agda довольно слабая. Плюс в Ариан-5 была отключена часть проверок:
Очень качественный, Ariane-5, The DAO и Therac-25 передают привет. И это только из известных. Из менее известных -- откройте любой более-менее крупный проект и посмотрите сколько там багов. Вот вам для примера linux и llvm
Удобно бросаться громкими тезисами, особенно если сливаться каждый раз, когда вам указывают на их ошибочность. Вы там в соседнем посте говорили, что функциональщина на понятии "греховность" строится. Уже смогли подтвердить свои слова какой-то статьёй, или хотя бы ссылкой на википедию? Кстати, про википедию и её авторитетность. Получилось разобраться с мутабельностью в эрланге или хотя бы с тем есть ли в ФП переменные? У вас там в ещё соседней ветке спрашивают как так получается, что типы ограничивают творчество и гениальность, а тесты нет.
Вы демострируете просто поражающий уровень слепоты ко всему, что не укладывается в вашу картину мира. А то, с каким упорством вы называете остальных сектантами это отличный пример для пословицы про соринку и бревно (ну или про камни и стеклянный дом)
Например, функция проверки того, произошёл ли мат хороший кандидат на верификацию. Думается, с первого раза её трудно будет правильно написать, но если тип будет требовать доказательств, то можно не беспокоиться о том, что какой-то ход остался неучтённым
При достаточном бюджете -- во все.
Это попросту ложное утверждение. Зависимые типы позволяют математические теоремы доказывать. Посмотрите Software Foundations или plfa
Валидация json внешняя к языку? Достаточно открыть сайт json-schema и убедиться, что подавляющее большинство валидаторов это просто библиотеки и используются внутри языка
Ну то есть через бюрократический и душащий свободу аналог
.parse().unwrap()?А можно статью какую-то про греховность в ФП? Я просто не очень шарю, хочу в своём пет-проекте по подсчёту факториала с помощью зигохистоморфного препроморфизма использовать
1, 2, 3
1, 2, 3
Но википедия, конечно, очень авторитетная, а ФПшники это просто сектанты
Эта статья про лямбда-исчисление, не про то, как нужно писать на лиспе. С тем же успехом можно взять любую статью про пи-исчисление и натягивать тезис, что в языках с многопоточностью программисты всё переусложняют
Это ответ аналогичный по абсурдности предложению @Alexsey. Я-то считаю, что если ютуб закроется (реально закроется, глобально, а не "сервера деградируют"), то достаточно быстро появится другая площадка, поэтому не особо переживаю. Если говорить про сам контент, то за бесполезными видео скучать не буду, а полезные (в моём случае различные лекции/доклады), обычно, где-то дублируют
А в чём должен возникать диссонанс? Если гугл выбрал бизнес-модель такую, что ютуб без рекламы/премиума не окупается, а с рекламой его смотреть не хотят, то проблема не в пользователях, а в гугле.
Наверное, если гуглу не нравится, что люди блокируют рекламу, им стоит закрыть ютуб в целом
Как и борьба с рекламой, которую компании пихают во все места, это нормальное поведение любого пользователя
А как он может использоваться для учёбы?
У меня TAPL с похожей скоростью проходился (хоть и с меньшим постоянством чем хотелось бы) и Elements of Set Theory Эндертона где-то как у вас книга Рилевской.
У меня work-life balance в сторону работы перекошен немного. Вы, емнип, в довольно жёстких и интересных местах работали типа стартапов и HFT. Там не было такого, что какие-то сложные задачи вытесняли всё остальное?
Расскажете поподробнее в каком темпе изучали и как удавалось совмещать с работой?
Лямбды, по-хорошему, должны быть настолько же мощными, насколько обычные функции. В питоновских лямбдах можно писать выражения, но нельзя, в отличие от функций, циклы
Тут на функциональном ЯП проверяют разные свойства сложения, тут используется система доказательств на основе теории типов для проверки того, что оптимизация не ломает код. С помощью типов можно проверять такие вещи, это просто пока очень далеко от мейнстрима
Даже просто проверить, что тех.задание формализовано правильно -- уже достаточно неподъёмная задача, кратно сложнее средних задач программиста. По сути это даже не программирование, а скорее переквалификация в математика. В качестве подтверждения своих слов, я предлагаю вам посмотреть Iris Tutorial, в частности, формальную спецификацию ticket lock и попытаться понять что там написано (всё что между
ProofиQedэто доказательства, их можно пропустить). Отдельно отмечу, что на данный момент Iris это самый продвинутый фреймворк для верификации программ, то есть описывать спецификации проще пока никто не умеетА как они визу получали? Для H-1B и её аналогов, вроде как нужен хотя бы диплом бакалавра