Телеграмм чат группы rust_offtopic страница 10898

parrot.ru

Рейтинг популярных групп и каналов

В рейтинге участвует:

групп:

каналов:

Виртуальный сервер на SSD - недорого!

Аренда выделенных и виртуальных серверов (VDS/VPS), хостинг, аренда IP-адресов, администрирование, круглосуточная поддержка

qwarta.ru подробнее

Резервное копирование с проверкой на вирусы!!!

Удобный сервис создания резервных копий на любой сервер сети интернет. Отслеживайте изменения, проверяйте на вирусы. Надежно защитите свой бизнес!

go.backupland.com

Выбираете сервер? Любая конфигурация на заказ!

Аренда физических серверов любых конфигураций под любые запросы - 1С бухгалтерия, игровые сервера, нагруженные проекты, интернет-магазины!

qwarta.ru подробнее

Size: a a a

rust_offtopic

371 membersпожаловаться на группу

2020 April 14

P

Pavel in rust_offtopic

Есть всякие Coq и идрисы, в которых твой код реально теорема, которую компилер реально доказывает, что прога валидная)

ну, тут точно так же, unsafe-блок — аксиома, сейф-блок — теорема, корректность которой проверяется по правилам определёнными реализацией компилятора.

источник

02:26пожаловаться #1

ML

Mike Lubinets in rust_offtopic

У меня гугл нашел что-то не то, типо это какая-то ткань.

Но мне банально лень(

https://github.com/rust-lang/chalk

rust-lang/chalk

A PROLOG-ish interpreter written in Rust, intended eventually for use in the compiler - rust-lang/chalk

источник

02:26пожаловаться #2

B

Bogdan in rust_offtopic

ну, тут точно так же, unsafe-блок — аксиома, сейф-блок — теорема, корректность которой проверяется по правилам определёнными реализацией компилятора.

Только сейфти проверяется

источник

02:26пожаловаться #3

P

Pavel in rust_offtopic

как бы философский вопрос вывода по логике тут не решает ничего

источник

02:26пожаловаться #4

B

Bogdan in rust_offtopic

https://github.com/rust-lang/chalk

rust-lang/chalk

A PROLOG-ish interpreter written in Rust, intended eventually for use in the compiler - rust-lang/chalk

Прикольно, да както давно натыкался, но забил

источник

02:27пожаловаться #5

B

Bogdan in rust_offtopic

А пролог я немного знаю, лол

источник

02:27пожаловаться #6

ML

Mike Lubinets in rust_offtopic

Прикольно, да както давно натыкался, но забил

Если осилишь блогпосты, можешь записать это ачивкой

источник

02:28пожаловаться #7

B

Bogdan in rust_offtopic

Если осилишь блогпосты, можешь записать это ачивкой

😂😂👍

источник

02:28пожаловаться #8

P

Pavel in rust_offtopic

Только сейфти проверяется

"сейфти проверяется" — "проверяется корректность вывода сложных конструкций из фундаментальных в рамках семантики языка"

источник

02:29пожаловаться #9

AZ

Alex Zhukovsky in rust_offtopic

Roman Proskuryakov

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

начал читать с конца, охренел))) Думал тебя подменили.

Потом проскроллил к началу дискуссии

источник

02:29пожаловаться #10

RP

Roman Proskuryakov in rust_offtopic

)))

источник

02:30пожаловаться #11

P

Pavel in rust_offtopic

Roman Proskuryakov

Ральф для λRust доказал

> Theorem 7.1 (Fundamental theorem of logical relations).For any inference rule of the type system, when we replace all⊢by|=, the resulting Iris theorem holds.

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

не надо, иначе получится, что фундаментальные ошибки в геометрии перенесутся на раст

источник

02:31пожаловаться #12

B

Bogdan in rust_offtopic

аааа, вот оно с чего началось.

Я в это время сношался с миграциями в дотнет коре и прокленал весь мир)

источник

02:31пожаловаться #13

P

Pavel in rust_offtopic

оно нам надо?

источник

02:32пожаловаться #14

RP

Roman Proskuryakov in rust_offtopic

не надо, иначе получится, что фундаментальные ошибки в геометрии перенесутся на раст

ты привел прикольную аналогию, но надо еще доказать, что твоя аналогия корректна.

источник

02:32пожаловаться #15

RP

Roman Proskuryakov in rust_offtopic

начал читать с конца, охренел))) Думал тебя подменили.

Потом проскроллил к началу дискуссии

может ты мне поможешь?)

источник

02:32пожаловаться #16

ML

Mike Lubinets in rust_offtopic

Stanislav Popov

кстати тут такой вопрос назрел - компилятор раста может как то понять что функция чистая и выкинуть её если значение не используется?

да, но это не раст, а ллвм

источник

02:35пожаловаться #17

P

Pavel in rust_offtopic

Roman Proskuryakov

ты привел прикольную аналогию, но надо еще доказать, что твоя аналогия корректна.

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

источник

02:35пожаловаться #18

P

Pavel in rust_offtopic

если unsafe sound и правила языка sound, то и программа sound. доказывать надо только правила языка и ансейф

источник

02:36пожаловаться #19

P

Pavel in rust_offtopic

короче, надо идти гёделя копать по этому вопросу, у него должно что-то быть

источник

02:37пожаловаться #20