b
ты понимаешь что граф может не помещаться в памяти? там настоящие челленжи
Size: a a a
2021 March 10
b
почему вам говорят что раст это игрушка, да потому что вы говорите об игрушечных проблемах) арены-хуены, в С++ это давно решенная и забытая база, настоящие инженерные проблемы несут другой характер
А
почему вам говорят что раст это игрушка, да потому что вы говорите об игрушечных проблемах) арены-хуены, в С++ это давно решенная и забытая база, настоящие инженерные проблемы несут другой характер
отлично
s
Люди хотят, чтобы безопасность памяти можно было проверить механически. Но проблема в том, что в расте есть только примитивные инструменты для этого.
s
Вроде борроу-чекера.
s
Как следствие, не прекращаются попытки натянуть сову на этот борроу-чекер.
А
Люди хотят, чтобы безопасность памяти можно было проверить механически. Но проблема в том, что в расте есть только примитивные инструменты для этого.
а непримитивные где?
s
а непримитивные где?
Ну, например, sel4 использует C + теоремы на Isabelle.
r
В пруфах, конечно.
А
и сова на эти пруфы без проблем натягивается?
AN
red75prime
В пруфах, конечно.
слушай а твой свг оптимизатор конфигурируется или нет? если я хочу например оставить айдишники с определенным префиксом?
r
слушай а твой свг оптимизатор конфигурируется или нет? если я хочу например оставить айдишники с определенным префиксом?
Я не поддерживаю никакие opensource проекты.
s
и сова на эти пруфы без проблем натягивается?
На пруфы и не такое натягивается. Только их писать нужно.
AN
red75prime
Я не поддерживаю никакие opensource проекты.
😳 был уверен что то твой проект. перепутал прости
ЕС
Люди хотят, чтобы безопасность памяти можно было проверить механически. Но проблема в том, что в расте есть только примитивные инструменты для этого.
В расте их нет
AK
работает потому что низкий уровень у всех будет примерно одинаковым
В unsafe Rust, помимо того за чем тебе приходится следить в сишке, ещё нужно не налажать с:
1) Алиасингом(алиасить Мут ссылку и птр нельзя, а Мут ссылки могут создаваться неявно, например: *ptr += 1).
2) Вариантностью лайфтаймов
3) Дропчеком
4) Поведением при панике
Мб, что-то забыл. 100 лет Ансейф не писал.
1) Алиасингом(алиасить Мут ссылку и птр нельзя, а Мут ссылки могут создаваться неявно, например: *ptr += 1).
2) Вариантностью лайфтаймов
3) Дропчеком
4) Поведением при панике
Мб, что-то забыл. 100 лет Ансейф не писал.
b
Ну, например, sel4 использует C + теоремы на Isabelle.
а что кстати sel4, я помню смотрел лекцию с какой–то конференции в этом году. чувак говорит они 90% формально покрыли, вопрос а кому это надо, откуда деньги?
MM
Кто-нибудь знает годный чат по си типо растового?
b
Кто-нибудь знает годный чат по си типо растового?
“прорыв запарты” есть такой чат, потрясающий. можешь не благодарить
А
а что кстати sel4, я помню смотрел лекцию с какой–то конференции в этом году. чувак говорит они 90% формально покрыли, вопрос а кому это надо, откуда деньги?
надо запарте, деньги из-под парты достали