Corrode, проект транслятора из C в Rust, получил финансирование Mozilla

Т.е., по мнению улыбчивых дурачков, это нужно только для того, чтобы распилить часть бюджета Mozilla.
На параллельном программировании можно зарабатывать
А вот транслятор с C в Rust и деньги... Эту мысль развить сможете? Смайликов хватит?

Хахаха :-) Совсем уже плохо с думалкой, да? :-)

Не вы ли приплели сентенцию «копирующими конструкторами и прочими прочими SFINAE» в данный тред?

Видимо, совсем плохо, да :-) Поинт в том, что эти всякие копирующие конструкторы и прочие прочие SFINAE - боль ещё та :-) Должна же она чем-то окупаться, эта муть :-) Лол :-)

Не поминай имя Гёделя всуе, отрок. Математики почему-то до сих пор чем-то занимаются, а не разбежались плакать по углам.

Благодаря ему и не разбежались.

А если ты хотел сказать про проблему остановки

Я хотел сказать то, что сказал.

а от тупых или не очень ошибок, приводящих к сегфолтам, перезаписыванию памяти и прочим remote code execution

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

Примеры:

генерация быстрого кода, быстрая разработка, безопасность, выразительность: HQ9+

генерация быстрого кода, быстрая разработка, безопасность, выразительность: С

генерация быстрого кода, быстрая разработка, безопасность, выразительность: какой-нибудь интерпретируемый язык с проверкой границ массивов, переполнений и т.д.

генерация быстрого кода, быстрая разработка, безопасность, выразительность: Program extraction из proof checker'ов

Rust не будет ни эффективным, ни безопасным.

Совсем уже плохо с думалкой, да?

Да, не удается понять то, что вы пытаетесь сказать.

Поинт в том, что эти всякие копирующие конструкторы и прочие прочие SFINAE - боль ещё та

Да? Ну ладно. Хотя для тех, для кого эта боль, уже давно есть возможность зарабатывать программируя на Java. А через пару-тройку лет, может быть, будет и возможность зарабатывать программируя на Rust-е.

Я хотел сказать то, что сказал.

Э? Наличие в каждой достаточно сложной формальной системе истинных, но недоказуемых утверждений каким-то образом мешает верифицировать вот эту конкретную программу, или мешает построить программу таким образом, чтобы её корректность можно было доказать?

Или вам обязательно нужны только программы, которые могут доказать свою собственную корректность?

Rust не будет ни эффективным, ни безопасным.

Доказать, что программа не пишет куда не надо, если она сконструирована по определенным правилам, это не проблему остановки решить. Так что потенциально и практически Rust безопасен.

генерация быстрого кода, быстрая разработка, безопасность, выразительность

А я из пяти пунктов могу: вышеуказанное плюс «язык - не Rust»

Да, не удается понять то, что вы пытаетесь сказать.

Так ты же не понял что финансирование, о котором поведал Джеймс и является главной мотивацией работы над транслятором C -> Rust :-) Так что непонимание не удивительно :-)

Да? Ну ладно. Хотя для тех, для кого эта боль, уже давно есть возможность зарабатывать программируя на Java.

Ну или на Haskell, что и делает Джеймс под патронажем Mozilla :-)

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

Это же деньги, бизнес, пойми уже :-)

Не получится ли так что переведённый код будет чуть более чем полностью состоять из unsafe блоков?

а он будет! потому что в GTK надо в документацию смотреть, чтоб видеть когда ownership отдаётся.

и потому что разработчику этого чудо-транслятора придётся вникать долго и мучительно в все внутренности GTK. Там ооооой как весело.

Так ты же не понял что финансирование, о котором поведал Джеймс и является главной мотивацией работы над транслятором C -> Rust

То, что вы так думаете, уже давно понятно. На понятно, зачем вы еще о чем-то стали пытаться говорить.

Это же деньги, бизнес, пойми уже

Упоротый лиспер, который вынужден зарабатывать на жизнь программированием на вызывающим у него боль C++, будет рассказывать о бизнесе... LOR еще торт.

потому что в GTK надо в документацию смотреть, чтоб видеть когда ownership отдаётся.

Нет.

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

Прочитай внимательнее предыдущий пост.

по определенным правилам

Повторяю ещё раз: «определённые правила» всегда отбрасывают корректные сценарии. Проще говоря, напиши двусвязный список на расте без unsafe.

То, что вы так думаете, уже давно понятно. На понятно, зачем вы еще о чем-то стали пытаться говорить.

Конечно, ведь я отдаю себе отчёт в том не оплачиваемый труд просто по определению не стоит и ломанного гроша :-)

Упоротый лиспер, который вынужден зарабатывать на жизнь программированием на вызывающим у него боль C++, будет рассказывать о бизнесе... LOR еще торт.

Хахаха :-) В том то и дело, что мне нет разницы цепепе, це, лисп или ещё что-то :-) Я говорю про мотивацию и про то, что за чью-то боль или труд нужно соразмерно платить :-) Но унылый васька так и не понял ничего :-)

Повторяю ещё раз: «определённые правила» всегда отбрасывают корректные сценарии.

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

Конечно, ведь я отдаю себе отчёт в том не оплачиваемый труд просто по определению не стоит и ломанного гроша

Речь не о том, что вы себе отдаете. Речь о том, есть ли в данной разработке еще какой-то смысл кроме того, что некий чувак будет несколько месяцев получать деньги от Mozilla.

Я говорю про мотивацию

Так определитесь уже, про мотивацию вы вещаете или про бизнес.

Главное верить.

Зато знаком с языками программирования, и не могу понять что хаскель такого может в dsl.

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

struct MyFoo {
   GtkWindow * mainWindow;
   GtkButton * button_in_window;
};

MyFoo * my_foo_new() {
   struct MyFoo * foo = ...;
   foo->mainWindow = gtk_window_new(...);
   foo->button_in_window = gtk_button_new(...);
   gtk_container_add(GTK_CONTAINER(foo->mainWindow), foo->button_in_window);
   return foo;
}

я погляжу как растаманы будут эту ситуацию натягивать на свои «парадигмы». под пивко.

целочисленное переполнение

В дебаге.

и выходы за пределы векторов

Всегда.

почему автор выбрал Rust, а не, скажем, D,

В D же GC. Он ничем не поможет. А в rust уже на этапе компиляции будет исправлена половина ошибок сишки.

Если вы не осилили прочесть FAQ раста на тему: какие гарантии предоставляет раст. То это ваши проблемы.

знатно выпадало с 11-м сигналом.

Это даже не pre-alpha. Ничего удивительно.

На rust после strip 331000 Не такой уж жирный рантайм у rust, что уже очень интересно.

Дык там 300кб - это jemalloc

А наоборот транслятора не изобрели ещё? Или транслировать нечего особо? :)

Иначе это же не такой уж и маленький performance penalty...

Его избегают как могут. Особенно в итераторах. Ну и оптимизатор может помочь.

оно тебя с растом переживёт ещё

Факт.

быстрая разработка
выразительность
С

Мы точно об одном и том же C говорим?

Прочитай внимательнее предыдущий пост.

Прочитал. Ничего интересного не нашёл. Телепатия не помогает. Какое отношение к теореме Гёделя имеет то, что система типов Хиндли-Миллера недостаточно мощна, а в System F вывод типов невозможен?

Повторяю ещё раз: «определённые правила» всегда отбрасывают корректные сценарии

Если можно написать интерпретатор машины Тьюринга, то ничего не отбрасывают. Не путайте формальные системы с практическими потребностями.

Проще говоря, напиши двусвязный список на расте без unsafe.

Чётче надо: напиши двухсвязный список на Rust, без unsafe, не используя сторонних библиотек, используя для связи элементов один из видов указателей (не индексы в массиве), не используя Arena или TypedArena, так, чтобы работала также быстро как и на C. Вот. Сдаюсь.

Вычеркните одно.

Но к теореме Гёделя по-прежнему отношения не имеет.

К слову о рантайме: 64k демосцена на расте: https://www.youtube.com/watch?v=rWwNgVwQG1A

Проще говоря, напиши двусвязный список на расте без unsafe.

Напишите прогу на C без уязвимостей. Вы проиграли.

К слову о рантайме: 64k демосцена на расте: https://www.youtube.com/watch?v=rWwNgVwQG1A

И для сравнения 64k-демосцена на устаревшем язычке, который хипсторы так ненавидят: https://www.youtube.com/watch?v=qRVTI2y0BBg

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

Годно. Но суть в маленьком рантайме раста, а не в том, что он лучше С.

Речь не о том, что вы себе отдаете. Речь о том, есть ли в данной разработке еще какой-то смысл кроме того, что некий чувак будет несколько месяцев получать деньги от Mozilla.

Сначала тебе была Не понятна мотивация автора подобного инструмента. Теперь ты заговорил о смысле :-) Переобулся в воздухе, так сказать :-)

И что тебе до денег некоего чувака? :-) Обидно что SObjectizer не финансируется компанией ранга Mozilla? :-)

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

Ты настолько 404, что тебя даже не видно :-)

Corrode написан на Haskell

это наверное чтоб ни с кем не делить финансирование

На Rust это придется писать с нуля, а для Haskell есть готовая либа.

https://github.com/KyleMayes/clang-rs

Но это же не Rust. Про обертки над Си-интерфейсом libclang см. ссылку выше.

Да и зачем писать _этот_ транслятор на Rust?

Чтоб его писал не один хаскелист just-for-fun, а было сообщество растоманов

Речь шла о технической стороне, а не о социальной. Зачем в компиляторе все танцы с лайфтаймами и трюками по реализации деревьев? Незачем. А с социальной точки зрения... коммюнити Хаскеля больше растовского и компиляторщиков там найти легче. Заинтересует ли Corrode растовское сообщество - большой вопрос.

Зато знаком с языками программирования

Тогда почему глупости спрашиваешь?

не могу понять что хаскель такого может в dsl.

Ну как бы DSL в основном на Haskell-е делают.

Одно большое не нужно...

Rust очень неудобный в плане работы со строками и структурами

Видимо, слово мотивация для вас означает только финансовую мотивацию. Что не удивительно, если человек вынужден зарабатывать на жизнь тем, что вызывает у него боль.

Ну и за меня не беспокойтесь. В отличии от автора этого транслятора у меня нет необходимости во внешних источниках финансирования для развития своего инструмента.

Просвещайтесь.

http://web1.cs.columbia.edu/~junfeng/09fa-e6998/papers/sel4.pdf

Programming in C is not sufficient for implementing a kernel.

Дальше не читал.

Я прикладной программист. Всякие теории меня мало волнуют.

По сравнению с чем?

структурами

Структурами чего?

Technically correct, best kind of correct.

Вручную переписано с Haskell на С, затем доказано соответствие C-части Haskell-части. Технически - да, написано на С.

Какое отношение к теореме Гёделя имеет то, что система типов Хиндли-Миллера недостаточно мощна, а в System F вывод типов невозможен?

Не знаю, это Вы сами сюда приплели зачем-то.

Но к теореме Гёделя по-прежнему отношения не имеет.

Адепты утверждают, что

1) раст позволяет писать настолько же быстрый код, как и C, иначе говоря, он настолько же выразителен

2) он безопасен, благодаря волшебной системе типов

Между типами и доказательствами ещё тов. Карри параллель провёл. Таким образом, эти два утверждения в сумме дают, что механический процесс компиляции раст-кода позволяет доказать непротиворечивость любой теоремы.

Я не утверждаю, что безопасный код нельзя писать. Можно, но он либо будет неинтересен (мой любимый пример про HQ9+), либо придётся вместо механического процесса (коим является тайп-чекинг) использовать свою голову. А тут уж не Rust в фаворитах.

Мы точно об одном и том же C говорим?

Да, но возможно наше понимание «быстрая разработка» и «выразительность» различны.

Уточняю: «быстрая разработка» здесь означает, что для написания программы не нужно формально доказывать её корректность.

«Выразительность» — способность писать программы, «интересные» в том смысле, любой (существующий на данный момент) тайпчекер находит в ней false positive ошибки.

«быстрая разработка» здесь означает, что для написания программы не нужно формально доказывать её корректность.

Время, затраченное на дебаг, не учитывается? Окей...

интересные» в том смысле, любой тайпчекер находит в ней false positive ошибки.

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

раст позволяет писать настолько же быстрый код, как и C, иначе говоря, он настолько же выразителен

Я не являюсь специалистом в академическом программировании. Я обычный пролетарий. Но с каких пор производительность стала синонимом выразительности?

он безопасен, благодаря волшебной системе типов

Если уточнить, что лайфтаймы являются типами - то да. И он не обладает абсолютной безопасностью, о который мечтаете вы. Он обладает вполне определенной безопасностью, которая описана в документации языка.

Видимо, слово мотивация для вас означает только финансовую мотивацию. Что не удивительно, если человек вынужден зарабатывать на жизнь тем, что вызывает у него боль.

Такова реальность, Женя :-) В конечном итоге всё сводится к деньгам :-) И, если ты не знал, то любой стоящий труд вызывает боль, это тоже реальность :-) Нет ни одного реального достижения, которое не далось бы болью или трудом :-)

Ну и за меня не беспокойтесь. В отличии от автора этого транслятора у меня нет необходимости во внешних источниках финансирования для развития своего инструмента.

Я не беспокоюсь, мне всё равно откуда ты кормишься :-)

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

Скорее всего. Обычно под выразительностью понимают способность написать quicksort (который обычно совсем не quick) в одну строчку и всё в том же духе. Каюсь, что я это слово использовал для другого смысла, а именно: способность выражать сложные алгоритмы и структуры (типа двусвязного списка ^___~). Пусть и в много строк кода.

Но с каких пор производительность стала синонимом выразительности?

Не синонимом, а следствием. Я исхожу из real life наблюдения, что хорошо оптимизированный код на C как правило представляет собой удивительный набор хаков. То, что на языке можно выразить все эти хаки, разве нельзя назвать «выразительностью»?

Между типами и доказательствами ещё тов. Карри параллель провёл. Таким образом, эти два утверждения в сумме дают, что механический процесс компиляции раст-кода позволяет доказать непротиворечивость любой теоремы.

Интересный вывод. Только неверный. Для обеспечения безопасности скомпилированного кода, достаточно гарантировать, что каждая компилирующаяся программа представляет собой выводимую теорему в соответствующей формальной системе. Если компилятор отвергнет корректную программу, то это не нарушит безопасности.

Впрочем, если система типов соответствует логике предикатов первого порядка, то согласно теореме Гёделя о полноте, можно сделать компилятор, который скомпилирует все корректные программы и отвергнет все некорректные. Но это неинтересно.