https://www.kickstarter.com/projects/958692255/prometheus-wept-a-post-digital-turn-based-rpg
Выглядит интересно. Напоминает про Shadowrun, но мрачнее и жёстче. Почти соло-проект, инди до мозга костей. Но разработчик умеет get shit done, респект.
Выглядит интересно. Напоминает про Shadowrun, но мрачнее и жёстче. Почти соло-проект, инди до мозга костей. Но разработчик умеет get shit done, респект.
Kickstarter
Prometheus Wept: A Post Digital Turn Based RPG
Explore the ruins of civilization after a cyber-attack, in this turn based RPG for PC from the developer of Vigilantes.
https://arxiv.org/abs/1505.03118
When causation does not imply correlation: robust violations of the Faithfulness axiom
We demonstrate that the Faithfulness property that is assumed in much causal analysis is robustly violated for a large class of systems of a type that occurs throughout the life and social sciences: control systems. These systems exhibit correlations indistinguishable from zero between variables that are strongly causally connected, and can show very high correlations between variables that have no direct causal connection, only a connection via causal links between uncorrelated variables. Their patterns of correlation are robust, in that they remain unchanged when their parameters are varied. The violation of Faithfulness is fundamental to what a control system does: hold some variable constant despite the disturbing influences on it. No method of causal analysis that requires Faithfulness is applicable to such systems.
Блин, логично. Но контринтуитивно. Вообще засада, а статья ещё 15го года.
When causation does not imply correlation: robust violations of the Faithfulness axiom
We demonstrate that the Faithfulness property that is assumed in much causal analysis is robustly violated for a large class of systems of a type that occurs throughout the life and social sciences: control systems. These systems exhibit correlations indistinguishable from zero between variables that are strongly causally connected, and can show very high correlations between variables that have no direct causal connection, only a connection via causal links between uncorrelated variables. Their patterns of correlation are robust, in that they remain unchanged when their parameters are varied. The violation of Faithfulness is fundamental to what a control system does: hold some variable constant despite the disturbing influences on it. No method of causal analysis that requires Faithfulness is applicable to such systems.
Блин, логично. Но контринтуитивно. Вообще засада, а статья ещё 15го года.
Forwarded from bravit-about
Если вдруг кто-то до сих пор не прикупил себе Haskell in Depth, то самое время: сегодня дают скидку 42% на https://www.manning.com/dotd. С той же скидкой можно заодно купить ещё три книжки: для начинающих изучать Haskell от Уила Курта (она отличная, я работал над ней в оригинале как technical proofer, и редактировал перевод на русский), для интересующихся дизайном приложений в функциональном стиле от Саши Гранина, ну и для интересующихся функциональным стилем вообще и не брезгующих при этом синтаксисом Scala от Michał Płachta.
Manning Publications
Deal of the Day
Manning is an independent publisher of computer books, videos, and courses.
https://arxiv.org/pdf/2104.13117.pdf
A Verified Decision Procedure for Orders in Isabelle/HOL
Статья безусловно крутая по нескольким причинам, но меня особо повеселило, что она на 200% эксплуатирует "класический Programming Language Theory" подход "для решения любой проблемы нужно просто сделать подходящий язык и систему типов". 😁
Итак, что же делается в статье? Упрощённо, следующее:
1. Кодируется алгоритм (decision procedure) для определения (не)консистентности системы (не)равенств (без кванторов).
1.1. Для представления неравенств, естественно, определяется язык формул с (не)равенствами.
2. Чтобы вообще поставить вопрос о верификации алгоритма, необходимо определить интерпретацию формул. Естественным образом в качестве модели используется функция валюации переменных и рефлексивное, транзитивное, антисимметричное (замкнутое) отношение.
2.1. После чего определяется отношение интерпретации между моделью и формулой.
3. Далее задаётся "абстрактная спецификация" алгоритма (который decision procedure), т.е. записывается логическая формула, которая показывает, когда система (не)равенств противоречива.
3.1. Эта формула записывается в терминах "синтаксической модели", т.е. по факту — ещё одного языка для записи отношений (в данном случае — тупо в виде множества пар, как обычно в теории множеств, но тут — на уровне синтаксиса).
3.2. После чего доказывается soundness and completeness этой спецификации, т.е. то, что синтаксическая модель будет противоречивой тогда и только тогда, когда любая другая модель будет противоречивой.
4. Между делом результат обобщается для линейных порядков, потому что до этого рассматривались только частичные порядки.
5. Далее начинается ещё более интересное. Поскольку этот алгоритм поиска противоречий (aka decision procedure) должен использоваться в системе доказательства теорем Isabelle/HOL, верить ему "на слово" нельзя (тогда ошибка в алгоритме приведёт к появлению ложных доказательств), нужно чтобы он сам возвращал доказательство наличия противоречия, которое можно будет проверить на правильность.
5.1. А это значит что?! Правильно, нам нужен язык для записи пруф-термов! И система правил вывода для него.
5.2. При наличии такого языка и системы можно доказать его полноту (и soundness) относительно "спецификации", т.е. тот факт, что вывести противоречие в этой системе можно тогда и только тогда, когда любая модель формулы будет противоречива.
5.2. Тут пришло время ещё одного обобщения. До сих пор рассматривались только нестрогие неравенства (типа
5.3. Оказывается, проблему можно решить, расширив язык формул операциями конъюнкции, дизъюнкции и отрицания!
5.4. А для нового языка нужна новая (расширенная) система правил вывода с новыми пруф-термами.
5.5. И ещё одна — для доказательства корректности преобразования между формулами.
6. В конце-концов можно всё-таки написать реализацию алгоритма поиска противоречия и доказать его корректность по отношению к спецификации.
7. И после написания некоторого количества интеграционного кода, подрубить эту реализацию к самой Isabelle/HOL.
7.1. Само собой, этот код включает ещё пару промежуточных языков, пару преобразований между ними и систему правил вывода.
Сколько языков и систем вывода было использовано в процессе — посчитайте сами, у меня что-то пальцы закончились. 😁
A Verified Decision Procedure for Orders in Isabelle/HOL
Статья безусловно крутая по нескольким причинам, но меня особо повеселило, что она на 200% эксплуатирует "класический Programming Language Theory" подход "для решения любой проблемы нужно просто сделать подходящий язык и систему типов". 😁
Итак, что же делается в статье? Упрощённо, следующее:
1. Кодируется алгоритм (decision procedure) для определения (не)консистентности системы (не)равенств (без кванторов).
1.1. Для представления неравенств, естественно, определяется язык формул с (не)равенствами.
2. Чтобы вообще поставить вопрос о верификации алгоритма, необходимо определить интерпретацию формул. Естественным образом в качестве модели используется функция валюации переменных и рефлексивное, транзитивное, антисимметричное (замкнутое) отношение.
2.1. После чего определяется отношение интерпретации между моделью и формулой.
3. Далее задаётся "абстрактная спецификация" алгоритма (который decision procedure), т.е. записывается логическая формула, которая показывает, когда система (не)равенств противоречива.
3.1. Эта формула записывается в терминах "синтаксической модели", т.е. по факту — ещё одного языка для записи отношений (в данном случае — тупо в виде множества пар, как обычно в теории множеств, но тут — на уровне синтаксиса).
3.2. После чего доказывается soundness and completeness этой спецификации, т.е. то, что синтаксическая модель будет противоречивой тогда и только тогда, когда любая другая модель будет противоречивой.
4. Между делом результат обобщается для линейных порядков, потому что до этого рассматривались только частичные порядки.
5. Далее начинается ещё более интересное. Поскольку этот алгоритм поиска противоречий (aka decision procedure) должен использоваться в системе доказательства теорем Isabelle/HOL, верить ему "на слово" нельзя (тогда ошибка в алгоритме приведёт к появлению ложных доказательств), нужно чтобы он сам возвращал доказательство наличия противоречия, которое можно будет проверить на правильность.
5.1. А это значит что?! Правильно, нам нужен язык для записи пруф-термов! И система правил вывода для него.
5.2. При наличии такого языка и системы можно доказать его полноту (и soundness) относительно "спецификации", т.е. тот факт, что вывести противоречие в этой системе можно тогда и только тогда, когда любая модель формулы будет противоречива.
5.2. Тут пришло время ещё одного обобщения. До сих пор рассматривались только нестрогие неравенства (типа
≤), в то время как нужно доказывать и для строгих (типа <).5.3. Оказывается, проблему можно решить, расширив язык формул операциями конъюнкции, дизъюнкции и отрицания!
5.4. А для нового языка нужна новая (расширенная) система правил вывода с новыми пруф-термами.
5.5. И ещё одна — для доказательства корректности преобразования между формулами.
6. В конце-концов можно всё-таки написать реализацию алгоритма поиска противоречия и доказать его корректность по отношению к спецификации.
7. И после написания некоторого количества интеграционного кода, подрубить эту реализацию к самой Isabelle/HOL.
7.1. Само собой, этот код включает ещё пару промежуточных языков, пару преобразований между ними и систему правил вывода.
Сколько языков и систем вывода было использовано в процессе — посчитайте сами, у меня что-то пальцы закончились. 😁
Forwarded from Новости синтеза доказательств
Брайан Ноузек (сооснователь OSF.io и большой активист борьбы с кризисом воспроизводимости) такое предлагает в своем твиттере: как разделить терминологию, касающуюся воспроизведения/репликации, чтобы не возникала сумятица. В частности, Мэтт Пейдж уже отписался, что они предлагаемую терминологию приняли для проекта REPRISE (https://doi.org/10.1186/s13643-021-01670-0) — крупнейшего в истории человечества исследования воспроизводимости синтезов доказательств.
А как мы это тогда по-русски бы обозвали?
* Repeatability — повторимость?
* Reproducibility — воспроизводимость?
* Robustness — реаналитическая устойчивость?
* Replicability — репликационная устойчивость?
Шарьте пост с коллегами, делитесь мнением в комментах, плз…
А как мы это тогда по-русски бы обозвали?
* Repeatability — повторимость?
* Reproducibility — воспроизводимость?
* Robustness — реаналитическая устойчивость?
* Replicability — репликационная устойчивость?
Шарьте пост с коллегами, делитесь мнением в комментах, плз…
Некоторое — уже значительное — время назад Observable проводили мастер-класс по анализу временных рядов с использованием Observable Notebooks, понятное дело. Доступны материалы — запись трансляции на YouTube и собственно ноутбуки с данными и примерами: https://observablehq.com/@observablehq/timeseries-workshop-materials
Хочу отметить, что мастер-класс был посвящён именно анализу, а не моделированию (ARIMA и т.п.) и предсказанию. При этом, основные инструменты анализа — грамотная группировка данных и подходящая визуализация. Для любителей хардкорного статистического численного анализа такой подход может показаться "детским", но тем не менее, демонстрируется пара приёмов, полезных перед применением "статистического хардкора" и после — для донесения результатов до "заинтересованных неспециалистов", в том числе в виде красивых визуализаций.
#datascience #analysis #visualization #timeseries
Хочу отметить, что мастер-класс был посвящён именно анализу, а не моделированию (ARIMA и т.п.) и предсказанию. При этом, основные инструменты анализа — грамотная группировка данных и подходящая визуализация. Для любителей хардкорного статистического численного анализа такой подход может показаться "детским", но тем не менее, демонстрируется пара приёмов, полезных перед применением "статистического хардкора" и после — для донесения результатов до "заинтересованных неспециалистов", в том числе в виде красивых визуализаций.
#datascience #analysis #visualization #timeseries
Observablehq
Workshop Materials: Analyzing Time Series Data
Introduction This three-part hands-on tutorial is based on the techniques and concepts put forth in the Analyzing Time Series Data articles. Each part guides you through implementing essential data visualization techniques for time series analysis. The live…
Зашёл в аптеку -- набрал лекарств на 4000. Как я дошёл до жизни такой?! Хочется лечь и умереть. Чувствую себя старым и разваливающимся. Ещё и колени болят...
Forwarded from Блуждающий нерв
В MIT Media Lab запущен проект по взлому сновидений. Есть первые успехи: сочетание звуковых сигналов и маски, отслеживающей стадии сна, позволяет редактировать контент сновидений. А вмешательство в контент, в принципе, может влиять на консолидацию памяти, на предпочтения бодрствующих и, как максимум, незаметно изменять черты их личности.
Светлая сторона таких разработок повернута к медицине — заманчиво так лечить фобии, депрессии, стрессовые расстройства. Или развивать творческие способности. Темной же стороной активно интересуются крупные компании, в т.ч. Microsoft. Их привлекает другая опция, ведь в сны так можно подмешивать рекламу. Например, через умные колонки.
Сами исследователи не хотели бы такой славы и написали летом открытое письмо, где призвали сочинить этику и политику в отношении технологии: «Наши сновидения не должны стать еще одной игровой площадкой для рекламодателей. Наука о мозге помогла разработать несколько технологий, вызывающих привыкание, от мобильных телефонов до социальных сетей, которые сегодня определяют большую часть нашей бодрствующей жизни; мы не хотим, чтобы то же самое произошло с нашим сном». Письмо подписали 38 ученых.
Конечно же, это не смутило бизнес. Согласно отчету Future of Marketing от Американской ассоциации маркетинга 77% опрошенных маркетологов хотели бы использовать сновидения для рекламы в ближайшие три года. Ученые вновь отреагировали, и вчера в Aeon вышел еще один текст-предостережение. С примерами и подробностями.
Сюжет до боли напоминает другую историю, о которой вы читали здесь два месяца назад: как разработчик нейроинтерфейсов призывает заранее обдумать их опасность и даже демонстрирует ее в экспериментах, чтобы всех проняло. Увы, таких сюжетов будет все больше: технологии, связанные с человеком, всегда обоюдоострые.
Светлая сторона таких разработок повернута к медицине — заманчиво так лечить фобии, депрессии, стрессовые расстройства. Или развивать творческие способности. Темной же стороной активно интересуются крупные компании, в т.ч. Microsoft. Их привлекает другая опция, ведь в сны так можно подмешивать рекламу. Например, через умные колонки.
Сами исследователи не хотели бы такой славы и написали летом открытое письмо, где призвали сочинить этику и политику в отношении технологии: «Наши сновидения не должны стать еще одной игровой площадкой для рекламодателей. Наука о мозге помогла разработать несколько технологий, вызывающих привыкание, от мобильных телефонов до социальных сетей, которые сегодня определяют большую часть нашей бодрствующей жизни; мы не хотим, чтобы то же самое произошло с нашим сном». Письмо подписали 38 ученых.
Конечно же, это не смутило бизнес. Согласно отчету Future of Marketing от Американской ассоциации маркетинга 77% опрошенных маркетологов хотели бы использовать сновидения для рекламы в ближайшие три года. Ученые вновь отреагировали, и вчера в Aeon вышел еще один текст-предостережение. С примерами и подробностями.
Сюжет до боли напоминает другую историю, о которой вы читали здесь два месяца назад: как разработчик нейроинтерфейсов призывает заранее обдумать их опасность и даже демонстрирует ее в экспериментах, чтобы всех проняло. Увы, таких сюжетов будет все больше: технологии, связанные с человеком, всегда обоюдоострые.
Для тех, кто не заметил ни сам факт, ни пост, Милевский рассказывает почему Factorio — это функциональное программирование (и категория): https://bartoszmilewski.com/2021/02/16/functorio/ 😊
Bartosz Milewski's Programming Cafe
Functorio
You might have heard people say that functional programming is more academic, and real engineering is done in imperative style. I’m going to show you that real engineering is functional, and …
https://marianoguerra.github.io/advent-of-future-of-code/
"Advent of Future of Code"
25 tasks 1 per day starting December 1st. With a twist: you have to solve it with some "Future of Code" (Low-code, Visual Programming or something) tool and record and send back your experience, especially hurdles. 😊
"Advent of Future of Code"
25 tasks 1 per day starting December 1st. With a twist: you have to solve it with some "Future of Code" (Low-code, Visual Programming or something) tool and record and send back your experience, especially hurdles. 😊
C.P. Snow’s chapter (with Norbert Wiener of Cybernetics as discussant) predicted a world where software would rule our lives, but the people who wrote the software would be outside the democratic process. He wrote, “A handful of people, having no relation to the will of society, having no communication with the rest of society, will be taking decisions in secret which are going to affect our lives in the deepest sense.”
In nineteen-fucking-sixty-one! And sixty years later here we are. 😒
From https://computinged.wordpress.com/2021/11/26/computer-science-was-always-supposed-to-be-taught-to-everyone-but-not-about-getting-a-job-a-historical-perspective/
Computing Education Research Blog
Computer Science was always supposed to be taught to everyone, and it wasn’t about getting a job: A historical perspective
I gave four keynote talks in the last two months, at SIGITE, Models 2021 Educators’ Symposium, VL/HCC, and CSERC. I’m honored to be invited to them, but I do suspect that four keynotes in six weeks…
Android: слушай, пальцами в экран тыкать -- это не твоё, лучше Ассистенту объясни голосом, что тебе надо, а?
https://osc-delft.github.io/posts/2021/11/24/open-data-and-software-in-tackling-the-climate-crisis/
Любопытная дискуссия в которой упомянули некоторые неочевидные проблемы. Интересный набор ссылок в конце. В частности, https://www.worldcommunitygrid.org/ — как старый добрый SETI@Home, но для других целей.
Любопытная дискуссия в которой упомянули некоторые неочевидные проблемы. Интересный набор ссылок в конце. В частности, https://www.worldcommunitygrid.org/ — как старый добрый SETI@Home, но для других целей.
www.worldcommunitygrid.org
Home
World Community Grid enables anyone with a computer or Android device to donate their unused computing power to advance cutting-edge scientific research on topics related to health and sustainability.