#prog #meme

К сожалению, жиза 🥲

#prog #sql #article

A Formalization of SQL with Nulls (pdf)

SQL is the world’s most popular declarative language, forming the basis of the multi-billion-dollar database industry. Although SQL has been standardized, the full standard is based on ambiguous natural language rather than formal specification. Commercial SQL implementations interpret the standard in different ways, so that, given the same input data, the same query can yield different results depending on the SQL system it is run on. Even for a particular system, mechanically checked formalization of all widely-used features of SQL remains an open problem. The lack of a well-understood formal semantics makes it very difficult to validate the soundness of database implementations. Although formal semantics for fragments of SQL were designed in the past, they usually did not support set and bag operations, lateral joins, nested subqueries, and, crucially, null values. Null values complicate SQL’s semantics in profound ways analogous to null pointers or side-effects in other programming languages. Since certain SQL queries are equivalent in the absence of null values, but produce different results when applied to tables containing incomplete data, semantics which ignore null values are able to prove query equivalences that are unsound in realistic databases. A formal semantics of SQL supporting all the aforementioned features was only proposed recently. In this paper, we report about our mechanization of SQL semantics covering set/bag operations, lateral joins, nested subqueries, and nulls, written in the Coq proof assistant, and describe the validation of key metatheoretic properties. Additionally, we are able to use the same framework to formalize the semantics of a flat relational calculus (with null values), and show a certified translation of its normal forms into SQL.

(thanks @daily_ponv)

Пара моментов:

В этой формализации не рассматриваются операции агрегирования и группировки.

Семантика, построенная для их формализации SQL, параметризована используемой логикой. Она может быть классической булевой (двухзначной) или же трёхзначной, как в SQL. В статье авторы показывают, что трёхзначность логики на самом деле не добавляет выразительности: они доказывают (конструктивно), что для любого запроса в трёхзначной логике есть эквивалентный в смысле семантики запрос, работающий в двухзначной логике. Обратное тоже верно.

---

Вообще, на мой взгляд, это какая-то дичь, что оптимизаторы запросов в БД до сих пор делают, не утруждаясь доказательствами корректности преобразований запросов.

Cмотрим на красную точку 30 секунд не отрываясь и очень пристально, а потом переводим взгляд на стену и начинаем быстро моргать.

Работает это из-за перенасыщения одной группы цветовых рецепторов в глазу (сине-желтые) и синие перенасыщаются, а желтые -- нет. Вот тут описание феномена: https://www.verywellmind.com/what-is-an-afterimage-2795828

Когда решал соревнование с саккадами, то столько нового узнал про зрение. Там костыль на костыле. Хуже чем в любом продакшне.

Поддерживать отношения со своим мозгом — хорошая идея.

Резидент «Сколково» создал замену популярного во всём мире британского компьютера Raspberry Pi — и назвал её Repka Pi.

Примечательно, что предзаказы принимают уже сейчас (причём исключительно через форму заказа, без указанной цены), а степень готовности — "Подготовка начала производства".

Ы - ымпортозамещение.

#prog #gamedev #article

Cramming 'Papers, Please' Onto Phones (перевод)

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

P. S.: Слава Арстоцке!

#prog #gamedev #article

Localizing Papers, Please (часть 1, часть 2)

(разбито на две части из-за ограничений tumblr на размер постов)

Там кстати Rust 1.63 вышел. TL;DR интересного (по моему мнению):

— из компилятора выкинули старый borrowck (я так и не понял что это меняет)
— [x; 0] теперь дропает x (ранее был баг из-за которого это было эквивалентно mem::forget)
— турборыбу можно использовать для дженериков в функциях с APIT [1]
— null и null_mut теперь работают с extern типами
— std теперь поддерживает nintendo 3DS 👀
— write!/print! теперь дропают tmp раньше
— Layout теперь реализует Hash
— needs_drop теперь работает для не Sized типов
— Termination теперь реализован для большего количества типов [2]
— Стабилизорована / const-ифицирована куча функций (мне лень их все перечислять) (кстати к некоторым я приложил лапки), в том числе стабилизировали scoped треды (!!!), более безопасные типы для работы с платформо зависимым IO и Mutex::new в const контексте
— Добавили в документацию заметку про то, что safety гарантии раста никак не защищают от /proc/self/mem
— У коллекций улучшена документация на счёт того, что происходит при логических ошибках (например в реализации Ord)

[blog] [github release]

[1]: это позволяет делать такое:

fn f<T>(f: impl FnOnce() -> T) { ... }
f::<u32>(|| 0);

раньше ::<u32> было нельзя писать из-за impl Trait в аргументах. сам APIT явно задать нельзя, но это может быть и плюсом, когда явно хочется задать только другие параметры.

[2]: Termination это трейт для типов, которые можно вернуть из main. В этом релизе добавили реализации для Infallible и Result<impl Termination, impl Debug> (ранее можно было возвращать только Result<(), _>, Result<!, _> и Result<Infallible, _>).

#prog #rust #rustreleasenotes

хочу миленькое лёгенькое платьице с клубничным паттерном а не вот это вот всё

#prog #rust #meme

https://twitter.com/iamdevloper/status/1258012522348716038

(thanks @ozkriff)

Ай

О некоторых вещах Вафель всё же зря умолчал.

Первое — это реализация типов для IO safety. Новые типы для Unix (OwnedFd, BorrowedFd) и Windows (OwnedHandle, HandleOrNull, HandleOrInvalid, BorrowedHandle, OwnedSocket, BorrowedSocket), полезные в основном для FFI, позволяют:

* на уровне типов — а не устных соглашений — описать, как именно функция обращается с сырыми ручками от OS;
* опять-таки, на уровне типов исключить возможность забыть обработку возможных невалидных значений;
* задействовать niche optimisation, чтобы не иметь оверхед на тег для опциональных значений;
* использовать их непосредственно в FFI-сигнатурах из-за #[repr(transparent)].

Не та вещь, которую будешь использовать каждый день, но для написания биндингов определённо полезна.

Вторая вещь — это array::from_fn (которая, кстати, реализована в терминах array::map). Пример использования:

let array = core::array::from_fn(|i| i);
assert_eq!(array, [0, 1, 2, 3, 4]);

Чем примечательна эта функция? Ну... В C есть фича под названием designated initializers. Обычно её вспоминают в связи со структурами:

struct A { int x; int y; int z; };
struct A a{.y = 2, .x = 1};

, но почему-то мало кто знает, что их можно использовать и с массивами:

int n[5] = {[4]=5,[0]=1}; // 1,0,0,0,5

array::from_fn позволяет (до некоторой степени) сымитировать это поведение:

// look ma no types!
let arr = std::array::from_fn(|i| match i {
4 => 5,
0 => 1,
_ => 0,
});

То есть Rust вынес в библиотеку то, что в C зашито в язык!

#game #video

The Music Of Metal Gear Rising Is Smarter Than You Think

ВНИМАНИЕ: СОДЕРЖИТ СПОЙЛЕРЫ К ИГРЕ ДЕВЯТИЛЕТНЕЙ ДАВНОСТИ

#prog #math

Вы когда-нибудь задумывались, как именно процессоры считают значения тригонометрических функций? Нет, не через ряды Тейлора — они слишком медленно сходятся. Через последовательное приближение половинками углов и сравнения с таблицей предвычисленных значений.

Подробнее в Википедии.

#prog #rust

github.com/rust-lang/rust/pull/95977 ❤️

Плюсы все делают лучше