ΑZ
@hirrolot как тебе мысль написать на идрисе квиксорт и доказать что он рабоатет правильно?)
Size: a a a
2020 September 01
AD
вот царь говорит - разделение на бд и апликейшен сервер - это разделение для макак. и ты просто впринципе не можешь с ним спорить потому что какой к этому антитезис? ну тоесть почему так сделали? потому что ниасилили сложноть, потому что "показалось" что разделять - лучше
И он не одинок - знаю я ещё одного очень популярного ютубера, который на чистом коде программирует.
SP
тарас не против бд, он против ооп и фреймворков
H
@hirrolot как тебе мысль написать на идрисе квиксорт и доказать что он рабоатет правильно?)
может когда-то попробуюъ, а конкретно сейчас мне не интересно с идрисом возиться
ΑZ
может когда-то попробуюъ, а конкретно сейчас мне не интересно с идрисом возиться
ну можно на аренде, не принципиально
ΑZ
а то я щас понял что квиксорт никогда не писал
ΑZ
а когда решил написать понял что не знаю как проверить что он правильный
ΑZ
не тесты же писать ей богу
AD
тарас не против бд, он против ооп и фреймворков
Тарас просто ещё не познал того дзена, когда кидаешься какахами и обзываешь макаками одновременно
H
ну можно на аренде, не принципиально
я щас свой CoC пишу, может на нём докажу потом
H
зато у меня есть квик сорт на макросах
H
хм а через индукцию не получается доказать что ли?
H
ладно, интересно стало уже))
AD
Типа для любого n a[n] > a[n+1]
H
сегодня попробую
ΑZ
ΑZ
Нижник через решётки какие то делал
ΑZ
Вроде
p
@Psilon какие свойства ты хочешь верифицировать?