По теореме Гёделя и по фразе "Каждый раз, меняя кусочек основания, мы как будто порождаем новую математическую вселенную — со своими законами, истинами и парадоксами".
1. В 1936-м Герхард Генцен доказал непротиворечивость PA (Peano Arithmetic, арифметика первого порядка - о которой идёт речь в теореме Гёделя) в аксиоматической системе, которая не сильнее PA, но и не слабее. Все аксиомы системы в этом доказательстве, кроме специальной дополнительной, образуют аксиоматическую систему более слабую, чем PA - эту систему называют PRA (primitive recursive arithmetic) или арифметика Скулема. Эта часть аксиматики, использованной Генценом, строго слабее PA - в PA доказывается её непротиворечивость.
Однако, дополнительная аксиома - аксиома трансфинитной индукции - не доказуема в PA (иначе бы результат Генцена противоречил бы теореме Гёделя). Тем не менее имеются определённые основания "доверять" этой аксиоме (о чём чуть ниже).
Таким образом, две аксиоматические системы - PA и система, использованная Генценом для доказательства непротиворечивости PA, не сравнимы по силе - в каждой из них есть теоремы, недоказуемые в другой. "В основном" система в доказательстве Генцена проще, заковыка в дополнительной аксиоме, аксиоме трансфинитной индукции.
Вот пример арифметической теоремы, не доказуемой в PA (и факт недоказуемости - доказан в 1982-м), но доказуемой в системах с трансфинитной индукцией: теорема Гудстейна о сходимости к нолю определённых арифметических последовательностей (опубликована в 1944-м).
Следует ли из перечисленных мной фактов делать какие-либо далекоидущие выводы - решайте сами.
2. По фразе о "новой математической вселенной" - обратите внимание на направление "обратная математика" (reverse mathematics). Оказывается, многие фундаментальные теоремы доказуемы в ограниченных системах, так что - многие "новые математические вселенные" не так уж и отличны от классической.
Подробных ссылок не приводил, поскольку (с удивлением для себя) обнаружил, что многие интересные материалы по матлогике и основаниям математики отсутствуют или труднонаходимы на русском (сравнивая, например, с довольно подробными статьями в английской википедии).
Смотрю слайды (полученные через Кроссворд Тьюринга): ещё одно пересечение - Смирнов. Посмотрю видео его лекций. Кстати, модель Изинга, перколяции ("теория протекания") - неплохая тема для маткружка тоже, была книга. Библиотечка "Квант". Выпуск 19. 1982. Эфрос А.Л. Физика и геометрия беспорядка. https://math.ru/lib/bmkvant/19
Дети из местной русскоязычной диаспоры (айтишников, в основном, но не только). Друзья также преподают в дружественной англоязычной кружковской организации Prime Factor, руководительница которой Анна Бураго выпустила серию книг по ведению школьных маткружков, вот русские переводы: https://www.ozon.ru/person/burago-anna-gennadevna-70592622/category/knigi-16500/. Аня участвует в американских конференциях по кружковой тематике, в общем, богатая область - например, есть кружки по программе The Art of Problem Solving (https://artofproblemsolving.com/), есть и другие богатые материалом для продвинутых школьников книги / кружки... Есть чем увлечься на пенсии :). Да, упомяну также книгу по материалам ленинградских / петербуржских математических кружков https://archive.org/details/mathematical-circles-russian-experience - авторы недавно хорошо её обновили для нового англоязычного издания (кстати, она переводилась в разных странах). Один из авторов как раз, выйдя на пенсию, смог плотно заняться новой редакцией.
Интересно, спасибо! С моей программисткой точки зрения, несколько линков по общей тематике популяризации / обучения. Если вам не попадалось, у меня на примете (ну, например, выйду на пенсию - возможно, изучу подробно и попробую поучаствовать) сайт-коллекция open source интерактивных заметок / уроков / курсов: https://explorabl.es/ (сейчас там 180 таких элементов, построенных на разных технологиях - конфедерация энтузиастов). Такого типа уроки (на основе некой общей платформы) я встречал на https://khanacademy.org, а в последние годы на Ютубе в научно-популярных роликах рекламируют коммерческую платформу похожего вида (у них в шатате на зарплате по крайней мере один программист! :) - впрочем, у Хан Академи тоже есть программисты на ставке ) https://brilliant.org.
Нет, хотя организаторы и некоторые дополнительные преподаватели вроде меня - выпускники 239, 30, 45 (выпускавшиеся из этих школ в 80-е, и затем учившиеся на мат-мехе ЛГУ). Географически мы в Редмонде - под Сиэтлом.
Большое спассибо, очень инетересный обзор. Хотел бы поделиться опытом изложения темы на школьных математических кружках с некоторым креном на вывод уравнений для решения простых задач. Пересечение с обзором - по задаче про разорение, мы рассматриваем на кружке некоторые вариации и обсуждаем различные способы решать. Благодаря соавтору - профессиональному математику (я - программист) - оформили материал кружковских занятий как журнальную заметку и опубликовали в "Кванте":
Эта заметка существует также на arXiv.org, так что у нас есть возможность вносить в неё исправления / добавления задним числом, так что дайте, пожалуйста, знать, если найдёте в ней неточности.
Последний штрих (заглянул в нашу заметку) - мы привлекли (как механизм для решения более широкого класса задач) упоминание про марковские цепи, собственно, вынеся "цепи" в заголовок заметки.
Да, наверно, использование std:: синхронизаций в комбинации с coroutines - рискованное занятие - я, может быть, поразбираюсь после выхода C++26 с senders / receivers. По подписочным делам - возможно, какой-то хорошо отлаженный код есть в крупных корпоративных OSS библиотеках вроде abseil, folly, но наверняка я не уверен (с обоими имел только шапочное знакомство).
В примере 1, по-моему, есть риск дедлока в Emit - в случае, если коллбэк деструктуриует одну из подписок (потому как используемый механизм блокировки - не reentrant; возможно, https://en.cppreference.com/w/cpp/thread/recursive_mutex поможет эту проблему преодолеть). Если вы используете этот код, попрубуйте прогнать тест, в котором коллбэк деструктуриует одну из подписок.
Я плотно ознакомился с двумя из перечисленных книг (слушал английские аудиокниги, по несколько раз каждую, на пробежках) и составил определённое мнение. Хочу ли я читать / слушать две другие книги? На данный момент - нет, но я могу переменить своё мнение.
Нассим старше меня на 9 лет; он, как и я, эмигрант первого поколения в США, переехавший из страны "восточнее Центральной Европы" (в моём случае это Россия, в его - Ливан). На его взгляды повлиял семейный опыт переезда (бегства?) из страны, охваченной гражданской войной (однако, его перевезли родители – сужу по датам из https://en.wikipedia.org/wiki/Nassim_Nicholas_Taleb, плюс, родители обеспечили ему учёбу в University of Paris, после чего он получал MBA уже в США). Я получил образование в ЛГУ, мои формативные young adult годы пришлись на 90-е в Петербурге, и я переезжал в США и перевозил свою семью сам, когда мне было 28. Пишу об этом в плане отметить – с какой колокольни я сужу о его творчестве? – ну, какой-никакой жизненный опыт у меня тоже есть, и мы оба «белые воротнички» по первой (и в моём случае – единственной) профессии; чувствую с ним сообщность стилей мышления. Он биржевой трейдер, я программист. У нас обоих по двое детей. Существенные различия тоже есть – Нассим – уроженец влиятельной семьи ливанских интеллектуалов / госчиновников высокого уровня. Он – богат, благодаря успешной работе трейдером на Wall Street и удачному управлению собственным капиталом; эти обстоятельства позволили ему сменить профессию (биржевой трейдер, конкретно в области опционных деривативов -> “essayist, mathematical statistician, risk analyst, and aphorist”). Я пока продолжаю работать «линейным сотрудником» в софтверной корпорации, математикой немного занимаюсь только на досуге, и не часто. Потребности учить кого-либо жизни "на собственном опыте" не испытываю.
В хорошо мною изученных книгах Талеба есть интересные идеи, интеллектуальные построения, чему я отдаю должное, не углубляясь в детали. Однако, мне претят элементы нравоучительного тона «человека, который добился всего сам и знает жизнь» (says who? – потомок состоятельной / влиятельной семьи, хорошо заработавший успешными операциями на бирже, а не работой в «производящей экономике»), хотя, вероятно, я здесь несколько пристрастен.
По «антихрупкости» и skin in the game (признаюсь, с этой последней книгой я не знаком) – хотел бы отметить «антихрупкость» (“antifragile”), по определениям Нассима, существующей системы, в которой высшие менеджеры имеют золотые парашюты и практически никакой "skin in the game" уровня ответственности… Система отлично переживает кризисы, из каждого из которых руководители выходят богаче и защищеннее, чем до кризиса, и сама система крепнет! Anitfragile! Любопытно, рассматривал ли он такой парадокс в своей последней книге.
По-моему, когда вы упомянули "Koko (.NET)", вы имели в виду Koka (https://koka-lang.github.io/) - ныне этот язык отвязан от .NET: компилятор порождает бинарный код для разных платформ через промежуточное представление на C.
Моё мнение: 1. За отсутствие шага транспиляции в определённых сценариях. 2. За более натуральную интеграцию типизированных компонентов в гетерогенных проектах.
По вашей ссылке, в самом начале статьи: "The aim of this proposal is to enable developers to run programs written in TypeScript, Flow, and other static typing supersets of JavaScript without any need for transpilation, if they stick within a certain reasonably large subset of the language."
Добавлю, что, по-моему, для JS пакетов появится более натуральный способ обеспечивать бесшовную интеграции с клиентским TS кодом - в сравнении с дополнительными d.ts файлами ("typings").
Ещё один момент - любопытно, что в предложении, процитированном выше, упоминаются и TS (с которым я знаком лучше по давнему проекту), и Flow (с которым я познакомился довольно шапочно) - интерграция двух различных типизирующих надстроек JS, пусть и частичная, может быть полезна в каких-то сценариях (в проектах, в которых используются и такие и сякие компоненты). Кроме того, есть и менее популярные чем TS и Flaw, но работающие проекты типизации JS (к примеру, с одним таким проектом я планирую познакомиться на досуге - enzo).
В плане pull vs push - есть ещё опция, message queue - в смысле, producer-ы пушают, consumer-ы пуллают (но: надо поддерживать брокеров). Я тесно знаком с такой моделью с Kafka в роли message queue. Любопытно, рассматривала ли ваша команда такую опцию.
Спасибо, интересно! Однако, предлагаю не обижать std::format_to в сравнении с sprintf: для sprintf буфер аллоцируется заранее, и с той же возможностью преаллоцировать буфер имеет смысл и std::format_to померять тоже. Я из любопытства померял - плюс добавил строчку на 10 миллионов итераций - получается примерно так (новая колонка с преаллоцированным буфером для std::format_to - предпоследняя):
iterations stringstream sprintf format_to fmt_to(2) format
Интересно - однако, я не понял, как ":" поступает с типами операндов и своего результата. В примерах либо слева и справа тот же тип (целое, строка) или (более интересный второй случай) справа - вызов функции, возвращающей void, и затем ";". Второй случай намекает, что тип правого параметра диктует тип результа. Первый случай намекает, что тип левого параметра - тоже в деле. Хорошо, а если справа - целое, а слева - строка? Скорее всего, произойдет ошибка приведения типов ( хотя, можно и пофантозировать, что ошибки не будет, а типом результата будет тип-сумма целого и строки, int | string, как можно делать на TypeScript-е). А если справа и слева - пользовательские типы в каких-то отношениях subtype / supertype?
Антон, спасибо - вопрос: используется ли в этом проекте идиома / утилита fast pimpl (вы рассказывали о ней в презентации "C++ трюки из Такси" 2.5 лет назад)? Я заглянул в пару-тройку хедеров и не наткнулся на использование (пока). Предполагаю, что не используется - т.е. C++ утилита / приём весьма общего назначения, полезная в одном крупном C++ проекте, с которым вы работали, в другом крупном C++ проекте (в той же фирме) оказалась не так уж полезна?
1. "Они могли бы добавить в язык атрибуты, упрощающие контроль и за выделением/освобождением памяти, и за использованием объектов на разных уровнях приоритета, чтобы не ловить это исключительно через Driver Verifier в процессе выполнения"
и
2. "Нет, вместо этого они предпочли писать и отлаживать весь системный код на C/C++ примитивными дедовскими методами, а теперь убедили себя, что нет ничего лучше, как переписать его на Rust".
По 1: приведу один пример того, что не только могли, но и делали. Вы, наверно, никогда не сталкивались с майкрософтовским SAL (Standard Annotation Language). Этот "язык аннотаций" для C, C++ был впервые внедрён, насколько я помню, в нулевые годы - и выпускался тогда в составе DDK (Dirver Development Kit) как хороший инструмент для повышения качества third party драйверов. https://learn.microsoft.com/en-us/cpp/code-quality/understanding-sal - хотя ныне, оставаясь полезным для кода в стиле C, этот инструмент кажется мне недостаточно современным для C++ кода. Современный msvc инструментарий включает майкрософтовский статический анализатор C++ кода, синхронизованный с рекомендацими C++ Core Guidelines (и, скорее всего, некоторыми стандартными атрибутами в двойных квадратных скобках - проверю этот аспект, когда мне это будет более кстати), и, в дополнение к этому, интеграцию с анализатором clang-tidy. Visual Studio предоставляет относительно удобный UI для использования этих возможностей. VS Code поддерживает эти возможности в какой-то мере тоже (читаю сейчас блог-пост про использование clang-tidy с VS Code).
По 2: это не так, в Microsoft активно используются статические анализаторы кода и другие методы формальной верификации (выше я коснулся только отдельных примеров, как такое использование возможно при применинии msvc toolchain), вот обзорная лекция по этому вопросу (я остановил на слайде, где перечисляются такие проекты / инструменты с 2001-го по 2022-й - для верификации в основном критического кода системного уровня): https://youtu.be/GEsvGGp0jyQ?t=935. Про переписывание на Rust - это ещё один инструмент; исходная заметка, которую мы комментируем, указывает только несколько таких проектов, пока имеющих относительно маленький размах, насколько я могу судить.
Ваша история про статистику смертности в автокатастрофах в США до и после внедрения подушек безопасности меня заинтересовала! Я поискал подтверждения, но пока не нашёл.
Нашёл вот такой график. Внедрение подушек безопасности происходило между примерно второй половиной 80-х (всё более широкое внедрение технологии, продолжавшей совершенствоваться; закон был принят в 1991-м, с отложенным вступлением в силу) и 1998-м годом (закон полностью вступил в силу). Красная кривая (смерти на милю) шла вниз, но не драматично (заметен небольшой зубец более резкого падения около 1992-го года - более заметный на оранжевой кривой, смерти на миллион населения). Главное - я не вижу отскока.
Annual US traffic fatalities per billion vehicle miles traveled (VMT) (red), per million people (orange), total annual deaths (light blue), VMT in 10s of billions (dark blue) and population in millions (teal), from 1921 to 2017
По теореме Гёделя и по фразе "Каждый раз, меняя кусочек основания, мы как будто порождаем новую математическую вселенную — со своими законами, истинами и парадоксами".
1. В 1936-м Герхард Генцен доказал непротиворечивость PA (Peano Arithmetic, арифметика первого порядка - о которой идёт речь в теореме Гёделя) в аксиоматической системе, которая не сильнее PA, но и не слабее. Все аксиомы системы в этом доказательстве, кроме специальной дополнительной, образуют аксиоматическую систему более слабую, чем PA - эту систему называют PRA (primitive recursive arithmetic) или арифметика Скулема. Эта часть аксиматики, использованной Генценом, строго слабее PA - в PA доказывается её непротиворечивость.
Однако, дополнительная аксиома - аксиома трансфинитной индукции - не доказуема в PA (иначе бы результат Генцена противоречил бы теореме Гёделя). Тем не менее имеются определённые основания "доверять" этой аксиоме (о чём чуть ниже).
Таким образом, две аксиоматические системы - PA и система, использованная Генценом для доказательства непротиворечивости PA, не сравнимы по силе - в каждой из них есть теоремы, недоказуемые в другой. "В основном" система в доказательстве Генцена проще, заковыка в дополнительной аксиоме, аксиоме трансфинитной индукции.
Вот пример арифметической теоремы, не доказуемой в PA (и факт недоказуемости - доказан в 1982-м), но доказуемой в системах с трансфинитной индукцией: теорема Гудстейна о сходимости к нолю определённых арифметических последовательностей (опубликована в 1944-м).
Следует ли из перечисленных мной фактов делать какие-либо далекоидущие выводы - решайте сами.
2. По фразе о "новой математической вселенной" - обратите внимание на направление "обратная математика" (reverse mathematics). Оказывается, многие фундаментальные теоремы доказуемы в ограниченных системах, так что - многие "новые математические вселенные" не так уж и отличны от классической.
Подробных ссылок не приводил, поскольку (с удивлением для себя) обнаружил, что многие интересные материалы по матлогике и основаниям математики отсутствуют или труднонаходимы на русском (сравнивая, например, с довольно подробными статьями в английской википедии).
Смотрю слайды (полученные через Кроссворд Тьюринга): ещё одно пересечение - Смирнов. Посмотрю видео его лекций. Кстати, модель Изинга, перколяции ("теория протекания") - неплохая тема для маткружка тоже, была книга. Библиотечка "Квант". Выпуск 19. 1982. Эфрос А.Л. Физика и геометрия беспорядка. https://math.ru/lib/bmkvant/19
О, оказалось - мы через одно рукопожатие! Тесен мир :).
Дети из местной русскоязычной диаспоры (айтишников, в основном, но не только). Друзья также преподают в дружественной англоязычной кружковской организации Prime Factor, руководительница которой Анна Бураго выпустила серию книг по ведению школьных маткружков, вот русские переводы: https://www.ozon.ru/person/burago-anna-gennadevna-70592622/category/knigi-16500/. Аня участвует в американских конференциях по кружковой тематике, в общем, богатая область - например, есть кружки по программе The Art of Problem Solving (https://artofproblemsolving.com/), есть и другие богатые материалом для продвинутых школьников книги / кружки... Есть чем увлечься на пенсии :). Да, упомяну также книгу по материалам ленинградских / петербуржских математических кружков https://archive.org/details/mathematical-circles-russian-experience - авторы недавно хорошо её обновили для нового англоязычного издания (кстати, она переводилась в разных странах). Один из авторов как раз, выйдя на пенсию, смог плотно заняться новой редакцией.
Интересно, спасибо! С моей программисткой точки зрения, несколько линков по общей тематике популяризации / обучения. Если вам не попадалось, у меня на примете (ну, например, выйду на пенсию - возможно, изучу подробно и попробую поучаствовать) сайт-коллекция open source интерактивных заметок / уроков / курсов: https://explorabl.es/ (сейчас там 180 таких элементов, построенных на разных технологиях - конфедерация энтузиастов). Такого типа уроки (на основе некой общей платформы) я встречал на https://khanacademy.org, а в последние годы на Ютубе в научно-популярных роликах рекламируют коммерческую платформу похожего вида (у них в шатате на зарплате по крайней мере один программист! :) - впрочем, у Хан Академи тоже есть программисты на ставке ) https://brilliant.org.
Нет, хотя организаторы и некоторые дополнительные преподаватели вроде меня - выпускники 239, 30, 45 (выпускавшиеся из этих школ в 80-е, и затем учившиеся на мат-мехе ЛГУ). Географически мы в Редмонде - под Сиэтлом.
Большое спассибо, очень инетересный обзор. Хотел бы поделиться опытом изложения темы на школьных математических кружках с некоторым креном на вывод уравнений для решения простых задач. Пересечение с обзором - по задаче про разорение, мы рассматриваем на кружке некоторые вариации и обсуждаем различные способы решать. Благодаря соавтору - профессиональному математику (я - программист) - оформили материал кружковских занятий как журнальную заметку и опубликовали в "Кванте":
https://www.mathnet.ru/php/archive.phtml?wshow=paper&jrnid=kvant&paperid=277
Эта заметка существует также на arXiv.org, так что у нас есть возможность вносить в неё исправления / добавления задним числом, так что дайте, пожалуйста, знать, если найдёте в ней неточности.
Последний штрих (заглянул в нашу заметку) - мы привлекли (как механизм для решения более широкого класса задач) упоминание про марковские цепи, собственно, вынеся "цепи" в заголовок заметки.
Да, наверно, использование std:: синхронизаций в комбинации с coroutines - рискованное занятие - я, может быть, поразбираюсь после выхода C++26 с senders / receivers. По подписочным делам - возможно, какой-то хорошо отлаженный код есть в крупных корпоративных OSS библиотеках вроде abseil, folly, но наверняка я не уверен (с обоими имел только шапочное знакомство).
В примере 1, по-моему, есть риск дедлока в Emit - в случае, если коллбэк деструктуриует одну из подписок (потому как используемый механизм блокировки - не reentrant; возможно, https://en.cppreference.com/w/cpp/thread/recursive_mutex поможет эту проблему преодолеть). Если вы используете этот код, попрубуйте прогнать тест, в котором коллбэк деструктуриует одну из подписок.
Я плотно ознакомился с двумя из перечисленных книг (слушал английские аудиокниги, по несколько раз каждую, на пробежках) и составил определённое мнение. Хочу ли я читать / слушать две другие книги? На данный момент - нет, но я могу переменить своё мнение.
Нассим старше меня на 9 лет; он, как и я, эмигрант первого поколения в США, переехавший из страны "восточнее Центральной Европы" (в моём случае это Россия, в его - Ливан). На его взгляды повлиял семейный опыт переезда (бегства?) из страны, охваченной гражданской войной (однако, его перевезли родители – сужу по датам из https://en.wikipedia.org/wiki/Nassim_Nicholas_Taleb, плюс, родители обеспечили ему учёбу в University of Paris, после чего он получал MBA уже в США). Я получил образование в ЛГУ, мои формативные young adult годы пришлись на 90-е в Петербурге, и я переезжал в США и перевозил свою семью сам, когда мне было 28. Пишу об этом в плане отметить – с какой колокольни я сужу о его творчестве? – ну, какой-никакой жизненный опыт у меня тоже есть, и мы оба «белые воротнички» по первой (и в моём случае – единственной) профессии; чувствую с ним сообщность стилей мышления. Он биржевой трейдер, я программист. У нас обоих по двое детей. Существенные различия тоже есть – Нассим – уроженец влиятельной семьи ливанских интеллектуалов / госчиновников высокого уровня. Он – богат, благодаря успешной работе трейдером на Wall Street и удачному управлению собственным капиталом; эти обстоятельства позволили ему сменить профессию (биржевой трейдер, конкретно в области опционных деривативов -> “essayist, mathematical statistician, risk analyst, and aphorist”). Я пока продолжаю работать «линейным сотрудником» в софтверной корпорации, математикой немного занимаюсь только на досуге, и не часто. Потребности учить кого-либо жизни "на собственном опыте" не испытываю.
В хорошо мною изученных книгах Талеба есть интересные идеи, интеллектуальные построения, чему я отдаю должное, не углубляясь в детали. Однако, мне претят элементы нравоучительного тона «человека, который добился всего сам и знает жизнь» (says who? – потомок состоятельной / влиятельной семьи, хорошо заработавший успешными операциями на бирже, а не работой в «производящей экономике»), хотя, вероятно, я здесь несколько пристрастен.
По «антихрупкости» и skin in the game (признаюсь, с этой последней книгой я не знаком) – хотел бы отметить «антихрупкость» (“antifragile”), по определениям Нассима, существующей системы, в которой высшие менеджеры имеют золотые парашюты и практически никакой "skin in the game" уровня ответственности… Система отлично переживает кризисы, из каждого из которых руководители выходят богаче и защищеннее, чем до кризиса, и сама система крепнет! Anitfragile! Любопытно, рассматривал ли он такой парадокс в своей последней книге.
По-моему, когда вы упомянули "Koko (.NET)", вы имели в виду Koka (https://koka-lang.github.io/) - ныне этот язык отвязан от .NET: компилятор порождает бинарный код для разных платформ через промежуточное представление на C.
Моё мнение: 1. За отсутствие шага транспиляции в определённых сценариях. 2. За более натуральную интеграцию типизированных компонентов в гетерогенных проектах.
По вашей ссылке, в самом начале статьи: "The aim of this proposal is to enable developers to run programs written in TypeScript, Flow, and other static typing supersets of JavaScript without any need for transpilation, if they stick within a certain reasonably large subset of the language."
Добавлю, что, по-моему, для JS пакетов появится более натуральный способ обеспечивать бесшовную интеграции с клиентским TS кодом - в сравнении с дополнительными d.ts файлами ("typings").
Ещё один момент - любопытно, что в предложении, процитированном выше, упоминаются и TS (с которым я знаком лучше по давнему проекту), и Flow (с которым я познакомился довольно шапочно) - интерграция двух различных типизирующих надстроек JS, пусть и частичная, может быть полезна в каких-то сценариях (в проектах, в которых используются и такие и сякие компоненты). Кроме того, есть и менее популярные чем TS и Flaw, но работающие проекты типизации JS (к примеру, с одним таким проектом я планирую познакомиться на досуге - enzo).
В плане pull vs push - есть ещё опция, message queue - в смысле, producer-ы пушают, consumer-ы пуллают (но: надо поддерживать брокеров). Я тесно знаком с такой моделью с Kafka в роли message queue. Любопытно, рассматривала ли ваша команда такую опцию.
Спасибо, интересно! Однако, предлагаю не обижать std::format_to в сравнении с sprintf: для sprintf буфер аллоцируется заранее, и с той же возможностью преаллоцировать буфер имеет смысл и std::format_to померять тоже. Я из любопытства померял - плюс добавил строчку на 10 миллионов итераций - получается примерно так (новая колонка с преаллоцированным буфером для std::format_to - предпоследняя):
iterations stringstream sprintf format_to fmt_to(2) format1 14.50 3.20 4.60 0.30 0.402 2.55 0.50 0.50 0.30 0.30
5 1.66 0.34 0.30 0.22 0.28
10 1.16 0.26 0.24 0.19 0.21
100 0.86 0.21 0.19 0.16 0.19
1000 0.82 0.20 0.17 0.15 0.18
10000 0.77 0.19 0.16 0.14 0.17
100000 0.74 0.17 0.14 0.13 0.15
1000000 0.77 0.18 0.17 0.14 0.18
10000000 0.74 0.17 0.14 0.13 0.16
Извините за поехавшее форматирование - не знаю, как это можно здесь исправить. Мерял с компилятором msvc, Release, все оптимизации - на скорость.
Код для новой колонки - как для sprintf:
std::string str(100, '\0');std::format_to(str.data(), "Number {} is great!", numbers[i]);
Интересно - однако, я не понял, как ":" поступает с типами операндов и своего результата. В примерах либо слева и справа тот же тип (целое, строка) или (более интересный второй случай) справа - вызов функции, возвращающей void, и затем ";". Второй случай намекает, что тип правого параметра диктует тип результа. Первый случай намекает, что тип левого параметра - тоже в деле. Хорошо, а если справа - целое, а слева - строка? Скорее всего, произойдет ошибка приведения типов ( хотя, можно и пофантозировать, что ошибки не будет, а типом результата будет тип-сумма целого и строки, int | string, как можно делать на TypeScript-е). А если справа и слева - пользовательские типы в каких-то отношениях subtype / supertype?
В плане accessibility - есть довольно интересная разрабока по диктовке математических формул - на случай, если вам будет любопытно: https://devblogs.microsoft.com/math-in-office/math-dictation/
Отлично, спасибо! Я себе сделал попроще, по мотивам той презентации, буду иметь в виду, если понадобится улучшить.
Антон, спасибо - вопрос: используется ли в этом проекте идиома / утилита fast pimpl (вы рассказывали о ней в презентации "C++ трюки из Такси" 2.5 лет назад)? Я заглянул в пару-тройку хедеров и не наткнулся на использование (пока). Предполагаю, что не используется - т.е. C++ утилита / приём весьма общего назначения, полезная в одном крупном C++ проекте, с которым вы работали, в другом крупном C++ проекте (в той же фирме) оказалась не так уж полезна?
Хотел бы прокоментировать
1. "Они могли бы добавить в язык атрибуты, упрощающие контроль и за выделением/освобождением памяти, и за использованием объектов на разных уровнях приоритета, чтобы не ловить это исключительно через Driver Verifier в процессе выполнения"
и
2. "Нет, вместо этого они предпочли писать и отлаживать весь системный код на C/C++ примитивными дедовскими методами, а теперь убедили себя, что нет ничего лучше, как переписать его на Rust".
По 1: приведу один пример того, что не только могли, но и делали. Вы, наверно, никогда не сталкивались с майкрософтовским SAL (Standard Annotation Language). Этот "язык аннотаций" для C, C++ был впервые внедрён, насколько я помню, в нулевые годы - и выпускался тогда в составе DDK (Dirver Development Kit) как хороший инструмент для повышения качества third party драйверов. https://learn.microsoft.com/en-us/cpp/code-quality/understanding-sal - хотя ныне, оставаясь полезным для кода в стиле C, этот инструмент кажется мне недостаточно современным для C++ кода. Современный msvc инструментарий включает майкрософтовский статический анализатор C++ кода, синхронизованный с рекомендацими C++ Core Guidelines (и, скорее всего, некоторыми стандартными атрибутами в двойных квадратных скобках - проверю этот аспект, когда мне это будет более кстати), и, в дополнение к этому, интеграцию с анализатором clang-tidy. Visual Studio предоставляет относительно удобный UI для использования этих возможностей. VS Code поддерживает эти возможности в какой-то мере тоже (читаю сейчас блог-пост про использование clang-tidy с VS Code).
По 2: это не так, в Microsoft активно используются статические анализаторы кода и другие методы формальной верификации (выше я коснулся только отдельных примеров, как такое использование возможно при применинии msvc toolchain), вот обзорная лекция по этому вопросу (я остановил на слайде, где перечисляются такие проекты / инструменты с 2001-го по 2022-й - для верификации в основном критического кода системного уровня): https://youtu.be/GEsvGGp0jyQ?t=935. Про переписывание на Rust - это ещё один инструмент; исходная заметка, которую мы комментируем, указывает только несколько таких проектов, пока имеющих относительно маленький размах, насколько я могу судить.
Ваша история про статистику смертности в автокатастрофах в США до и после внедрения подушек безопасности меня заинтересовала! Я поискал подтверждения, но пока не нашёл.
Нашёл вот такой график. Внедрение подушек безопасности происходило между примерно второй половиной 80-х (всё более широкое внедрение технологии, продолжавшей совершенствоваться; закон был принят в 1991-м, с отложенным вступлением в силу) и 1998-м годом (закон полностью вступил в силу). Красная кривая (смерти на милю) шла вниз, но не драматично (заметен небольшой зубец более резкого падения около 1992-го года - более заметный на оранжевой кривой, смерти на миллион населения). Главное - я не вижу отскока.
Аттрибуция графика: By Dennis Bratland - Own work, CC BY-SA 4.0, https://commons.wikimedia.org/w/index.php?curid=66179446