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

а Zig разве умеет си компилировать?

19:45пожаловаться #1

gо

goldstein опять in rust_offtopic

Да

19:47пожаловаться #2

кстати зачем придумали запись через черту для этого вывода типов. Как дробь. Как то не очень удобно если честно.

20:27пожаловаться #3

как они это рисуют постоянно не представляю :)

20:28пожаловаться #4

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

20:45пожаловаться #5

Да ладно, я прикалываюсь. Лучше скажи если можно по тому видосу. почему это не то что в Liquid Haskel ?)

20:47пожаловаться #6

Prusti это логика Хоара со всеми соответствующими.

20:48пожаловаться #7

https://ucsd-progsys.github.io/liquidhaskell-blog/2019/10/20/why-types.lhs/

20:48пожаловаться #8

Ну и кроме того, в данный момент prusti неюзабелен даже для leftpad'а.

20:49пожаловаться #9

https://github.com/viperproject/prusti-dev/issues/447

GitHub

[Prusti internal error] generating fold-unfold Viper statements failed · Issue #447 · viperproject/prusti-dev

Prusti reports this error at push_all function: [Prusti internal error] generating fold-unfold Viper statements failed (FailedToObtain(Pred(Local(_old$l22$0: Ref(__TYPARAM__$T$__), Position { line:...

20:49пожаловаться #10

ага. а контракты в С++ это вообще о чём?

20:50пожаловаться #11

Börgar in rust_offtopic

это без пруфов

20:50пожаловаться #12

просто аззерты напихают?

20:50пожаловаться #13

Börgar in rust_offtopic

да

20:50пожаловаться #14

сильно

20:51пожаловаться #15

посмотрю

20:51пожаловаться #16

есть и другие нотации

21:05пожаловаться #17

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

21:05пожаловаться #18

и ещё это красиво выглядит

21:05пожаловаться #19

вообще я теорию типов только из-за этой записи начал изучать, лол