Добавлю со своей UEFI-колокольни об упомянутых современных машинах для плодотворной работы с кодом: с точки зрения прошивки лучшие машины сейчас делают Dell и HP, на второе место я бы поставил Lenovo, которые тоже относительно неплохи, но не без греха, да еще и с SuperFish и WPBT оскандалится умудрились. У Apple сейчас пока еще все очень грустно, но уже в следующем поколении MBP они обещают решить проблемы с защитой от вредоносных OptionROMов, с защитой от подмены загрузчика, с защитой от DMA-атак и с отсутствием HW root-of-trust или хотя бы чипа TPM 2.0 для measured boot.
В общем, если покупать прямо завтра, я бы купил систему у Dell. Они уже и ESRT внедрить успели, и обновления прошивки через репозитории fwupdate распрострают, и BootGuard на них включен и протестирован.
Я вам про ветряную мельницу уже ниже ответил. Никто утверждение "для описания реальности нужны НЕ ТОЛЬКО формулы" не оспаривает, вот с высказыванием вроде "формулы — ну нужны" спорили, спорят, и спорить будут. И эти два высказывания — совсем не одно и то же.
Вы с ветряной мельницей воюете, в таком случае. Ложность высказывания
реальную жизнь можно описать ТОЛЬКО формулами
строго и формально доказал Курт Гёдель в 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, и если есть, на базе какого дистрибутива он сделан и насколько его ядро отличается от ванильного?
В общем, если покупать прямо завтра, я бы купил систему у Dell. Они уже и ESRT внедрить успели, и обновления прошивки через репозитории fwupdate распрострают, и BootGuard на них включен и протестирован.
не брал в руки шашекне писал длинных русских текстов, если найдете очепятку — пишите в Л/С, постараюсь исправить.Жизненный опыт — он у каждого свой, и кто-то может понять, как работает радио, а кому-то оно так и останется черной магией до конца его дней.
А в высказывании об аберрациях у вас логика сломалась, извините. Формулы — это слова другого языка с другими свойствами, и из того, что "формулы — тоже слова", никак не следует "язык математики подвержен аберрациям не меньше естественных языков". Формальный язык специально сконструирован таким образом, чтобы быть подверженным этим самым аберрациям намного меньше, чем любой естественный. Именно для этого формальные системы придуманы, и именно для этого используются.
А из утверждения "формулы — тоже слова", если считать это утверждение истинным, по правилам формальной логики может следовать только "Не слова — это и не формулы", больше ничего.
Дело в том, что любые неформальные языки сильно страдают от потери информации при передаче мыслей, иногда настолько, что два разных человека могут прочесть в одном и том же тексте на неформальном языке две совершенно противоположных мысли, а автор при этом "имел в виду" третью, никак не связанную с первыми двумя. Вот эта "гибкость" — с ней оказалось столько проблем, что Пифагор даже отказывался от использования языка для доказательств вообще — "Смотри!".
Мы, вообще говоря, не думаем словами, мы обрекаем мысли в форму слов (при этом теряя заметную часть информации), а потом эти слова у другого человека снова превращаются в мысли, причем обязательно не в те, что были в голове автора изначально. Удалось донести какие-то крупицы оригинального смысла — прекрасно, нет — нужно формулировать мысль иначе. Формализация же позволяет "вынести личное за скобки", оставив только наиболее абстрактную (т.е. очищенную от не относящейся к сути конкретики) часть мысли. И если теорему Пифагора или "дважды два — четыре" вы еще сможете донести неформальным языком почти до любого человека (если только он ваш неформальный язык знает, попробуйте китайцу доказать ТП, используя только русский язык), то донести суть (а главное, строгое доказательство) чуть более сложных вещей (да хоть упомянутых ниже рядов) уже не получится от слова никак — в неформальном языке нет слов, чтобы выражать такие мысли.
Самое обидное, что я осознаю прекрасно, что вот этот текст — такие же мысли, выраженные на русском, и их точно так же каждый поймет, "сделав из себя"… Очень жду появления прямого интерфейса мозг-могз, без этих дурацких слов и тестов. Вот тогда пониманием каких-то вещей можно будет делиться непосредственно, а пока это светлое (или не очень, как посмотреть) будущее еще не наступило, формальные системы — наше всё.
Если же вернуться в область SoC общего назначения, в которой я работаю сейчас, там есть такое семейство процессоров AMD eKabini (FT3), на которые есть не только открытый BKDG, но и открытая схема. При этом процессор не является ни устаревшим (будет производится до 2020 года), ни малопроизводительным (новые APU лучше процентов на 20), ни непопулярным (куча плат для Embedded и Industrial, по одной-две платы от всех главных десктопных вендоров). Ни 10 лет назад, ни 5 я такого не видел, но, возможно, просто не смотрел.