Добрый день! Я пробовал ещё до релиза. Мне нравится гораздо больше, чем VS Code. По дизайну, по тому, как спроектирован интерфейс. Это во многом эмоционально, но всё-таки Zed мне милее, чем VS Code.
Я слышал мнение, что не обязательно делать ставку на резюме. Что современные сайты вакансий мертвы (уверен в этом на 65%). А искать работу нужно через нетворкинг, через знакомых, говоря по русски.
Приветствую! Я тут готовлю заметки для статьи про облегчённые методы оптимизации. Вопрос состоит в том, возможно ли добиться большого прироста производительности, прилагая в разы меньшие усилия. Я думаю, что это в некоторых случаях возможно. По крайней мере, программисту стоит знать базовые приёмы.
Есть три направления оптимизации - оптимизация расхода памяти, оптимизация времени выполнения и оптимизация времени компиляции. Обычно мы приходим к тому, нельзя прибавить одно, не убавив что-то другое.
Меня волнует в первую очередь оптимизация времени выполнения. А вот время компиляции релизных сборок я не прочь как раз увеличить!
Вообще, очень медленная операция в современных компьютерах - это чтение и запись в оперативную памяти. А ввод вывод бывает порой ещё хуже...
По этому очень важно, чтобы ваш код как можно меньше бегал за данными в плашки, и как можно больше работал с данными в кэше процессора (желательно L1) а то и в регистрах.
Вы наверное все знаете, что есть O большое, бывают алгоритмы константные, бывают линейные, логарифмические, квадратичные, экспоненциальные... Обычно, чем меньше O большое, тем быстрее работает алгоритм.
Например, время поиска элемента в хэш-таблице всегда примерно одно и тоже, и не должно меняться в зависимости от того, сколько в ней элементов. А бинарный поиск работает за логарифмическое время.
Казалось бы, хэш-таблица всегда должна выигрывать. Ан нет! O большое позволяет оценить примерную скорость роста затрат по мере увеличения входных данных. Кроме этой оценки есть ещё и коэффициенты. Массив, по которому мы проходимся бинарным поиском может уместиться в кэш, а хэш-таблица нет. Может быть, пока она высчитывает хэш, мы уже десять раз успеем бинарным поиском пройтись по массиву.
Это реальный случай. Кажется, тогда код запускался на микроконтроллере.
Я слышал фразу, что самый главный приём оптимизации - это профилирование. Чтобы что-то оптимизировать, нужно сначала это измерить.
Буду рад, если вы подскажете и другие приёмы.
Где-то ещё я слышал, что оптимизация - это во многом перебор различных приёмов. Вся штука в том, что они друг-друга нивелируют, и нужно подобрать такую комбинацию, которая даст наилучший эффект.
Вообще интересно, что будет, если дать ИИ агентам фрагмент кода, и таблицу способов, как его можно оптимизировать. Пущай перебирает! Небось так можно и глобально оптимальный вариант найти. Главное потом проверить, что он ничего не поломал...
Как жалко, чтоб большинство языков программирования не позволяют доказывать корректность, как мой ненаглядный Lean!
В компиляторах есть такая техника - супероптимизация. Она состоит в том, что мы берём кусочек кода, который хотим оптимизировать, и перебираем все возможные варианты машинного кода, меньшего определённой длины. Так мы ищем самый быстрый фрагмент, про который доказано, что он делает то же, что и исходный код. Ясное дело, что там есть много-много хитростей, чтобы отсечь большую часть невалидных вариантов, но всё равно это работает ужасно медленно.
Обычно супероптимизацию не применяют. Я слышал, её могут использовать, чтобы скомпилировать небольшие кусочки кода, которые потом будет использовать компилятор. Что-то вроде библиотеки оптимизированных фрагментов.
Приветствую! Доказать, что в коде нет багов мешает не только проблема останова, но и Теорема Гробовой Крышки. Она же Теорема Райса. Она утверждает, что если какое-то свойство встречается у одних программ, и не встречается у других, мы не можем для любой из программ доказать, что она обладает этим свойством. Но тут ключевое слово "для любой". Есть куча программ, для которых мы можем доказать очень многие свойства!
Проблема останова разрешима! Пусть и не в общем случае. Но есть даже специальные языки программирования, которые называются тотальными. Если программа на них скомпилировалась, можно быть уверенным: она завершит свою работу.
Один из тотальных языков - это любимый мною Lean. В нём можно доказать, что функция обязательно завершается. А если это так, то Теорема Гробовой Крышки немного ослабляет свои позиции, и мы можем доказывать разные свойства о наших функциях.
Тотальные языки - это очень интересная тема. О ней я выпущу отдельную статью.
Мне очень интересно функциональное программирование. Я сейчас изучаю язык Lean 4. Это функциональный язык программирование и в то же время программа для доказательства теорем. У него есть одна отличная особенность: если на объект не осталось ссылок, и нам нужно создать его копию, объект будет изменён, а не скопирован. Это позволяет сильно повысить эффективность программы.
Но самая интересная особенность - это зависимы типы. Они позволяют выражать любые свойства программы в типах и доказывать их. Мы можем доказать корректность нужной нам программмы, и тогда не нужно будет ни одного теста! Хотя написать доказательство может быть сложнее, чем написать тесты, но зато доказательство практически гарантирует, что ошибок нет! Это всё равно, что написать бесконечное количество тестов!
Думаю, что тесты и доказательства могут идти рука об руку. Тесты используются для поиска багов на этапе разработки, а доказательства пишутся перед крупным релизом, и в первую очередь для критических частей.
Одно омрачает мне радость: язык очень молодой и для него очень мало прикладных библиотек. Гораздо меньше, чем для Haskell.
А вообще я хочу написать про Lean статью. Буду рад, если вы зададите вопросы, а ещё лучше, если попробуете сами попрограммировать на Lean, и поделитесь своим мнением.
Добрый день! Было интересно прочитать про функциональное программирование в реальном мире. Мне нравится идея неизменяемого состояния. Datalog мне симпатичен, хотя я его не использовал.
Один из моих любимых языков на данный момент - это Lean 4. Он такой классный! Там мощнейшая система типов. С зависимыми типами. Она очень выразительная. Одна беда. Библиотек почти нет для прикладного программирования. А ведь этот язык мог бы стать новым Haskell!
Я хорошо отношусь к Clojure, но это язык не моего духа. Я просто не представляю, как можно писать большие программы без статических типов! А ведь в Clojure чаще всего вообще типов не определяют! Никаких вам структур. Только хэш-таблицы. И проверки типов в рантайме. Не представляю, как так можно жить! Это не мой стиль. Мне нравится, когда можно определить все поля заранее, задать их тип, и определить операции над структурой.
Но тут есть одна интересная деталь. У того банка распределённая система. Как они синхронизируют время в своих микросервисах? Я слышал про Логические часы. Их создал Лэмпорт. Они используются для того, чтобы восстанавливать причинно следственные связи.
Скажите, вы что-то слышали про логические часы? Было бы интересно прочитать.
Ура! Я так ждал! Я использовал Gemma 3 12b когда отключали интернет. Вот не знаю, будет ли эта версия лучше, чем предыдущая. С одной стороны, она лучше обучена, а с другой, она сильно меньше.
Хм... Возможно, сложность может уменьшиться, если программист искусен? Например, он может применить хорошие паттерны, а то и вообще монады и моноиды...
Нужно всё-таки признать, что способы чуть-чуть уменьшить сложность всё-таки есть. Языки более высокого уровня могут уменьшить сложность. Использование библиотек позволяет перенести сложность с того, кто пишет продакшен код на автора библиотеки.
Есть хитрые техники, которые сокращают код, если их уметь применять.
Добрый день! Спасибо вам за статью! Я когда-то писал парсер-комбинаторы на Лиспе. Похоже, что подходящей оптимизации не было, комбинаторы работали очень медленно. В языке программирования Lean комбинаторы чуть ли не в стандартную библиотеку встроены. Скажите, может быть, вы не против посмотреть язык Lean, и немного попрограммировать на нём? Он вообще имеет двоякую природу. С одной стороны он язык программирования общего назначения, похожий на Haskell, только там гораздо более мощная система типов - зависимые типы. С другой - средство доказательства теорем. Мне было забавно сегодня доказать теоремы про алгоритм Евклида. Правда, на индуктивном доказательстве я застрял. Но это нормально. Математику я только изучаю.
Вообще мне кажется, что в таких случаях могут помочь программы проверки моделей. Они позволяют смоделировать дизайн программы, и посмотреть, есть ли у него нужные свойства! Может быть, если предварительно написать модель на Alloy (Вот по нему книжка), а потом заставить ИИ работать по этой модели, удастся хоть немного повысить качество?
Вообще, смоделировать программу может быть полезно даже при обычной разработке. Обычно модель получается не очень большой. По крайней мере, гораздо меньше самой программы.
Может быть, тут есть синьёры, которые могли бы проверить этот подход на своих пет-проектах? Мне было бы интересно посмотреть на результат.
Мне вот интересен Lean 4. Это одновременно и язык программирования, и помощник для доказательств. Он помогает изучать математику. Если ты доказал теорему, и верифицировал доказательство в Lean, можно быть практически уверенным, что доказательство правильное.
Полагаю, что его следует сравнивать в первую очередь с Си. Я, с одной стороны Си люблю, с другой мне многое в нём очень не нравится. Я рад, что ему была найдена достойная замена.
И да, он безопаснее, чем C. Стандартная библиотека на порядок лучше, чем в Си. На счёт того, кто быстрее... Тут, наверное, Си немного выиграет, потому что в нём есть оптимизации на основе UB и отсутствуют многие проверки. Зато в Zig гораздо проще работать с SIMD! Но в любом случае, Zig - это очень быстрый язык. Хотя правильно написанный код на Julia может оказаться быстрее неправильно написанного кода на Zig...
Самое любимое преимущество Zig - это алгебраические типы данных. А именно, маркированное объединение (tagged union) - тип сумма. В C есть union, но он не хранит информации о том, какой именно вариант сейчас активен. В Zig union(enum) хранит тег, и его можно красиво сочетать со switch ```
Это очень помогло мне, когда я писал компилятор, представлять абстрактное синтаксическое дерево. Тип сумма - это один из базовых способов описания мира.То, что его нет в большинстве популярных языков - это какое-то кошмарное недоразумение. Тут уже не понятно, кто виноват.
Другой большое преимущество - это comptime - вычисления во время компиляции. Он позволяет, например, делать регулярные выражения, которые оптимизируются во время компиляции. Хотя тут возникает проблема, что само регулярное выражение должно быть известно во время компиляции. Но это проблема библиотеки регулярных выражений. Можно написать и обычным образом.
А ведь в comptime можно производить вычисления над типами... Так реализованы обобщённые типы:
Если сравнивать безопасность Си и Zig, то побеждает конечно же Zig. В нём все указатели, которые могут содержать Null обязательно помечаются, и если мы хотим из разыменовать, нам нужно будет их проверить, что они не Null.
fn foo(a: ?*GenUsize) void {
if (a) |gen| { // Вот тут мы проверяем, что указатель не null, и кладём его значение в gen, если он таки не null.
std.debug.print("First: {}, Second: {}\n", .{ gen.first, gen.second });
} else {
std.debug.print("No value\n", .{});
}
}
Работа с памятью заметно улучшена, по сравнению с Си. Для выделения памяти используется специальный объект - аллокатор. Если функция решила выделить память, она должна принимать аллокатор в качестве параметра:
const std = @import("std");
/// Создаёт динамический массив целых чисел от 0 до n-1,
/// возвращает срез (slice). Вызывающий отвечает за освобождение памяти.
fn createRange(allocator: std.mem.Allocator, n: usize) ![]u64 {
// Выделяем память под n элементов
const slice = try allocator.alloc(u64, n);
// Заполняем значениями
for (slice, 0..) |*item, i| {
item.* = @intCast(i);
}
return slice;
}
pub fn main() !void {
// Используем GeneralPurposeAllocator для отслеживания утечек
var gpa = std.heap.GeneralPurposeAllocator(.{}){};
defer {
const status = gpa.deinit();
if (status == .leak) {
std.debug.print("Обнаружена утечка памяти!\n", .{});
}
}
const allocator = gpa.allocator();
// Вызываем нашу функцию
const numbers = try createRange(allocator, 10);
defer allocator.free(numbers); // освобождаем при выходе из scope
// Печатаем результат
for (numbers) |num| {
std.debug.print("{} ", .{num});
}
std.debug.print("\n", .{});
}
Этих аллокаторов есть несколько видов, самые полезные - это GeneralPurposeAllocator и аллокатор арена.
GPA просто позволяет выделять куски памяти, а потом их освобождать. Каждый выделенный кусок нужно один раз освободить.
Арена же позволяет на сначала выделить много-много кусков памяти, но очищаем мы их все разом! Это очень удобно, и решает множество проблем с утечками и двойным освобождением памяти.
Замечательно, что аллокаторы имеют один интерфейс, так что для выделения памяти функцией можно использовать как арену, так и GPA, в зависимости от того, чего мы хотим добиться!
В Zig есть срезы (слайсы). В них хранится как указатель на массив, так и его длина. При попытке доступа к элементу может быть проверка на выход за границу массива, но это зависит от режима.
Ещё одно прекрасное преимущество Zig - это обработка ошибок. Начнём с того, что в отличие от Си она тут хотя бы есть! То, что есть в Си - не считается, это костыли и прошлый век.
В Zig под обработку ошибок выделена отдельная система. Функция может быть помечена как способная вернуть ошибку. Ошибку можно либо прокинуть вверх при помощи try, либо отловить при помощи catch. Эти ключевые слова в Zig действуют не так, как в других языках.
const MyError = error {
Ploho, // Возможноые варианты ошибки
Ujasno,
};
fn baz(a: usize) MyError!void { // Помечаем, что функция вернёт либо ошибку типа MyError, либо void
if (a % 2 == 0) {
return error.Ploho;
} if (a % 3 == 0) {
return error.Ujasno;
}
}
pub fn main() void {
try baz(1); // Просто выполнится, так-как baz не возвращает ошибку. try ничего не сделает
baz(2) catch |err| { // Перехватываем ошибку, и что-то с ней делаем
std.debug.print("Error: {}\n", .{err});
};
try baz(4); // Так-как baz вернёт ошибку, оператор try просто вернёт её из функции.
Короче говоря, Zig побеждает C по многим параметрам. Это я ещё не все перечислил. Составить ему конкуренцию могут только Rust и C++. Что же он противопоставит им? Простоту. Zig очень простой язык. Говорят, его реально, без шуток можно выучить за 21 день, если вы уже умеете программировать. Я слышал отзыв одной компании, которая использовала Zig, что ей не нужно было нанимать тех, кто его уже знает. Они могли просто научить ему программиста сами.
C++ он побеждает ещё и тем, что в Zig нет такого адского количества неопределённого поведения. А ещё в C++ куча легаси, оставшегося за пятьдесят лет развития, и он унаследовал множество недостатков Си! Его очень трудно знать хорошо.
Rust, наверное, самый сильный противник. Думаю, что многим он подойдёт больше. С другой стороны, в Zig управление памятью полностью ручное, а в Rust оно автоматическое. Часто это плюс, но я могу представить ситуацию, когда это минус. Хотя не знаю, что это за ситуацию.
И вообще, тут много вкусовщины. Мне Zig нравится больше всего. Rust я не осилил. C++ мне категорически не нравится.
Очень советую попробовать написать на Zig достаточно большую программу, чтобы почувствовать, ваш это язык, или не ваш. Если вы любите C, то скорее всего полюбите и Zig.
Добрый день!
Я очень благодарю вас за эти статьи. Мне они кажутся очень полезными и важными.
Мой вам совет: меняйте картинку на превью, чтобы была какая-то драматургия, чтобы образ развивался от статьи к статье.
Добрый день!
Я пробовал ещё до релиза. Мне нравится гораздо больше, чем VS Code.
По дизайну, по тому, как спроектирован интерфейс.
Это во многом эмоционально, но всё-таки Zed мне милее, чем VS Code.
Добрый день!
Скажите пожалуйста, а каков общий алгоритм оптимизации любой программы?
Может быть, вы знаете книги, в которых его можно посмотреть?
Я слышал мнение, что не обязательно делать ставку на резюме. Что современные сайты вакансий мертвы (уверен в этом на 65%). А искать работу нужно через нетворкинг, через знакомых, говоря по русски.
Вы согласны с этим мнением?
Приветствую!
Я тут готовлю заметки для статьи про облегчённые методы оптимизации.
Вопрос состоит в том, возможно ли добиться большого прироста производительности, прилагая в разы меньшие усилия. Я думаю, что это в некоторых случаях возможно. По крайней мере, программисту стоит знать базовые приёмы.
Есть три направления оптимизации - оптимизация расхода памяти, оптимизация времени выполнения и оптимизация времени компиляции. Обычно мы приходим к тому, нельзя прибавить одно, не убавив что-то другое.
Меня волнует в первую очередь оптимизация времени выполнения. А вот время компиляции релизных сборок я не прочь как раз увеличить!
Вообще, очень медленная операция в современных компьютерах - это чтение и запись в оперативную памяти. А ввод вывод бывает порой ещё хуже...
По этому очень важно, чтобы ваш код как можно меньше бегал за данными в плашки, и как можно больше работал с данными в кэше процессора (желательно L1) а то и в регистрах.
Вы наверное все знаете, что есть O большое, бывают алгоритмы константные, бывают линейные, логарифмические, квадратичные, экспоненциальные...
Обычно, чем меньше O большое, тем быстрее работает алгоритм.
Например, время поиска элемента в хэш-таблице всегда примерно одно и тоже, и не должно меняться в зависимости от того, сколько в ней элементов. А бинарный поиск работает за логарифмическое время.
Казалось бы, хэш-таблица всегда должна выигрывать. Ан нет! O большое позволяет оценить примерную скорость роста затрат по мере увеличения входных данных. Кроме этой оценки есть ещё и коэффициенты. Массив, по которому мы проходимся бинарным поиском может уместиться в кэш, а хэш-таблица нет. Может быть, пока она высчитывает хэш, мы уже десять раз успеем бинарным поиском пройтись по массиву.
Это реальный случай. Кажется, тогда код запускался на микроконтроллере.
Я слышал фразу, что самый главный приём оптимизации - это профилирование. Чтобы что-то оптимизировать, нужно сначала это измерить.
Буду рад, если вы подскажете и другие приёмы.
Где-то ещё я слышал, что оптимизация - это во многом перебор различных приёмов. Вся штука в том, что они друг-друга нивелируют, и нужно подобрать такую комбинацию, которая даст наилучший эффект.
Вообще интересно, что будет, если дать ИИ агентам фрагмент кода, и таблицу способов, как его можно оптимизировать. Пущай перебирает! Небось так можно и глобально оптимальный вариант найти. Главное потом проверить, что он ничего не поломал...
Как жалко, чтоб большинство языков программирования не позволяют доказывать корректность, как мой ненаглядный Lean!
В компиляторах есть такая техника - супероптимизация. Она состоит в том, что мы берём кусочек кода, который хотим оптимизировать, и перебираем все возможные варианты машинного кода, меньшего определённой длины. Так мы ищем самый быстрый фрагмент, про который доказано, что он делает то же, что и исходный код. Ясное дело, что там есть много-много хитростей, чтобы отсечь большую часть невалидных вариантов, но всё равно это работает ужасно медленно.
Обычно супероптимизацию не применяют. Я слышал, её могут использовать, чтобы скомпилировать небольшие кусочки кода, которые потом будет использовать компилятор. Что-то вроде библиотеки оптимизированных фрагментов.
Извините, а как включить турбоквант в LM Studio для Gemma 4 E4B?
Эх... С монадами код был бы краше...
Приветствую!
Доказать, что в коде нет багов мешает не только проблема останова, но и Теорема Гробовой Крышки. Она же Теорема Райса.
Она утверждает, что если какое-то свойство встречается у одних программ, и не встречается у других, мы не можем для любой из программ доказать, что она обладает этим свойством.
Но тут ключевое слово "для любой". Есть куча программ, для которых мы можем доказать очень многие свойства!
Проблема останова разрешима! Пусть и не в общем случае. Но есть даже специальные языки программирования, которые называются тотальными. Если программа на них скомпилировалась, можно быть уверенным: она завершит свою работу.
Один из тотальных языков - это любимый мною Lean. В нём можно доказать, что функция обязательно завершается. А если это так, то Теорема Гробовой Крышки немного ослабляет свои позиции, и мы можем доказывать разные свойства о наших функциях.
Тотальные языки - это очень интересная тема. О ней я выпущу отдельную статью.
Мне очень интересно функциональное программирование.
Я сейчас изучаю язык Lean 4. Это функциональный язык программирование и в то же время программа для доказательства теорем.
У него есть одна отличная особенность: если на объект не осталось ссылок, и нам нужно создать его копию, объект будет изменён, а не скопирован. Это позволяет сильно повысить эффективность программы.
Но самая интересная особенность - это зависимы типы. Они позволяют выражать любые свойства программы в типах и доказывать их. Мы можем доказать корректность нужной нам программмы, и тогда не нужно будет ни одного теста! Хотя написать доказательство может быть сложнее, чем написать тесты, но зато доказательство практически гарантирует, что ошибок нет! Это всё равно, что написать бесконечное количество тестов!
Думаю, что тесты и доказательства могут идти рука об руку. Тесты используются для поиска багов на этапе разработки, а доказательства пишутся перед крупным релизом, и в первую очередь для критических частей.
Одно омрачает мне радость: язык очень молодой и для него очень мало прикладных библиотек. Гораздо меньше, чем для Haskell.
А вообще я хочу написать про Lean статью. Буду рад, если вы зададите вопросы, а ещё лучше, если попробуете сами попрограммировать на Lean, и поделитесь своим мнением.
Добрый день!
Было интересно прочитать про функциональное программирование в реальном мире.
Мне нравится идея неизменяемого состояния.
Datalog мне симпатичен, хотя я его не использовал.
Один из моих любимых языков на данный момент - это Lean 4. Он такой классный! Там мощнейшая система типов. С зависимыми типами. Она очень выразительная. Одна беда. Библиотек почти нет для прикладного программирования. А ведь этот язык мог бы стать новым Haskell!
Я хорошо отношусь к Clojure, но это язык не моего духа. Я просто не представляю, как можно писать большие программы без статических типов! А ведь в Clojure чаще всего вообще типов не определяют! Никаких вам структур. Только хэш-таблицы. И проверки типов в рантайме. Не представляю, как так можно жить! Это не мой стиль. Мне нравится, когда можно определить все поля заранее, задать их тип, и определить операции над структурой.
Но тут есть одна интересная деталь. У того банка распределённая система. Как они синхронизируют время в своих микросервисах? Я слышал про Логические часы. Их создал Лэмпорт. Они используются для того, чтобы восстанавливать причинно следственные связи.
Скажите, вы что-то слышали про логические часы? Было бы интересно прочитать.
Мне тоже очень нравится семейство Gemma. Четвёртая версия показалась мне сравнимой с Gemini 3. Конечно, с поправкой на размер.
Но мне очень интересно провести один эксперимент, для которого у меня нет вычислительных мощностей.
Один человек заметил, что если подобрать и продублировать определённый блок слоёв модели, у неё резко улучшаются показатели.
https://dnhkng.github.io/posts/rys/
https://dnhkng.github.io/posts/rys-ii/
И вот мне интересно, можно ли так улучшить модели серии Gemma 4? Это было бы шикарно!
Вот тред в обсуждении модели: https://huggingface.co/google/gemma-4-31B-it/discussions/60
Буду рад, если кто-нибудь там отпишется.
Ура!
Я так ждал! Я использовал Gemma 3 12b когда отключали интернет. Вот не знаю, будет ли эта версия лучше, чем предыдущая. С одной стороны, она лучше обучена, а с другой, она сильно меньше.
Хм... Возможно, сложность может уменьшиться, если программист искусен? Например, он может применить хорошие паттерны, а то и вообще монады и моноиды...
Нужно всё-таки признать, что способы чуть-чуть уменьшить сложность всё-таки есть.
Языки более высокого уровня могут уменьшить сложность. Использование библиотек позволяет перенести сложность с того, кто пишет продакшен код на автора библиотеки.
Есть хитрые техники, которые сокращают код, если их уметь применять.
Добрый день!
Спасибо вам за статью!
Я когда-то писал парсер-комбинаторы на Лиспе. Похоже, что подходящей оптимизации не было, комбинаторы работали очень медленно.
В языке программирования Lean комбинаторы чуть ли не в стандартную библиотеку встроены.
Скажите, может быть, вы не против посмотреть язык Lean, и немного попрограммировать на нём?
Он вообще имеет двоякую природу. С одной стороны он язык программирования общего назначения, похожий на Haskell, только там гораздо более мощная система типов - зависимые типы.
С другой - средство доказательства теорем. Мне было забавно сегодня доказать теоремы про алгоритм Евклида. Правда, на индуктивном доказательстве я застрял. Но это нормально. Математику я только изучаю.
В любом случае, штука интересная.
Каноническая IDE для Lean - это VSCode. Там работает языковой сервер, который даёт очень много различных подсказок.
Вообще мне кажется, что в таких случаях могут помочь программы проверки моделей. Они позволяют смоделировать дизайн программы, и посмотреть, есть ли у него нужные свойства!
Может быть, если предварительно написать модель на Alloy (Вот по нему книжка), а потом заставить ИИ работать по этой модели, удастся хоть немного повысить качество?
Вообще, смоделировать программу может быть полезно даже при обычной разработке. Обычно модель получается не очень большой. По крайней мере, гораздо меньше самой программы.
Может быть, тут есть синьёры, которые могли бы проверить этот подход на своих пет-проектах? Мне было бы интересно посмотреть на результат.
Мне вот интересен Lean 4. Это одновременно и язык программирования, и помощник для доказательств. Он помогает изучать математику. Если ты доказал теорему, и верифицировал доказательство в Lean, можно быть практически уверенным, что доказательство правильное.
Я для работы с Unicode использую вот эту библиотеку:
https://codeberg.org/atman/zg
Полагаю, что его следует сравнивать в первую очередь с Си.
Я, с одной стороны Си люблю, с другой мне многое в нём очень не нравится. Я рад, что ему была найдена достойная замена.
И да, он безопаснее, чем C. Стандартная библиотека на порядок лучше, чем в Си. На счёт того, кто быстрее... Тут, наверное, Си немного выиграет, потому что в нём есть оптимизации на основе UB и отсутствуют многие проверки. Зато в Zig гораздо проще работать с SIMD! Но в любом случае, Zig - это очень быстрый язык. Хотя правильно написанный код на Julia может оказаться быстрее неправильно написанного кода на Zig...
Самое любимое преимущество Zig - это алгебраические типы данных. А именно, маркированное объединение (tagged union) - тип сумма. В C есть union, но он не хранит информации о том, какой именно вариант сейчас активен. В Zig union(enum) хранит тег, и его можно красиво сочетать со switch
```
Это очень помогло мне, когда я писал компилятор, представлять абстрактное синтаксическое дерево. Тип сумма - это один из базовых способов описания мира.То, что его нет в большинстве популярных языков - это какое-то кошмарное недоразумение. Тут уже не понятно, кто виноват.
Другой большое преимущество - это comptime - вычисления во время компиляции. Он позволяет, например, делать регулярные выражения, которые оптимизируются во время компиляции. Хотя тут возникает проблема, что само регулярное выражение должно быть известно во время компиляции. Но это проблема библиотеки регулярных выражений. Можно написать и обычным образом.
А ведь в comptime можно производить вычисления над типами... Так реализованы обобщённые типы:
Если сравнивать безопасность Си и Zig, то побеждает конечно же Zig.
В нём все указатели, которые могут содержать Null обязательно помечаются, и если мы хотим из разыменовать, нам нужно будет их проверить, что они не Null.
Работа с памятью заметно улучшена, по сравнению с Си. Для выделения памяти используется специальный объект - аллокатор. Если функция решила выделить память, она должна принимать аллокатор в качестве параметра:
Этих аллокаторов есть несколько видов, самые полезные - это GeneralPurposeAllocator и аллокатор арена.
GPA просто позволяет выделять куски памяти, а потом их освобождать. Каждый выделенный кусок нужно один раз освободить.
Арена же позволяет на сначала выделить много-много кусков памяти, но очищаем мы их все разом! Это очень удобно, и решает множество проблем с утечками и двойным освобождением памяти.
Замечательно, что аллокаторы имеют один интерфейс, так что для выделения памяти функцией можно использовать как арену, так и GPA, в зависимости от того, чего мы хотим добиться!
В Zig есть срезы (слайсы). В них хранится как указатель на массив, так и его длина. При попытке доступа к элементу может быть проверка на выход за границу массива, но это зависит от режима.
Ещё одно прекрасное преимущество Zig - это обработка ошибок. Начнём с того, что в отличие от Си она тут хотя бы есть! То, что есть в Си - не считается, это костыли и прошлый век.
В Zig под обработку ошибок выделена отдельная система. Функция может быть помечена как способная вернуть ошибку. Ошибку можно либо прокинуть вверх при помощи try, либо отловить при помощи catch. Эти ключевые слова в Zig действуют не так, как в других языках.
Короче говоря, Zig побеждает C по многим параметрам. Это я ещё не все перечислил. Составить ему конкуренцию могут только Rust и C++. Что же он противопоставит им? Простоту. Zig очень простой язык. Говорят, его реально, без шуток можно выучить за 21 день, если вы уже умеете программировать. Я слышал отзыв одной компании, которая использовала Zig, что ей не нужно было нанимать тех, кто его уже знает. Они могли просто научить ему программиста сами.
C++ он побеждает ещё и тем, что в Zig нет такого адского количества неопределённого поведения. А ещё в C++ куча легаси, оставшегося за пятьдесят лет развития, и он унаследовал множество недостатков Си! Его очень трудно знать хорошо.
Rust, наверное, самый сильный противник. Думаю, что многим он подойдёт больше. С другой стороны, в Zig управление памятью полностью ручное, а в Rust оно автоматическое. Часто это плюс, но я могу представить ситуацию, когда это минус. Хотя не знаю, что это за ситуацию.
И вообще, тут много вкусовщины. Мне Zig нравится больше всего. Rust я не осилил. C++ мне категорически не нравится.
Очень советую попробовать написать на Zig достаточно большую программу, чтобы почувствовать, ваш это язык, или не ваш. Если вы любите C, то скорее всего полюбите и Zig.