Вы с ветряной мельницей воюете, в таком случае. Ложность высказывания
реальную жизнь можно описать ТОЛЬКО формулами
строго и формально доказал Курт Гёдель в 1931 году, с тех пор всех, кто эту мысль так или иначе высказывает, молча посылают доказывать теорему его имени.
Нет никакой ошибки, ни глобальной, ни локальной. Доказательство — это вывод внутри формальной системы, точка, Так называемый "смысл" любому доказательству придает интерпретация его результатов. И если у вас получилось интерпретировать результаты так, что они согласуются с экспериментом — отлично, а если нет — нужно проверять только аксиомы и шаги, а не сами правила вывода. А в случае доказательств на естесственном языке — еще и автора к интерпретации подключать, ибо правила вывода знает только он. Вот в этом и разница, которую вы никак не хотите увидеть.
Не нахожу. Для того, чтобы аргументированно отрицать большой взрыв, мне не хватит знаний ни физики, ни космологии, ни математики. Более того, верность или ошибочность гипотезы о БВ я для себя не рассматриваю как принципиальный вопрос — мне это не важно. Если вам достаточно "немного подумать" — я вам завидую.
Дело вообще не в языке и не в формулах. Главное в формальных системах — не символы, а правила вывода. Ни в одном естественном языке их нет, и потому "дважды два — стеариновая свечка". Именно они делают формальное доказательство значительно более ценным, чем описанное на естественном языке, ибо для его проверки достаточно проверить только шаги доказательства, а не сами правила, по которому оно строится.
Так точно. Ваш "жизненный опыт" очень сильно ограничен длительностью и вариативностью вашей жизни. Радиоволны низких частот видите? Проявления ОТО непосредственно можете наблюдать? Там выше уже спрашивали про цвет рентгеновского излучения. Будете утверждать, что все эти вещи "не имеют смысла"?
Жизненный опыт — он у каждого свой, и кто-то может понять, как работает радио, а кому-то оно так и останется черной магией до конца его дней.
Понимаете, в самой формальной системе не бывает "верных" или "ошибочных" утверждений, только истинные и ложные. Разница в том, что "верность" теоремы — это её согласуемость с экспериментом, а истинность — выводимость из имеющейся системы аксиом. И иногда получается так, что якобы "ошибочная" аксиома (да хоть тот же пятый постулат Евклида возьмите) приводит к весьма интересным результатам — геометриям Лобачествого и Шварца. Если теоремы доказываются и доказываются, а система не приводит к противоречиям, то такая система уже интересна математикам, даже будучи "противоречащей" нынешним экспериментам или так называемому "здравому смыслу". Почитайте про "наивную теорию множеств", узнаете много нового про высказывания на естественном языке, которые кажутся истинными, пока их не пытаются формализовать нормально.
Примерно у 90% "вещей" в современной математике никаких других "своих" имен, кроме имен их авторов, нет, так что и называть их как-то иначе просто нечем. Ни в одном естесственном языке нет слова, обозначающего, например, поле Галуа. Язык, как уже писали выше — это прямое отражение окружающей и окружавшей его носителей реальности, а в ней эти поля не очень-то представлены, зато они очень круто представлены в информатике и криптографии, и сколько их там не называй "своими именами", без формулы не получится пояснить ни суть идеи, ни её применение.
А в высказывании об аберрациях у вас логика сломалась, извините. Формулы — это слова другого языка с другими свойствами, и из того, что "формулы — тоже слова", никак не следует "язык математики подвержен аберрациям не меньше естественных языков". Формальный язык специально сконструирован таким образом, чтобы быть подверженным этим самым аберрациям намного меньше, чем любой естественный. Именно для этого формальные системы придуманы, и именно для этого используются.
А из утверждения "формулы — тоже слова", если считать это утверждение истинным, по правилам формальной логики может следовать только "Не слова — это и не формулы", больше ничего.
Раз уж тут меня упомянули, отвечу автору на его вопрос о преимуществах формальных систем на неформальными.
Дело в том, что любые неформальные языки сильно страдают от потери информации при передаче мыслей, иногда настолько, что два разных человека могут прочесть в одном и том же тексте на неформальном языке две совершенно противоположных мысли, а автор при этом "имел в виду" третью, никак не связанную с первыми двумя. Вот эта "гибкость" — с ней оказалось столько проблем, что Пифагор даже отказывался от использования языка для доказательств вообще — "Смотри!".
Мы, вообще говоря, не думаем словами, мы обрекаем мысли в форму слов (при этом теряя заметную часть информации), а потом эти слова у другого человека снова превращаются в мысли, причем обязательно не в те, что были в голове автора изначально. Удалось донести какие-то крупицы оригинального смысла — прекрасно, нет — нужно формулировать мысль иначе. Формализация же позволяет "вынести личное за скобки", оставив только наиболее абстрактную (т.е. очищенную от не относящейся к сути конкретики) часть мысли. И если теорему Пифагора или "дважды два — четыре" вы еще сможете донести неформальным языком почти до любого человека (если только он ваш неформальный язык знает, попробуйте китайцу доказать ТП, используя только русский язык), то донести суть (а главное, строгое доказательство) чуть более сложных вещей (да хоть упомянутых ниже рядов) уже не получится от слова никак — в неформальном языке нет слов, чтобы выражать такие мысли.
Самое обидное, что я осознаю прекрасно, что вот этот текст — такие же мысли, выраженные на русском, и их точно так же каждый поймет, "сделав из себя"… Очень жду появления прямого интерфейса мозг-могз, без этих дурацких слов и тестов. Вот тогда пониманием каких-то вещей можно будет делиться непосредственно, а пока это светлое (или не очень, как посмотреть) будущее еще не наступило, формальные системы — наше всё.
Qt их поддерживает из коробки начиная с четвертой версии, поэтому я ими успещно пользовался и был не в курсе проблем с ними. А потом по лицензионным причинам пришлось отвязывать ПО от Qt, и проблемы неожиданно вскрылать так ярко, что теперь, видимо, придется писать свой велосипед по лекалам какого-нибудь FAR Manager'а, код которого открыт и длинные пути который поддерживает в полном объеме.
Никогда не доверяйте dmidecode, т.к. таблицы SMBIOS могут быть заменены кем угодно и на что угодно. Большинство реализаций BIOS/UEFI выводят в них всякий мусор, любой DXE драйвер/модуль ядра может их перехватывать и изменять в них данные. Если можете им не пользоваться — пожалуйста, не пользуйтесь, говорю вам как человек, который эти таблицы заполняет.
Не могу сказать точно, скорее всего там именно цифровые сенсоры. Прошу прощения за неточность формулировки, имел в виду temperature sensor без привязки к особенностям реализации.
Показания температурного сенсора вырабатывает микроконтроллер SMU, код прошивки которого закрыт и с этим AMD ничего сделать не может без его полного переписывания. Процессор содержит около 20 внутренних терморезисторов, показания которых нужно каким-то образом свести к одному-двум числам, для чего используется довольно хитрый алгоритм с множеством параметров, большую часть которых можно настроить из регистра D18F3xA4 Reported Temperature Control. Вопрос достаточно подробно освещен в BKDG, там же рассказано, относительно какой точки измеряется температура и как повлиять на эту точку.
В области решений для сетевой техники я, каюсь, разбираюсь довольно слабо, поэтому поверю вам на слово. Нет открытых решений — значит нет, но никто нам не запрещает хотеть их появления.
Если же вернуться в область SoC общего назначения, в которой я работаю сейчас, там есть такое семейство процессоров AMD eKabini (FT3), на которые есть не только открытый BKDG, но и открытая схема. При этом процессор не является ни устаревшим (будет производится до 2020 года), ни малопроизводительным (новые APU лучше процентов на 20), ни непопулярным (куча плат для Embedded и Industrial, по одной-две платы от всех главных десктопных вендоров). Ни 10 лет назад, ни 5 я такого не видел, но, возможно, просто не смотрел.
Тем не менее, документацию понемногу приоткрывают, и это прекрасно. Сделано это для стимуляции продаж или нет, сразу или позже — главное, что сделано. Я с большой надеждой смотрю на проекты LowRISC и OpenRISC, ибо открытое железо — первый шаг к возвращению хоть какого-то доверия к этому самому железу.
Планируется ли открытие BKDG, без которого портировать свои системы на новую SoC практически невозможно? Какой предлагается загрузчик по умолчанию, есть ли в нем поддержка ACPI, devtree или аналогичных систем, реализующих абстракцию от оборудования? Есть ли готовый "золотой" дистрибутив Linux, и если есть, на базе какого дистрибутива он сделан и насколько его ядро отличается от ванильного?
Фиг там, извините. Тот факт, что create_directories любезно вызовет CreateDirectoryW, если ей дать полный путь с префиксом \\?\ — это замечательно, конечно, только вот это не поддержка ни разу. Ни канонизацию, ни траверс, ничего с длинным путем нормально сделать нельзя, а соотвествующие тесты даже закомментированы (filesystem\test\path_test.cpp). Т.е. весь траверс и канонизацию предлагается написать самому, и непонятно, зачем тогда вообще такая библиотека.
Ни boost::FS, ни "новая" std::FS до сих пор не поддерживают пути длинее PATH_MAX (260 байт) в Windows, которые самой системой поддерживаются уже почти 10 лет. При этом все красиво и здорово, итераторы и emplace, только вот по факту "новая" функциональность ничуть не лучше какой-нибудь замшелой _mkdir из direct.h, прости рандом.
У меня такое сравнение запланированно в ближайший месяц — два, но статью я про него точно писать не буду, т.к. проверяемый код (реализации UEFI) закрыт, а проверять второй раз Quark BSP смысла почти нет.
Отдельно скажу про Clang — когда наши ~400 Мб кода прошивки начнут им собираться, тогда можно будет к нему вернуться, а пока им нормально не собирается даже постоянно обновляемый EDK2, не говоря уже о вендорском коде времен царя Гороха.
Жизненный опыт — он у каждого свой, и кто-то может понять, как работает радио, а кому-то оно так и останется черной магией до конца его дней.
А в высказывании об аберрациях у вас логика сломалась, извините. Формулы — это слова другого языка с другими свойствами, и из того, что "формулы — тоже слова", никак не следует "язык математики подвержен аберрациям не меньше естественных языков". Формальный язык специально сконструирован таким образом, чтобы быть подверженным этим самым аберрациям намного меньше, чем любой естественный. Именно для этого формальные системы придуманы, и именно для этого используются.
А из утверждения "формулы — тоже слова", если считать это утверждение истинным, по правилам формальной логики может следовать только "Не слова — это и не формулы", больше ничего.
Дело в том, что любые неформальные языки сильно страдают от потери информации при передаче мыслей, иногда настолько, что два разных человека могут прочесть в одном и том же тексте на неформальном языке две совершенно противоположных мысли, а автор при этом "имел в виду" третью, никак не связанную с первыми двумя. Вот эта "гибкость" — с ней оказалось столько проблем, что Пифагор даже отказывался от использования языка для доказательств вообще — "Смотри!".
Мы, вообще говоря, не думаем словами, мы обрекаем мысли в форму слов (при этом теряя заметную часть информации), а потом эти слова у другого человека снова превращаются в мысли, причем обязательно не в те, что были в голове автора изначально. Удалось донести какие-то крупицы оригинального смысла — прекрасно, нет — нужно формулировать мысль иначе. Формализация же позволяет "вынести личное за скобки", оставив только наиболее абстрактную (т.е. очищенную от не относящейся к сути конкретики) часть мысли. И если теорему Пифагора или "дважды два — четыре" вы еще сможете донести неформальным языком почти до любого человека (если только он ваш неформальный язык знает, попробуйте китайцу доказать ТП, используя только русский язык), то донести суть (а главное, строгое доказательство) чуть более сложных вещей (да хоть упомянутых ниже рядов) уже не получится от слова никак — в неформальном языке нет слов, чтобы выражать такие мысли.
Самое обидное, что я осознаю прекрасно, что вот этот текст — такие же мысли, выраженные на русском, и их точно так же каждый поймет, "сделав из себя"… Очень жду появления прямого интерфейса мозг-могз, без этих дурацких слов и тестов. Вот тогда пониманием каких-то вещей можно будет делиться непосредственно, а пока это светлое (или не очень, как посмотреть) будущее еще не наступило, формальные системы — наше всё.
Если же вернуться в область SoC общего назначения, в которой я работаю сейчас, там есть такое семейство процессоров AMD eKabini (FT3), на которые есть не только открытый BKDG, но и открытая схема. При этом процессор не является ни устаревшим (будет производится до 2020 года), ни малопроизводительным (новые APU лучше процентов на 20), ни непопулярным (куча плат для Embedded и Industrial, по одной-две платы от всех главных десктопных вендоров). Ни 10 лет назад, ни 5 я такого не видел, но, возможно, просто не смотрел.
Отдельно скажу про Clang — когда наши ~400 Мб кода прошивки начнут им собираться, тогда можно будет к нему вернуться, а пока им нормально не собирается даже постоянно обновляемый EDK2, не говоря уже о вендорском коде времен царя Гороха.