Вангуем

— Я покупаю это за доллар!
Робокоп

Интро

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

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

1. Storage Systems

— Aerospike (SSD, LuaJIT)
— BlazingDB (GPU)
— PumpkinDB (SPDK, LMDB, FORTH)

Мы видим так, что современные базы данных должны использовать современные технологии AVX, GPU, OpenCL. Нам кажется это логичным.

В прошлом были быстрые базы данных, которые использовали mmap (LMDB, MUMPS) и геометрию диска, особенности операционной системы, свой язык управления курсорами. В будущем базы будут напрямую управлять котнроллером SSD диска, как то spdk.io.

Системы хранения и базы данных все скучные. Хочется базу данных, которая использует особенности SSD дисков и/или OpenCL для паралельной обработки запросов. Хочется табулярную, а не реляционную или графовую структуру. Табулярные структуры давно используются в построении хранилищ и неплохо скейлятся учитывая особенности различных бекендов. Главный примеры: MUMPS, BigTable, mnesia. Для нас база данных это не черный ящик, а конструктор для построения своих храилищ.

2. Array Processing Languages

— Futhark (GPU)
— Julia (AVX)
— AutumnAI (ML)

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

В прошлом все использовали Fortran, Mathlab, R, TensorFlow и другие инструменты разных классов для извлечения информации из данных и ее процессинга. Мы видим системы будущего, построенные на современных технологиях и не хотим использовать медленные инструменты ориентированные на масс-маркет. Так как многие инструменты были созданы математиками, а не инженерами — эти вещи не ложатся на продакшин.

3. Concurrency Runtimes and Languages

— Pony (CAS, Zero-Copy, Lock-free)
— Erlang (Actor, Message passing, Lock-free)
— Rust (Language with Linear Types)

Первая взрослая система для конкурентного программирования была Ada, другие системы это E, Oz, Erlang. Erlang продержался дольше всех и до сих пор конкурирует с другими популярными рантаймами низкого качества, мультипроцессорными системами, виртуальными машинами и даже операционными системами.

Первая попытка популяризировать Compare-and-Swap семантику курсоров и структур данных без копирования была LMAX Disruptor. Pony эксплуатирует эту идею и мы хотим видеть рантаймы которые обладают этими характеристиками. Кроме того, мы являемся авторами такого рантайма.

Также у нас в активе рантайм предыдущего поколения LING, который совместим с Erlang/OTP и может работать на Xen без использования стека операционной системы.

4. Target Languages

— OCaml (GC)
— LLVM/MIR (Assembler)
— Rust (GC-free, Linear Types)
— D (GC)
— GHC (GC)

Несмотря на то, что LLVM является устаревшей технологией, которая является общим знаменателем всех ассемблеров, мы приводим этот список языков, как целевых платформ для наших рантаймов. Попытка избавиться от наследия LLVM была предпринята в проекте Go, но далека от идеала.

А пока мы рассматриваем все LLVM системы, вместе с высокоуровневыми языками, которые предоставляют широкий спектр статических гарантий. Мы не можем включить сюда С++ или С, так как гарантии для них могут предоставляться, только если этот код генерируется из моделей, где статические гарантии доказаны. Это пока не будущее, но направление в котором нужно двигаться.

5. Certified Kernels

— Coq (Tactics, Extraction)
— F* (MLTT Crypto Stack)
— Z3 (External SMT Solver)
— Lean (External MLTT Protocol)

Системы автоматического доказательства теорем раньше исользовались исключительно математиками, современные тенденции ведут к полностью верифицированым вычислительным средам, которые линкуются с верифицированными рантаймами или рантаймами со статическими гарантиями.

Мы не конкурируем с такими стеками как functor.se, которые базируются на CompCert, VST и доказательстве C программ. В том числе мы не конкурируем с seL4. Это не тот путь, которым мы хотим пойти.

Несмотря на то, что существует много систем с зависимыми типами, такие как Agda, Idris, ACL2, HOL/Isabell, мы ориентируемся на системы с открытыми терм-протоколами (Lean), Coq (как доминирующий язык программирования с зависимыми типами) и внешние SMT солверы. Наша цель — построить базовую библиотеку и часть рантайма на Coq, а потом создать под нее свой язык и ядро со статическими гарантиями. Это длительный проект который подразумевает взаимодействие с академией.

Также мы являемся авторами высокопроизводительного трастед кернела ОМ, который может использоваться как ядро с зависимыми типами и виртуальная вычислительная среда для выполнения тотальных корекурсивных программ в управляемых и доверительных окружениях: криптовалютах, финансовых языках и других системах требующих тотальности.