Рубрика «Euclid»

в 18:35, , рубрики: Euclid, астрономия, евклид, ЕКА, космонавтика, Научно-популярное

Телескоп «Евклид» вскоре начнёт изучать два миллиарда галактик. И это будет воистину технологическое чудо.

Как построить телескоп для охоты за тёмной энергией - 1

Вселенную заполняет загадочная сила, известная под названием тёмной энергии. Она заставляет нашу Вселенную расширяться с ускорением, в результате чего галактики разлетаются друг от друга всё быстрее и быстрее. Проблема в одном – мы не знаем точно, что это за сила. Как вообще может существовать такая важная сила, которую мы не понимаем?

Десятилетия астрономы задаются этим вопросом. И новый телескоп призван прояснить эту загадку. Телескоп Евклид Европейского космического агентства (ЕКА), который планируется запустить во второй половине 2022 года, не похож ни на какой другой аппарат. Он отправится в космос с тем, чтобы окончательно раскрыть некоторые из секретов тёмной энергии. Также он будет наблюдать и за тёмной материей – странным невидимым веществом, массой превосходящим всю обычную материю Вселенной. Невиданная доселе точность этих наблюдений перевернёт все наши представления о космосе.
Читать полностью »

в 13:00, , рубрики: context, Euclid, geometry, latex, metapost, tex

Fancy Euclid's “Elements” in TeX - 1

In 2016, I came across Oliver Byrne's “The first six books of the Elements of Euclid.” The main feature of this book is that instead of ordinary letter designations such as “triangle ABC,” it employs inclusions of miniature pictures directly in the text, that is, for example, an image of a triangle. As difficult as it probably was in the XIX century, as easy, with the right tools, it should be to make such a book nowadays. And so I decided to find out by myself whether that's the case.
Читать полностью »

в 20:09, , рубрики: ACL2, alloy, Altran, Cleanroom, CompCert, Euclid, IronFleet, Isabelle, Praxis, smt, TLA+, z3, контрактное программирование, контракты, логика Хоара, математика, Надя Поликарпова, Программирование, решатель, типизация, формальные методы, формальные языки, языки спецификаций

На Software Engineering Stack Exchange я увидел такой вопрос: «Что мешает широкому внедрению формальных методов?» Вопрос был закрыт как предвзятый, а большинство ответов представляли собой комментарии типа «Слишком дорого!!!» или «Сайт — это не самолёт!!!» В каком-то смысле это верно, но мало что объясняет. Я написал эту статью, чтобы дать более широкую историческую картину формальных методов (FM), почему они на самом деле не используются и что мы делаем для исправления ситуации.

Прежде чем начать, нужно сформулировать некоторые условия. На самом деле существует не так много формальных методов: всего несколько крошечных групп. Это означает, что разные группы по-разному применяют термины. В широком смысле есть две группы формальных методов: формальная спецификация изучает запись точных, однозначных спецификаций, а формальная проверка — методы доказательства. Сюда входят и код, и абстрактные системы. Мало того, что мы используем разные термины для кода и систем, мы часто используем разные инструменты для их верификации. Чтобы ещё больше всё запутать, если кто-то говорит, что создаёт формальную спецификацию, обычно это означает и верификацию дизайна. А если кто-то говорит, что делает формальную верификацию, обычно это относится к верификации кода.
Читать полностью »

в 10:00, , рубрики: Carta, ebook, Euclid, onyx boox, Блог компании МакЦентр, гаджеты, Читальный зал, электронная книга

Как древнегреческого геометра Евклида спросили:
— Что бы ты предпочёл — два целых яблока или четыре половинки?
— Конечно, четыре половинки.
— А почему? Это ведь одно и то же.
— Отнюдь. Выбирая два целых яблока, как я узнаю, червивые они или нет?

Когда теорема стала аксиомой: обзор ONYX BOOX Euclid - 1

Привет! Ну что ж, в полку электронных книг прибыло! Этот рынок может и небольшой, но он развивается и никакие новейшие планшеты не способны обратить этот процесс вспять :) Сегодня поговорим про новинку — книгу ONYX BOOX Euclid, которая была представлена в ноябре этого года. И даже если вы скептически относитесь к данной категории гаджетов, советуем заглянуть под кат — девайс заслуживает внимания не только любителей почитать перед сном.
Читать полностью »

Главная   |  Архив новостей  |   Android  |   Google  |   Apple  |   Microsoft  |   Информационная безопасность  |   Веб – разработка
Публикации RSS  |  Комментарии RSS
https://ajax.googleapis.com/ajax/libs/jquery/3.4.1/jquery.min.js