П
У меня хотяб "лучше" не было
Пока приоритет не умереть с голоду :D ( :( )
Я обычно пет-проектами занимаюсь по ночам, но сессия+работа так сейчас ябут, что спать таки хочется.
Size: a a a
2021 May 29
G
gо
Срочно все cargo install!
G
Там реально хороших альтернатив таки немного, из того что я пробовал. зашёл fd, намного быстрее find, это да.
H
жалко нельзя поставить диз
gо
У меня:
cat -> bat
grep -> ripgrep
find -> fd
make -> иногда just
* -> tokei
на одном из ноутов
ls -> exa
cat -> bat
grep -> ripgrep
find -> fd
make -> иногда just
* -> tokei
на одном из ноутов
ls -> exa
AN
exa, bat норм ещё
gо
Какой-то фрик пробовал coreutils -> uutils
gо
Вроде как, у него даже получилась относительно рабочая инсталляция Debian
p
Я уже озвучивал. Делаем вместо завтипов пруфы. Что-то типо такого:
{- declare the function that expected that first argument applies the rule x > 15 -}
foo: (x: Int) -> Int where x > 15
{- declare proof that if f x y and f y z then f x z. Proof is a special type that creates new proof in the scope of proofs -}
Transitive: (x: a) -> (y: a) -> (z: a) -> (f: a -> a -> bool) -> Proof (f x z) where f x y && f y z
{- there are no way to proof this by the compiler. Programmer must proof this by himself. If function does not satisfied the theorem, program may have undefined behaviour. -}
proof (>) is Transitive
bar: IO ()
bar = do
x <- readLine
{- check that rule x > 20 applies. Into first branch of if clause will be put proof x > 20 -}
if x > 20 then do
{- compiler cannot proof that if x > 20 then x > 15, but we can do this by applying transitive rule. We already checks that x > 20, compiler can check that 20 > 15 by evaluating this expression, so we can apply transitive rule and put proof that x > 15 into the scope. -}
apply Transitive x 20 15 (>)
{- compiler checks that in the scope available proof that x > 15 -}
foo xgо
А в чём смысл, если всё сводится к, типа, «unsafe impl Transitive for Gt»?
p
В том что ты получаешь всю силу тайплевел пруфов без необходимости коренным образом менять свой обычный стиль программирования и без необходимости пруфать машине каждое действие, что очень трудоемко
p
Как избавить от UB я пока не придумал
H
просто trust_me() что ли?
p
Да
p
H
какая революционная идея
p
Гениальность в простоте
gо
Но это фигня же.