портируешь на coq

профит

ну пишешь обычное доказательство

Это как? Как я напишу машине, что пи - это трансцендентное число?

Это как? Как я напишу машине, что пи - это трансцендентное число?

ну соре, объяснять как работают пруферы это оффтоп

ну соре, объяснять как работают пруферы это оффтоп

да норм, про isabelle/coq/z3 можно

даже про tla+ можно

ну тогда у меня не остается выхода кроме как признать что я не знаю)

ихихих

но вообще тема интересная, гораздо интереснее кодировок вывода в виндовой консоли

но вообще тема интересная, гораздо интереснее кодировок вывода в виндовой консоли

+

Парсить argv?

Вопрос: как доказать через ЯП, что в числе пи есть любая комбинация цифр, например, мой номер телефона?

Ну вот, например, тут на Coq доказывают большую теорему Ферма для n=4: https://github.com/coq-contribs/fermat4/blob/master/Fermat4.v А вообще гуглить в сторону матлогики и аксиом теории чисел (скажем, аксиомы Пеано для натуральных). Дальше надо будет как-то аксиоматически определить вещественные числа, само число пи (скажем, через ряды) и так далее.

Вопрос: как доказать через ЯП, что в числе пи есть любая комбинация цифр, например, мой номер телефона?

Если что, то свойство, которое вы назвали, называется "нормальностью по основанию 10" (https://ru.wikipedia.org/wiki/%D0%9D%D0%BE%D1%80%D0%BC%D0%B0%D0%BB%D1%8C%D0%BD%D0%BE%D0%B5_%D1%87%D0%B8%D1%81%D0%BB%D0%BE). Оно не следует из иррациональности или трансцедентности. Человечество пока не знает, нормально ли пи по основанию 10.

Если что, то свойство, которое вы назвали, называется "нормальностью по основанию 10" (https://ru.wikipedia.org/wiki/%D0%9D%D0%BE%D1%80%D0%BC%D0%B0%D0%BB%D1%8C%D0%BD%D0%BE%D0%B5_%D1%87%D0%B8%D1%81%D0%BB%D0%BE). Оно не следует из иррациональности или трансцедентности. Человечество пока не знает, нормально ли пи по основанию 10.

Хочешь сказать, что если взять пи и разбавить нулями через одну цифру, то трансцендентности не убавится, а вот большинство телефонных номеров там точно не появятся? И, видимо, для любой строки из цифр мы не можем доказать, что её нет в пи, зато если она есть где-то недалеко, то можем найти и предьявить.

но вообще тема интересная, гораздо интереснее кодировок вывода в виндовой консоли

+, но надо ботать теории типов и все такое чтобы норм вписаться в это

реквестирую ссылку на пи-fs

реквестирую ссылку на пи-fs

я тоже о ней подумал

+, но надо ботать теории типов и все такое чтобы норм вписаться в это

Необязательно ботать теорию типов (а вот функциональное программирование может помочь), есть офигительная книжка: https://softwarefoundations.cis.upenn.edu/

Необязательно ботать теорию типов (а вот функциональное программирование может помочь), есть офигительная книжка: https://softwarefoundations.cis.upenn.edu/

#book

@antoshkka , @NataMakarova еще четырех людей надо призвать в РГ21, чтоб в чате было 2100 участников )

а буст кукбук не будут сливать?...

а буст кукбук не будут сливать?...

так ты попроси у @antoshkka . мб у него есть ссылка на торрент

а буст кукбук не будут сливать?...

был же где-то

был же где-то

не нашель

Необязательно ботать теорию типов (а вот функциональное программирование может помочь), есть офигительная книжка: https://softwarefoundations.cis.upenn.edu/

ну меня скорее всего интересует формальная верификации чем матемвтические пруфы, поэтому я не совсем представляю как там все

ну меня скорее всего интересует формальная верификации чем матемвтические пруфы, поэтому я не совсем представляю как там все

Норм, там книжка как раз про формальную верификацию программ, а не теоремы. Вот, например, формально доказанный компилятор C: http://compcert.inria.fr/ https://github.com/AbsInt/CompCert

Норм, там книжка как раз про формальную верификацию программ, а не теоремы. Вот, например, формально доказанный компилятор C: http://compcert.inria.fr/ https://github.com/AbsInt/CompCert

ну как раз в формальной верификации я понимаю немного больше чем ничего

в отличии от

Вопрос по организации работы с множеством репозиториев(7 штук на данный момент). Проект состоит из модулей друг от друга фактически зависимых - клиент, бэкэнд, конфигурации, статика и т.д. каждый живет в своем репозитории. Сейчас все работают только в двух ветках - develop и release. Все это собирается через CI и деплоится по кнопке аля teamcity. Минусы подхода очевидны - только 2 ветки не дают возможности раздельно тестировать\разрабатывать фичи. В виду коммерческого характера проекта - не все члены команды должны иметь доступ ко всем репозиториям- например в статику имеют доступы художники поддержки(льют картинки), но к репозиторию с серверным кодом они доступ не имеют. Хотим перейти на git-flow-подобную схему работы, но заводить по ветке в каждом репозитории накладно, когда не каждый реп нужно менять. Ситуацию осложняет то, что есть несколько однотипных проектов и например бэкэнд посути у них общий.

Вопрос по организации работы с множеством репозиториев(7 штук на данный момент). Проект состоит из модулей друг от друга фактически зависимых - клиент, бэкэнд, конфигурации, статика и т.д. каждый живет в своем репозитории. Сейчас все работают только в двух ветках - develop и release. Все это собирается через CI и деплоится по кнопке аля teamcity. Минусы подхода очевидны - только 2 ветки не дают возможности раздельно тестировать\разрабатывать фичи. В виду коммерческого характера проекта - не все члены команды должны иметь доступ ко всем репозиториям- например в статику имеют доступы художники поддержки(льют картинки), но к репозиторию с серверным кодом они доступ не имеют. Хотим перейти на git-flow-подобную схему работы, но заводить по ветке в каждом репозитории накладно, когда не каждый реп нужно менять. Ситуацию осложняет то, что есть несколько однотипных проектов и например бэкэнд посути у них общий.

и что вы предлагаете

1) все в один большой репозиторий, но уйти с git и попытаться разделять доступы(правда не очень понятны некоторые моменты мерджа) в типа SVN... 2) мучаться и заводить ветки, но попытаться это автоматизитровать?

Наверняка мы не первые, может кто-то придумал как красиво решить данный момент)

но с icache у c++ и так все плохо за счет over inlining в огромном множестве проектов

Ну а префетч для кого придумали?

1) все в один большой репозиторий, но уйти с git и попытаться разделять доступы(правда не очень понятны некоторые моменты мерджа) в типа SVN... 2) мучаться и заводить ветки, но попытаться это автоматизитровать?

у каждой команды свой репозиторий. А что шарится - то пусть лежит в общем

у каждой команды свой репозиторий. А что шарится - то пусть лежит в общем

Очень часто для фичи требуется редактировать конфигурацию(в ней настройки некой фичи) и например клиент, но редактирование конфигурации требует пересборки еще и сервера, хотя по факту изменений в нем не будет мы все-равно должны завести ветку, но как минимум мы должны прогнать тесты с новой конфигурацией

@urandon, как поможет префетч при джампах, больших размера страницы?

держите конфиг из repo:branch в отдельном репо, стягивайте через google repo и собирайте

а при аггрессивном инлайнинге это вполне себе кейс

держите конфиг из repo:branch в отдельном репо, стягивайте через google repo и собирайте

можно так

ну и tlb не резиновый

1) все в один большой репозиторий, но уйти с git и попытаться разделять доступы(правда не очень понятны некоторые моменты мерджа) в типа SVN... 2) мучаться и заводить ветки, но попытаться это автоматизитровать?

Perforce посмотри

но поскольку надо использовать gcc8 а не 5, то это проблема надуманная

Хотели сказать 4? :)

Вопрос: как доказать через ЯП, что в числе пи есть любая комбинация цифр, например, мой номер телефона?

Это невозможно

Точнее так: человечество не умеет решать эту задачу

Еще точнее так: википедия уверена, что эта задача до сих пор не решена

Можно начинать гуглить с вот этого https://ru.wikipedia.org/wiki/%D0%9D%D0%BE%D1%80%D0%BC%D0%B0%D0%BB%D1%8C%D0%BD%D0%BE%D0%B5_%D1%87%D0%B8%D1%81%D0%BB%D0%BE

Хотели сказать 4? :)

ни тот ни другой не надо использовать

Как можно сесурно и портабельно обнулить данные по указателю? Есть memset_s, но мб в крестах тож есть что-то подобное

std::memset ?

std::memset ?

может соптимизироваться же

В C11, говорят, мог появиться memset_s

Как можно сесурно и портабельно обнулить данные по указателю? Есть memset_s, но мб в крестах тож есть что-то подобное

https://gist.github.com/foxcpp/0938ecddf71d6258dd985a882e89caef#file-secure_memory-cpp-L49 Что-то типо того?

В C11, говорят, мог появиться memset_s

да, яж сказал про memset_s, вопрос про плюсы

https://gist.github.com/foxcpp/0938ecddf71d6258dd985a882e89caef#file-secure_memory-cpp-L49 Что-то типо того?

сложноватенько, однако

Как можно сесурно и портабельно обнулить данные по указателю? Есть memset_s, но мб в крестах тож есть что-то подобное

https://wiki.sei.cmu.edu/confluence/display/c/MSC06-C.+Beware+of+compiler+optimizations https://stackoverflow.com/questions/13299420/mac-os-x-equivalent-of-securezeromemory-rtlsecurezeromemory/13299459#13299459

https://wiki.sei.cmu.edu/confluence/display/c/MSC06-C.+Beware+of+compiler+optimizations https://stackoverflow.com/questions/13299420/mac-os-x-equivalent-of-securezeromemory-rtlsecurezeromemory/13299459#13299459

а, все таки volatile + явного цикла достаточно

недостаточно, но с современными компиляторами работает

А почему недостаточно?

а, все таки volatile + явного цикла достаточно

volatile испортит все оптимизации, касающиеся этого указателя

по стандарту, volatile pointer не значит убирать оптимизации над памятью, на которую этот pointer указывает

side effect относится к поинтеру, а не к памяти

тоже верно

http://www.daemonology.net/blog/2014-09-04-how-to-zero-a-buffer.html

The C standard states that accesses to volatile objects are part of the unalterable observable behaviour — but it says nothing about accesses via lvalue expressions with volatile types.

возможно, в c++ этот странный момент описан иначе

Можно посмотреть, как OpenSSL справляются)

А, там тоже Си, соря.

side effect относится к поинтеру, а не к памяти

В смысле «если я записываю по volatile указателю и больше ничего с ним не делаю, то компилятор имеет право это убрать»?

В смысле «если я записываю по volatile указателю и больше ничего с ним не делаю, то компилятор имеет право это убрать»?

Имеет, но на практике никто так не делает, ибо все понимают, зачем люди обычно записывают через volatile-указатель.

по стандарту, volatile pointer не значит убирать оптимизации над памятью, на которую этот pointer указывает

а поинтер на volatile?

Указателю на волатильные данные же!

А, да

А ещё лучше волатильные данные по волатильному указателю

А ещё лучше почитать как твой компилятор это решает

А ещё лучше волатильные данные по волатильному указателю

зачем

зачем

Как-то играл с segfault-ами, чтобы его получить разименовывание указателя на волатильные данные не работало, а вот волатильного указателя работало)

потомучто это уб

скорее всего он предподсчитал заранее какието смещения

Как можно сесурно и портабельно обнулить данные по указателю? Есть memset_s, но мб в крестах тож есть что-то подобное

std::fill?

секурно

Ну, если используется указатель, то о какой секьюрности может вообще идти речь)

да, яж сказал про memset_s, вопрос про плюсы

тоже memset_s