Рубрика «Rust» - 2

Это обзорная статья, в которой очень поверхностно и не подробно рассказывается о том, что такое формальная верификация программного кода, зачем она нужна и чем она отличается от аудита и тестирования.

Формальная верификация — это доказательство с использованием математических методов корректности программного обеспечения.

Формальная верификация молода. На сегодняшний день, на сайте хабр, например, нет (пока) специализации «Формальная верификация», нет специальности «Proof инженер» или «Специалист по формальной верификации». А люди, работающие по этой специальности — есть.

Читать полностью »

Всем здравствуйте, меня зовут Антон, и этой статьей я открываю новый цикл публикаций про Unicode. Сразу может возникнуть вопрос — зачем? Их же и так море?

На Хабре, как и вообще в русскоязычном сегменте Интернета, в основном можно найти обзорные статьи, дающие лишь общее представление о Юникоде, но о том, как с ним работать — информации крайне мало. Сами же его разработчики, Unicode Consortium, предоставляют довольно подробную… но очень объемную документациюЧитать полностью »

В одном недавнем подкасте о том, кто сейчас главный в Rust, вновь всплыл вопрос о том, кому быть BDFL (великодушным пожизненным диктатором), и Джереми Соллер сказал (это был чемпионский заход на приз «за преуменьшение века»): «Я считаю, Грейдон забраковал бы некоторые вещи, которые всем нам сейчас нравятся». Этим он вторит другой дискуссии на redditЧитать полностью »

Хочу поделиться своей историей расследования одной довольно необычной компиляторной оптимизации. Необычна она в том плане, что для нее производятся довольно нетривиальные математические вычисления. Приступим!

Чем я пользовался

Есть такой замечательный сайт: Compiler ExplorerЧитать полностью »

image

1. Вступление

У меня в портфолио есть несколько готовых пет-проектов на Rust, и я заметил, что позиция «а у нас уже получилась DataFrame?» нисколько меня не устраивает. Поэтому я подумал, не сделать ли мне элементарный контейнер, который решал бы мою конкретную задачу. Но этот проект вышел из-под контроля.

Год спустя, написав немало кода, я создал одну из самых быстрых библиотек датафреймов, применимую в Rust и Python. Вот мой первый официальный «Hello World» на polars, размещённый у меня в блоге. Надеюсь, что с помощью этого поста я смогу пояснить читателю некоторые решения, которые мне довелось принять при проектировании, и вам станет понятнее, как Polars работает под капотом.
Читать полностью »

Я начал программировать на Rust несколько лет назад, и это постепенно изменило мой подход к разработке программ на других языках программирования, особенно на Python. До того, как я начал использовать Rust, я обычно писал код на Python очень динамично, без подсказок типов, повсюду передавая и возвращая словари и время от времени возвращаясь к интерфейсам со «строковой типизацией». Однако, испытав на себе строгость системы типов Rust и заметив все проблемы, которые она предотвращает, я внезапно стал сильно беспокоиться всякий раз, когда возвращался к Python и не получал тех же гарантий.

Читать полностью »

Начались майские праздники, но это не значит, что дайджест новостей из мира программирования ушёл на второй план. В этой подборке пройдёмся по важным новостям IT-мира за прошедшую неделю: разработчики Arduino выпустили обновление Arduino IDE 2.1, команда Flipper Zero добавила режим сна для своего устройства, а проект Prossimo начал переписывать sudo и su на Rust.

Дайджест новостей из мира программирования #2 - 1

Читать полностью »

Ускоряем Python в сто раз при помощи менее чем ста строк на Rust - 1


Однажды на работе у нас возникла проблема с производительностью одной из наших основных Python-библиотек.

Эта библиотека формирует фундамент нашего конвейера 3D-обработки. Это довольно большая и сложная библиотека, использующая NumPy и другие научные пакеты Python для выполнения широкого спектра математических и геометрических операций.

Кроме того, наша система должна работать на мощностях компании с ограниченными ресурсами CPU, и хотя поначалу она справлялась хорошо, с ростом количества одновременных физических пользователей у нас начали возникать проблемы, а наша система едва выдерживала нагрузку.

Мы пришли к выводу, что для работы с увеличившейся нагрузкой нужно сделать систему, по крайней мере, в пятьдесят раз быстрее, и решили, что помочь в этом нам может Rust.

Так как проблемы производительности, с которыми мы столкнулись, встречаются довольно часто, мы можем воссоздать и решить их прямо здесь, в (не такой уж короткой) статье.

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

Если вы хотите сразу перейти к получившемуся коду, то читайте раздел «Подведение итогов».
Читать полностью »

microsoft-is-rewriting-core-windows-libraries-in-rust-v0-Nsy2e3-Z9k4-XXJv-6k-XV9d4a-Mmj-VKb-Th-Cj-Sh

Недавно стало известно о том, что команда разработчиков Windows 11 занимается новым типом работы — переписывает ряд модулей ядра и системных библиотек операционной системы на Rust. При этом работа уже в разгаре, это не просто анонс проекта или планы на будущее — реализация идет полным ходом. Зачем корпорации все это понадобилось?
Читать полностью »

Самая маленькая хеш-таблица в мире - 1

1 декабря я в очередной раз поучаствовал в Advent of Code, написав программу на Rust. Если интересно — код можно найти на GitHub. Тут мне хотелось бы рассказать о моём решении задачи, предлагавшейся во 2 день мероприятияЧитать полностью »


https://ajax.googleapis.com/ajax/libs/jquery/3.4.1/jquery.min.js