То, что Вы зовёте теоремами - простые констрейнты, ограничивающие подмножество внутри множества.
Вот это:
∀ n → n ≥ 3 → ∀ a b c → a ^ n + b ^ n ≢ c ^ n
тоже просто констрейнт?
Тип не защитит Вас от того, что Вы в этом месте напишете x > 0 вместо x >= 0.
Я вам в куче разных веток уже показывал, что защитит. Вы продолжаете твердить одно и то же из ветки в ветку, с завидным упорством игнорируя наблюдаемые данные. Как это можно назвать?
Когда наблюдаемые данные противоречат предсказаниям науки, вы меняете теорию и аксиомы.
Когда наблюдаемые данные противоречат предсказаниям богословия, вы сжигаете еретика или в лучшем случае применяете фундаментальную аксиому «пути господни неисповедимы».
Потому что подразумевается математическая логика, которая слегка отличается от богословской или ещё какой.
Кроме названий у анонимных функций, каким боком программирование может стоять близко к лямбда исчислению?
Лямбда-исчисление является моделью для программирования. Можно сформулировать язык в терминах одного из лямбда-исчислений и потом описывать его свойства, опираясь на соответствующий матаппарат.
что такое тип в программировании? Это сущность отделяющая одно значение от другого.
Нет. Это способ классификации выражений, который описывает, что с этими выражениями можно делать (или что они сами делают), а что — нельзя (или не делают).
Куски достаточно глубокой теории лежат даже тогда, когда вы обсуждаете ковариантность или контравариантность аргументов и возвращаемых значений ваших фукнций в вашей иерархии ООП-классов, или ко/контравариантность дженериков.
Но при чём здесь теория типов из математики? Ага, снова ни при чём!
Только в том случае, если вы с ней незнакомы. Но это больше говорит о вашем уровне знаний, а не о теории типов.
здесь тоже скрещивающиеся прямые: не всякий алгоритм может быть запрограммирован.
Лолшто.
Алгоритм — это практически по определению то, что может быть запрограммировано на тьюринг-полном языке.
Соответственно: математика - язык, на котором та или иная наука МОЖЕТ выражать свои выводы. А может этого не делать.
Может. Только науки без математики остались глубоко в прошлом, потому что даже современная, не знаю, биология весьма пользуется математикой (например, для построения филогенетических деревьев для анализа близости организмов, консервативности мутаций, и так далее).
Другое дело, что программирование — не наука, и программированием можно успешно заниматься (сиречь делать работу и получать за неё деньги) со школьным знанием математики. Просто неплохо при этом осознавать границы своего знания, а не рассказывать «да это всё не может быть нужно и не имеет никакого отношения».
С зарядками на каждом углу ещё очень нескоро будет хорошо.
Но да, PHEV — тема. Мой F-150 Lightning был ошибкой, так что я уже джва года жду Ram 1500 Ramcharger — пикап, батарея на 92 киловатт-часа (и пробег в овер 100 миль), генератор на 130 киловатт, 700 миль на одном заряде + баке (на магистральных скоростях будет 400, всё равно неплохо), возможность от него запитать дом целиком и использовать как резервный генератор, а не просто батареи.
Светлый демократический идеал — нет. В этом идеале люди на выборах там что-то решают и о чём-то договариваются, поэтому это куда ближе к нормальному bottom-up-процессу.
Редкий случай, когда я позволю себе де-юре проигнорировать большую часть комментария, потому что основная проблема вот здесь (и повторяется в остальных местах):
Это именно оно самое! Схема взаимодействия индивидуумов между собой. А любая схема - это инженерия. А кто там ее создал: бог/природа или человек - дело десятое.
Нет. Социальная инженерия — по определению top-down-процесс, когда узкая группа людей решает, как жить всем остальным.
И именно против таких top-down-процессов, когда приходят урбанисты (коммунисты, кто угодно), и говорят, что они решили, что я теперь должен так-то жить, я и выступаю.
Lat pulldown — 200 баксов. Набор гантелек — 200 баксов. Штанга с весами — 100 баксов. Bicep curl — 300 баксов (и только потому, что я не осилил это правильно делать со штангой, и у меня на штанге болит что-то в окрестности flexor carpi ulnaris). Leg press — 700 баксов. Pect fly — 300 баксов. Smith, самая дорогая штука, наверное — примерно 1000 баксов.
Беговую дорожку я и так покупал отдельно, потому что занимался тогда ей почти ежедневно, и её не считаю, но это ещё баксов 600.
Итого 2800 баксов. Это моя зарплата за 10 дней на самой моей низкооплачиваемой работе, когда я был позорным недоучёным-типотеоретиком, и зарплата за 3 дня, когда я был самым высокооплачиваемым быстроперекладывателем байтиков. Можно себе позволить даже на самой низкой.
Более того, я плачу за тренажерку 45 баксов в месяц. То есть, эти 2800 баксов отобьются за 5 лет, что ИМХО куда меньше срока службы этих машин.
Более того, и что ещё важнее, за эти деньги я получаю не только железо. За эти деньги по сравнению с тренажеркой я получаю возможность заниматься, когда мне удобно (хоть в 11 вечера 31-го декабря). Я получаю возможность не ждать тренажеры, особенно когда какой-нибудь клоун начинает суперсеты устраивать и занимает 4-5 тренажеров сразу. Я получаю возможность ходить в тренажерку даже тогда, когда случается очередная эпидемия, и тренажерки закрывают. Я получаю возможность пойти потягать железо, пока мой код компилируется.
Содержание этого дома стоит денег.
Как там дела со звукоизоляцией квартир от соседей?
Кстати, не знаю, что вы там в доме содержать собирались. Серьёзные траты за четыре года обладания дома — замена крыши (почти целиком оплачено страховкой, которая стоит не сильно больше таковой для квартиры), замена кое-какой сантехники (баксов 300) и добавление теплоизоляции в стены и на чердак (штукарь). Последние два необязательны.
И, кстати, сколько будет стоить утеплить стены квартиры без уменьшения жилой площади, заливая туда специальную хренотень? Больше нервов потратите на согласование с ЖКХ.
Содержание машин стоит денег.
Машины и так необходимы в не-мегаполисах.
Кстати, за сколько денег сделаете всегда доступный вам тир в вашей квартире? По местным законам, если у меня 50+ акров земли, город де-факто не может меня ограничить (а большинство городов и так не ограничивает) в том, что я делаю на своём участке, за некоторыми редкими исключениями (типа, не ближе N к границе участка). За ближайшим местом, где я могу устроить тактикул-беготню, мне надо ехать полчаса, а где я могу заниматься ночной стрельбой — часа два.
75 минут из квартиры, находящейся почти на МКАДе до офиса на другом конце города
Мне в своё время, чтобы гарантированно успеть в школу на Ленинском Проспекте к девяти, нужно было выходить из дома где-то в ВАО в 7:20. Дорога обратно занимала тоже часа полтора.
Как я и сказал, удобство себе за счет неудобства других.
Проблема в том, что вы уравниваете несколько различные неудобства. В аналогии выше вы уравниваете ваше неудобство от того, что я воспользовался вашими деньгами, и моё неудобство от того, что я не могу воспользоваться вашими деньгами. Мне такое уравнивание представляется этически нечестным.
Либо я переключаю контекст, либо тот кого я спросил.
Вам и так в любом случае надо будет переключать контекст (чтобы вопрос задать, по меньшей мере).
Но мне то интереснее сделать СВОЮ задачу быстрее.
Тогда в долгосрочной перспективе вам выгоднее, чтобы помогающий вам человек был заинтересован вам помогать, а не отвечал односложно или «мне некогда». В этом случае асинхронное общение тоже поможет.
Я бы не сказал, что поиск работы требует минимальных усилий.
Выход на гибрид для вас, очевидно, требует куда меньших усилий, чем социализация вне работы. Это прямо следует из ваших комментариев.
Тем более, других рабочих способов решить проблему никто не предложил. Только сарказм и троллинг.
Они получают удобство и ништяки за ваш счёт, тролля вас и используя вас как клоуна. В чём претензии?
Это косвенный признак того, что каждый создает свою демократию, что она рукотворна.
От того, что кто-то что натеоретизировал, оно в реальность не воплотилось. Реальная демократия (что бы это ни значило) делается многими протестующими, многими выходящими на баррикады, многими проливающими свою кровь за независимость колонии, и так далее.
Да нет же! Если бы они описывали явление, то описание было бы более менее одинаковым.
Если вы развернёте эту мысль, то увидите, что сами себе доказали, что таких явлений нет, следовательно, они (за их несуществованием) не заинженерены.
Вы даже выше написали о том, что каждый сам себе придумывает свою демократию.
И от этого она не воплощается в реальность.
Давайте, раз тут рядом так газоны обсуждают, на природу пойдём. Там есть куча разных растений (государств). Эти растения (государства) различаются по куче разных признаков — какие-то гибкие и зелёные, но низкие, какие-то твёрдые и высокие с одним стволом, какие-то в воде растут, какие-то насекомых жрут (какие-то государства расстреливают за критику правительства, в каких-то государствах людям нечего жрать, какие-то государства декларируемо гарантируют безбедную старость). Дальше можно вводить разные классы, вроде «трава», «сорняк», «кусты», «деревья» (говорят, кстати, ботаники до сих пор затрудняются формально определить дерево). Но человек, вводящий эти классы, не создаёт деревья. Линней не создал всю жизнь на земле (хотя он и описал некоторую классификацию).
Если бы ее открывали, то все было бы очень легко и скучно (как химия или физика).
Лол.
Мы, например, не знаем, кто первый придумал колесо, кто приручил лошадь или собаку - значит ли это, что данных событий не было?
Это значит, что эти события могли зависеть от многих участников, и top-down-социнженера у них не было.
Ну а так, сколько людей, столько и мнений - прямое свидетельство социального конструирования.
Социальное конструирование терминов, описывающих мир, но не самих явлений. Опять же, было бы очень здорово разделять эти вещи.
Даже у животных есть своя социальная инженерия - муравейник, волчья стая...
Это не социальная инженерия. Социальная инженерия — это когда узкая группа тем или иным образом насаждает широкой группе (обычно — всему населению) желательные для узкой группы паттерны поведения.
Это как аджайл в крупных фирмах, когда C-level officer, услышал, что от аджайла понижается число багов и time-to-market и повышается продуктивность и потенция, и форсирует внедрение «аджайла» во все команды. Это — социальная инженерия в масштабах фирмы (и обычно получается ерунда и нытьё о том, что это не нужно). Когда команда собирается и рационально решает для себя, что ей удобнее аджайл, и просит нанять ей аджайл-коуча и скам-мастера, и имеет возможность от этого легко отказаться, если поймёт, что ей не подходит — это не социальная инженерия, а свободный bottom-up-выбор.
Когда одни люди изобретают биткоин, а другие — добровольно им пользуются, это не социальная инженерия. Когда правительство говорит «больше никакого кэша, вот вам CBDC, кто пользуется кэшем — тот в тюрьму» — это социальная инженерия.
Вот это:
тоже просто констрейнт?
Я вам в куче разных веток уже показывал, что защитит. Вы продолжаете твердить одно и то же из ветки в ветку, с завидным упорством игнорируя наблюдаемые данные. Как это можно назвать?
Когда наблюдаемые данные противоречат предсказаниям науки, вы меняете теорию и аксиомы.
Когда наблюдаемые данные противоречат предсказаниям богословия, вы сжигаете еретика или в лучшем случае применяете фундаментальную аксиому «пути господни неисповедимы».
Потому что подразумевается математическая логика, которая слегка отличается от богословской или ещё какой.
Лямбда-исчисление является моделью для программирования. Можно сформулировать язык в терминах одного из лямбда-исчислений и потом описывать его свойства, опираясь на соответствующий матаппарат.
Нет. Это способ классификации выражений, который описывает, что с этими выражениями можно делать (или что они сами делают), а что — нельзя (или не делают).
Куски достаточно глубокой теории лежат даже тогда, когда вы обсуждаете ковариантность или контравариантность аргументов и возвращаемых значений ваших фукнций в вашей иерархии ООП-классов, или ко/контравариантность дженериков.
Только в том случае, если вы с ней незнакомы. Но это больше говорит о вашем уровне знаний, а не о теории типов.
Лолшто.
Алгоритм — это практически по определению то, что может быть запрограммировано на тьюринг-полном языке.
Может. Только науки без математики остались глубоко в прошлом, потому что даже современная, не знаю, биология весьма пользуется математикой (например, для построения филогенетических деревьев для анализа близости организмов, консервативности мутаций, и так далее).
Другое дело, что программирование — не наука, и программированием можно успешно заниматься (сиречь делать работу и получать за неё деньги) со школьным знанием математики. Просто неплохо при этом осознавать границы своего знания, а не рассказывать «да это всё не может быть нужно и не имеет никакого отношения».
Теслу.
Лайтнинг в гараж тупо не влазит.
С зарядками на каждом углу ещё очень нескоро будет хорошо.
Но да, PHEV — тема. Мой F-150 Lightning был ошибкой, так что я уже джва года жду Ram 1500 Ramcharger — пикап, батарея на 92 киловатт-часа (и пробег в овер 100 миль), генератор на 130 киловатт, 700 миль на одном заряде + баке (на магистральных скоростях будет 400, всё равно неплохо), возможность от него запитать дом целиком и использовать как резервный генератор, а не просто батареи.
А что же изменилось?
Светлый демократический идеал — нет. В этом идеале люди на выборах там что-то решают и о чём-то договариваются, поэтому это куда ближе к нормальному bottom-up-процессу.
На практике же зависит.
Редкий случай, когда я позволю себе де-юре проигнорировать большую часть комментария, потому что основная проблема вот здесь (и повторяется в остальных местах):
Нет. Социальная инженерия — по определению top-down-процесс, когда узкая группа людей решает, как жить всем остальным.
И именно против таких top-down-процессов, когда приходят урбанисты (коммунисты, кто угодно), и говорят, что они решили, что я теперь должен так-то жить, я и выступаю.
Это работает даже в случае той же РФ, особенно до последних 2-3 лет. Я тоже считал.
Говорят, в кружках по интересам периодически появляются новые люди, и их там вполне хотят видеть.
Нет. Изначально речь шла о том, что социализироваться можно прочими способами.
Там, где я живу — дешевле, чем в городе.
Никто не говорил, но ответ на вашу фразу «комфортная жизнь в городе дешевле» не подразумевает рассмотрение конкретно вас.
Что, гибрида недостаточно, надо 5 дней в неделю ходить?
Что именно вам непонятно и сомнительно?
Это вообще никак не отвечает на мой вопрос.
Хм…
…а почему общество должно о вас вообще задумываться и беспокоиться?
Такого снега зимой в центральном Техасе не бывает почти никогда (а когда он бывает, то двор — меньшая из ваших проблем).
Стригу газон раз в две недели. Полчаса и смешная сумма на газонокосилку.
Что там обслуживать?
Она уже сделана, что там ещё делать?
Можете за сотню баксов раз в пару лет приглашать инспектора, чтобы он это всё проверял, только смысла в этом нет.
Там, где я сейчас — столько же, сколько в городе.
В глубинке куплю себе старлинк и буду платить на 50% больше, чем сейчас. Готов пожертвовать тем, что там будет не гигабит, а 100 мегабит, скажем.
Давайте считать. Я люблю считать.
Ну чем я сейчас в тренажерке пользуюсь?
Lat pulldown — 200 баксов.
Набор гантелек — 200 баксов.
Штанга с весами — 100 баксов.
Bicep curl — 300 баксов (и только потому, что я не осилил это правильно делать со штангой, и у меня на штанге болит что-то в окрестности flexor carpi ulnaris).
Leg press — 700 баксов.
Pect fly — 300 баксов.
Smith, самая дорогая штука, наверное — примерно 1000 баксов.
Беговую дорожку я и так покупал отдельно, потому что занимался тогда ей почти ежедневно, и её не считаю, но это ещё баксов 600.
Итого 2800 баксов. Это моя зарплата за 10 дней на самой моей низкооплачиваемой работе, когда я был позорным недоучёным-типотеоретиком, и зарплата за 3 дня, когда я был самым высокооплачиваемым быстроперекладывателем байтиков. Можно себе позволить даже на самой низкой.
Более того, я плачу за тренажерку 45 баксов в месяц. То есть, эти 2800 баксов отобьются за 5 лет, что ИМХО куда меньше срока службы этих машин.
Более того, и что ещё важнее, за эти деньги я получаю не только железо. За эти деньги по сравнению с тренажеркой я получаю возможность заниматься, когда мне удобно (хоть в 11 вечера 31-го декабря). Я получаю возможность не ждать тренажеры, особенно когда какой-нибудь клоун начинает суперсеты устраивать и занимает 4-5 тренажеров сразу. Я получаю возможность ходить в тренажерку даже тогда, когда случается очередная эпидемия, и тренажерки закрывают. Я получаю возможность пойти потягать железо, пока мой код компилируется.
Как там дела со звукоизоляцией квартир от соседей?
Кстати, не знаю, что вы там в доме содержать собирались. Серьёзные траты за четыре года обладания дома — замена крыши (почти целиком оплачено страховкой, которая стоит не сильно больше таковой для квартиры), замена кое-какой сантехники (баксов 300) и добавление теплоизоляции в стены и на чердак (штукарь). Последние два необязательны.
И, кстати, сколько будет стоить утеплить стены квартиры без уменьшения жилой площади, заливая туда специальную хренотень? Больше нервов потратите на согласование с ЖКХ.
Машины и так необходимы в не-мегаполисах.
Кстати, за сколько денег сделаете всегда доступный вам тир в вашей квартире? По местным законам, если у меня 50+ акров земли, город де-факто не может меня ограничить (а большинство городов и так не ограничивает) в том, что я делаю на своём участке, за некоторыми редкими исключениями (типа, не ближе N к границе участка). За ближайшим местом, где я могу устроить тактикул-беготню, мне надо ехать полчаса, а где я могу заниматься ночной стрельбой — часа два.
Сколько стоит в городе иметь три-четыре комнаты, свой задний двор, и звукоизоляцию от соседей вместе с их собаками, детьми, вечеринками, и так далее?
В качестве задачи со звёздочкой предлагаю в обычных городских условиях найти место для аккумуляторных батарей и электрогенератора.
Пробовал. Отвратительный опыт, в ебенях лучше.
Кто в айтишечке работает на двух работах по нужде, и кто из 14-часовых работников получает почасовую оплату?
Я говорю скорее о всяких работниках в потогонных хедж-фондах.
Мне в своё время, чтобы гарантированно успеть в школу на Ленинском Проспекте к девяти, нужно было выходить из дома где-то в ВАО в 7:20. Дорога обратно занимала тоже часа полтора.
Проблема в том, что вы уравниваете несколько различные неудобства. В аналогии выше вы уравниваете ваше неудобство от того, что я воспользовался вашими деньгами, и моё неудобство от того, что я не могу воспользоваться вашими деньгами. Мне такое уравнивание представляется этически нечестным.
Вам и так в любом случае надо будет переключать контекст (чтобы вопрос задать, по меньшей мере).
Тогда в долгосрочной перспективе вам выгоднее, чтобы помогающий вам человек был заинтересован вам помогать, а не отвечал односложно или «мне некогда». В этом случае асинхронное общение тоже поможет.
Выход на гибрид для вас, очевидно, требует куда меньших усилий, чем социализация вне работы. Это прямо следует из ваших комментариев.
Они получают удобство и ништяки за ваш счёт, тролля вас и используя вас как клоуна. В чём претензии?
От того, что кто-то что натеоретизировал, оно в реальность не воплотилось. Реальная демократия (что бы это ни значило) делается многими протестующими, многими выходящими на баррикады, многими проливающими свою кровь за независимость колонии, и так далее.
Если вы развернёте эту мысль, то увидите, что сами себе доказали, что таких явлений нет, следовательно, они (за их несуществованием) не заинженерены.
И от этого она не воплощается в реальность.
Давайте, раз тут рядом так газоны обсуждают, на природу пойдём. Там есть куча разных растений (государств). Эти растения (государства) различаются по куче разных признаков — какие-то гибкие и зелёные, но низкие, какие-то твёрдые и высокие с одним стволом, какие-то в воде растут, какие-то насекомых жрут (какие-то государства расстреливают за критику правительства, в каких-то государствах людям нечего жрать, какие-то государства декларируемо гарантируют безбедную старость). Дальше можно вводить разные классы, вроде «трава», «сорняк», «кусты», «деревья» (говорят, кстати, ботаники до сих пор затрудняются формально определить дерево). Но человек, вводящий эти классы, не создаёт деревья. Линней не создал всю жизнь на земле (хотя он и описал некоторую классификацию).
Лол.
Это значит, что эти события могли зависеть от многих участников, и top-down-социнженера у них не было.
Социальное конструирование терминов, описывающих мир, но не самих явлений. Опять же, было бы очень здорово разделять эти вещи.
Это не социальная инженерия. Социальная инженерия — это когда узкая группа тем или иным образом насаждает широкой группе (обычно — всему населению) желательные для узкой группы паттерны поведения.
Это как аджайл в крупных фирмах, когда C-level officer, услышал, что от аджайла понижается число багов и time-to-market и повышается продуктивность и потенция, и форсирует внедрение «аджайла» во все команды. Это — социальная инженерия в масштабах фирмы (и обычно получается ерунда и нытьё о том, что это не нужно). Когда команда собирается и рационально решает для себя, что ей удобнее аджайл, и просит нанять ей аджайл-коуча и скам-мастера, и имеет возможность от этого легко отказаться, если поймёт, что ей не подходит — это не социальная инженерия, а свободный bottom-up-выбор.
Когда одни люди изобретают биткоин, а другие — добровольно им пользуются, это не социальная инженерия. Когда правительство говорит «больше никакого кэша, вот вам CBDC, кто пользуется кэшем — тот в тюрьму» — это социальная инженерия.