AZ
Т-34 85
то есть, тебя не волнует то, что ты будет продолжать юзать багованный софт. Или не ты, а твои родственники. Или просто другие незнакомые люди
я не буду его юзать)
Size: a a a
2020 March 08
AZ
вот я линуксом не пользуюсь например
G
Так писать просто, доказывать вот уже может быть сложнее.
Но тут мы верем в SMT солверы и помогающую нам параметричность
Но тут мы верем в SMT солверы и помогающую нам параметричность
+ как я уже говорил, можно для тривиальных случаев писать теоремы без доказательств, а нетривиальные тестировать (если скорость разработки важнее безопасности)
AZ
потому что он у меня глючит по кд
Т8
и кто реально такпишет? 2.5 анонимуса?
p
Так писать просто, доказывать вот уже может быть сложнее.
Но тут мы верем в SMT солверы и помогающую нам параметричность
Но тут мы верем в SMT солверы и помогающую нам параметричность
Мы только начали разговор, а я уже ничего не понимаю
А тесты написал хуяк-хуяк и готово
А тесты написал хуяк-хуяк и готово
AZ
Научиться писать теоремы сложнее чем тесты, т-34 прав
ты пробовал протестировать что разворот списка делает что нужно?
p
ты пробовал протестировать что разворот списка делает что нужно?
Сортировку пробовал
p
Двусвязного
DS
Мы только начали разговор, а я уже ничего не понимаю
А тесты написал хуяк-хуяк и готово
А тесты написал хуяк-хуяк и готово
Чтобы на подобных языках писать, знать эти названия не обязательно.
Попробуй туториал по F* на их сайте для понимания как оно работает, очень прикольно там
Попробуй туториал по F* на их сайте для понимания как оно работает, очень прикольно там
AZ
потому что люди кого я видел обычно писали 2 теста
revEmpty = rev [] == []
revNontEmpty = rev [1,2,3] == [3,2,1]
и на этом успокаивались
revEmpty = rev [] == []
revNontEmpty = rev [1,2,3] == [3,2,1]
и на этом успокаивались
G
Сортировку пробовал
я вставлю в твою сортировку printf и тесты пройдут
AZ
но это не тесты а говно
p
Чтобы на подобных языках писать, знать эти названия не обязательно.
Попробуй туториал по F* на их сайте для понимания как оно работает, очень прикольно там
Попробуй туториал по F* на их сайте для понимания как оно работает, очень прикольно там
Посмотрб
G
Т-34 85
и кто реально такпишет? 2.5 анонимуса?
это не так распространено сейчас, как хотелось бы
Т8
Вопрос: а что можно сделать?
можно сделать такой язык, который будет не стоит отталкивающим для основной массы, но при этом отсекающий как можно больше ошибок. Раст перегнул со вторым, как мне кажется
G
Чтобы на подобных языках писать, знать эти названия не обязательно.
Попробуй туториал по F* на их сайте для понимания как оно работает, очень прикольно там
Попробуй туториал по F* на их сайте для понимания как оно работает, очень прикольно там
Ага, F* прикольный
p
но это не тесты а говно
ПочемуБ
G
Посмотрб
задавай вопросы, если возникнут
AI
а я скорее на хабре в последнее время пролистыаю статью до комментов. Интересно
Мне тоже коменты интересны, но я их больше не пишу из-за долбанутой системы кармы