Вообще, лучшие научно-популярный книги — те, где сам учёный (не журналист) рассказывает о том, как делается наука. Из тех, что я читал — «Следы трав индейских» Мейена (палеоботаника) и «Рыбы открытого океана» Парина (ихтиология). Но это книги, мягко говоря, не весёлые, для развлечения не годятся. Если же хочется узнать, как что устроено, то лучше почитать хороший учебник (а как его найти — надо скачать несколько учебников и попробовать).
Трудно сказать, но вообще всего четыре страны достоверно сделали обогащение урана сами (США, СССР, Бразилия и Северная Корея). Англия, Франция, Израиль, Китай, Индия и Пакистан получили в подарок. Ирану, по слухам, сильно помогали северные корейцы.
Нужен простой пример. Если мы бросаем монету, частота выпадения герба стремится к одной второй для большинства испытаний. Выписать последовательности из двух бросков 00, 01,10, 11, затем из трёх и четырёх, посчитать частоту герба, всё станет ясно. Притом, монета может случайно падать одним гербом сколько угодно раз подряд (но вероятность этого мала).
Долго читать не смог, но первые замечания про равенство (a=a очевидно и в этом суть) очень похожи на современные проблемы с равенством в теории типов homotopytypetheory.org/book
Фреге, видимо, далеко глядел. Интересно, что Пирс придумал кванторы на 15 лет раньше Фреге и вставил в толстую книгу «Семиотика», там они и пропали, потому что никто не мог её читать (был русский перевод части этой книги в толстом сборнике советских времён тоже с названием «Семиотика», поищите, если интересно). Фреге был всё-таки математик и иногда излагал понятнее.
Есть задача «написать программу, печатающую свой собственный текст», решается подстановкой чего-то куда-то. Вот именно это и проделал Гёдель. Если можно говорить о строках и подстановке, можно выписать формулу, утверждающую что-то наперёд заданное о себе самой.
Возьмём теорию, в которой можно говорить о натуральных числах. Например, ZF (стандартную теорию множеств Цермело-Френкеля). Занумеруем формулы этой теории натуральными числами. Дальше, ловко применив диагональный метод, можно выписать формулу, утверждающую что-то о своём собственном номере. Например, пишем формулу «число 150 простое» и номер этой формулы оказывается как раз 150 (150 тут условно, какое именно число получится, зависит от построения). То есть, это формула как бы говорит «мой номер — простое число». Можно вместо натуральных чисел говорить о строках (во времена Гёделя это было не принято, потому что программирования не было). Тогда и нумеровать не надо, потому что формулы и так уже строки. Тогда можно построить формулу, утверждающую что-то о себе самой (например «в результате подстановки такой-то строки в такую-то вместо такой-то буквы получается строка такой-то длины» и если проделать эту подстановку, то получается как раз сама эта формула. То есть, она утверждает «моя длина такая-то»). Дальше, легко определить множество формул, доказуемых (или «выводимых») в ZF. Это все формулы, которые можно получить из аксиом, применяя некоторые простые правила («правила вывода» вроде Modus ponens). Итого, мы пишем формулу ZF с одним параметром-строкой, утверждающую «строка выводима». Дальше строим формулу, утверждающую «я невыводима в ZF». Если эта формула выводима, то по смыслу получаем противоречие (она утверждает, что её вывести нельзя, а мы вывели). Немного потрудившись, в этом случае можно получить и формальное противоречие в ZF. Если она невыводима, то истинна по смыслу (она как раз утверждает, что её вывести нельзя). Таким образом, или ZF противоречива, или в ней есть невыводимая, но содержательно истинная формула. Всё это применимо и к гораздо более слабым теориям (чем ZF), лишь бы можно было говорить про строки и подстановку строк друг в друга.
Разработаны языки, позволяющие строго записывать математические доказательства (с той же строгостью, с какой мы записываем алгоритмы в языках программирования). Длина такого доказательства обычно раз в двадцать больше длины обычного (какое мы излагаем в статье). Зато правильность его легко проверить автоматически (проверяет простая программка «пруфчекер»). Дело в том, что ни у кого нет времени и желания формализовать доказательство Мотидзуки.
Надо гуглить. Ну, вот непонятный текст из вики-статьи про Воеводского
«В работах 1989—1990 годов по высшим группоидам, написанных в соавторстве с Капрановым, развил идею Гротендика о возможности описания CW-комплексов с гомотопической точки зрения как группоидов. В 1998 году Карлосом Симпсоном построен контрпример к одной из основных конструкций этих работ, который Воеводский с Капрановым изначально не признали, и статья Симпсона не была принята в журналы; лишь в 2013 году Воеводский подтвердил доводы Симпсона.»
Расшифровываю: в 90-м году Воеводский и Капранов «доказали» некую хорошую теорему. В 98-м Симпсон нашёл пример, вроде бы опровергающий эту теорему. Воеводский считал, что Симпсон ошибся и приводил какие-то доводы. И доказательство, и пример Симпсона настолько сложны, что никто не мог проверить до 2013-го года, когда Воеводский сам нашёл ошибку в своей статье (через 23 года). После этого он все свои доказательства проверял пруфчекером.
Проблема в том, что у людей нет столько времени. Тут точно так же, как с доказательным программированием. Была австралийская фирма NICTA (полугосударственная), они писали маленькую безотказную операционку для медицинской техники. Писали на C, вставляли в программу условия, которые должны быть выполнены в момент, когда до них дойдёт дело (логика Хоара). Например, (x>0) x=x+1; (x>1) Если перед выполнением присваивания x=x+1 было верно предусловие (x>0), то после будет верно (x>1). Затем писали доказательство, что условия действительно выполнены и проверяли его пруфчекером Isabelle. На 7500 строк кода пришлось выписать примерно 200 тысяч строк доказательств, это заняло 11 человеко-лет работы. Пруфчекер нашёл 144 ошибки. Дело хорошее, но ясно, что так мы много не напрограммируем. В математике сейчас доказательства настолько сложные (всё простое давно доказано), что проверять их нет желающих, авторитетам верят на слово. Тот же Воеводский в своей статье нашёл ошибку через 20 лет.
Юсуф недоволен arxiv-ом. Странным образом, я согласен в этом с Юсуфом. С некоторых пор на arxiv ввели анонимную цензуру (твою статью отклоняет неизвестно кто неизвестно почему), притом в списке модераторов нет ни одного известного мне математика (кроме лично шапочно знакомого Шурика Кириллова). Но уже скоро вместо еврейской модерации будет негритянская, вместо Шурика Кирилова будет Бубба Мапиндози, вот тогда и заживём.
С одной стороны, Ломоносов ввёл в русский язык 200 новых слов («газ», «атмосфера» и т.д.). С другой, если всякий будет так делать… Вообще, если слово «маркер» воспринимается как более русское — значит, дело плохо.
Обнаружил, что можно прекрасно работать с сетью на Lua через nmap. Например, задача — скачать фотку по ftp. Пишем программу на Lua, но с расширением .nse (скрипт nmap), основная часть выглядит так (вместо pathtoimage надо подставить адрес фотки)
local ftp = require "ftp"
local socket, code, message, buffer = ftp.connect(host, port, {request_timeout=8000})
local status, code, message = ftp.auth(socket, buffer, "anonymous", "pass")
local jpg_socket, err = ftp.pasv(socket, buffer)
local status, err = socket:send("RETR pathtoimage.jpg\r\n")
local jpg = {}
while true do
local status, data = jpg_socket:receive()
if (not status) or data == "" then
break
end
jpg[#jpg + 1] = data
end
jpg = table.concat(jpg)
Рисовать можно не только растения, но и фракталы, и клеточное деление эмбрионов (там есть специальная программа для рисования эмбрионов). Математика простая на грани шарлатанства (типа клеточных автоматов), но картинки красивые.
А я всегда говорил, что программистский жаргон — это искажённый тюремный. Вышел пацан из маргинализированной зоны, нигде не получалось находить работу.
Qt тем и хорош, что заметно облегчает работу с невменяемым C++. Если бы его (Qt) приделали к более разумному языку! Но даже версия для Явы не обновляется уже несколько лет.
А почему, интересно? Я просто по себе вижу, что занимался долго теорией типов (как математик), а программировать предпочитаю на Lua, если есть возможность. Haskell при том совсем не возбуждает. Программисты, кажется, в обратную сторону ползут.
Мазафака. Этот негр воображает себя Львом Толстым. Дальше фраза из Льва Толстого для сравнения
Стоя в холодке вновь покрытой риги с необсыпавшимся еще пахучим листом лещинового решетника, прижатого к облупленным свежим осиновым слегам соломенной крыши, Левин глядел то сквозь открытые ворота, в которых толклась и играла сухая и горькая пыль молотьбы, на освещенную горячим солнцем траву гумна и свежую солому, только что вынесенную из сарая, то на пестроголовых белогрудых ласточек, с присвистом влетавших под крышу и, трепля крыльями, останавливавшихся в просветах ворот, то на народ, копошившийся в темной и пыльной риге, и думал странные мысли.
Если хотите непременно программировать, есть Categorical abstract machine, это такой «ассемблер» для функционального программирования. Машина вычисляет «категорные комбинаторы». Сейчас ещё что-то новое есть в этом роде. Возможно, когда-нибудь взлетит и будут в железе такие машины. Но мне кажется, основная польза от теории категорий для программистов — она максимально приближает программирование к математике. Эти самые монады придуманы в абстрактной математике для вычисления каких-то «гомотопий», а потом оказалось, что это весьма общая идея «вычисления функций с дополнительным прибамбахом» (например, вычисления с побочными эффектами описываются монадой).