These are chat archives for dev-ua/rust

7th
Oct 2016
Oleksandr Nikitin
@wizzard0
Oct 07 2016 16:41
панове, а хтось бачив пейпери по теорії, що лежить під borrow checking'ом?
Michael Pankov
@mkpankov
Oct 07 2016 16:54
@wizzard0 http://plv.mpi-sws.org/rustbelt/ внизу Related Papers
Oleksandr Nikitin
@wizzard0
Oct 07 2016 16:55
Ага, спасибо
Unfortunately, none of Rust's safety claims have been formally investigated, and it is not at all clear that they hold.
Вот я пришел к такому же где-то выводу и стало как-то неуютно)))
Michael Pankov
@mkpankov
Oct 07 2016 16:56
ещё можно почитать про ATS и Cyclone (языки такие были)
думаю про них-то должны быть статьи
Oleksandr Nikitin
@wizzard0
Oct 07 2016 16:57
Мб, мб
Просто все с одной стороны ссылаются на Wadler et al. про LTL, но как-то никакой очевидной связи не видно...
Michael Pankov
@mkpankov
Oct 07 2016 17:08
@wizzard0 хз, но тут вот в вики в applications написано "Expressing important properties in formal verification" и там про safety и liveness
а это как раз про раст)
Oleksandr Nikitin
@wizzard0
Oct 07 2016 17:08
ссылку, ссылку!
или wikipedia/rust?
Oleksandr Nikitin
@wizzard0
Oct 07 2016 17:12
Дадада, дадада, но по ощущениям оно как-то мало общего имеет с имплементацией в Rust, даже майкрософтовский пейпер Uniqueness, Immutability and Safe Parallelism ближе
Обосновать пока не могу, впрочем
Ruslan Shevchenko
@rssh
Oct 07 2016 18:07

@online{Patine,
 author = {Eric Reed},
 title = {Patina: A Formalization of the Rust Programming Language.},
 url = { ftp://ftp.cs.washington.edu/tr/2015/03/UW-CSE-15-03-02.pdf},
 datr = {2015-02}
}
Oleksandr Nikitin
@wizzard0
Oct 07 2016 20:25
@rssh спасибо