ΑZ
он ещё под линукс умеет запускаться
Size: a a a
2020 August 24
CD
Да, потому что с верификацией ошибок не будет, потому что все нужные свойства доказаны, а что не доказал то не верифицировано следовательно проблема не в верификации
Да да да, интересно, как осуществляются перекодировки в Idris? :)
p
Да да да, интересно, как осуществляются перекодировки в Idris? :)
?
CD
Тащим 3МБ таблиц кодировок или используем системную функцию WideCharToMultiByte в которой баг, найденный тестами?
CD
На вин?
p
Тащим 3МБ таблиц кодировок или используем системную функцию WideCharToMultiByte в которой баг, найденный тестами?
Какое это отношение имеет к разговору?
CD
Какое это отношение имеет к разговору?
Простое - твоя формально верифицированная программа не работает, если завязана на перекодировку строк
p
Простое - твоя формально верифицированная программа не работает, если завязана на перекодировку строк
Чё ты так решил?
CD
Чё ты так решил?
Тащим 3МБ таблиц кодировок или используем системную функцию WideCharToMultiByte в которой баг, найденный тестами?
p
Тащим 3МБ таблиц кодировок или используем системную функцию WideCharToMultiByte в которой баг, найденный тестами?
Какое это отношение имеет а разговору?
CD
Какой стул?
CD
Какое это отношение имеет а разговору?
Потому что альтернатив нет
CD
Либо ты используешь функцию, не соответствующую спецификации, либо пишешь свою, а она требует мегабайты данных
CD
Покажешь, на каком стуле сидит Idris?
p
Либо ты используешь функцию, не соответствующую спецификации, либо пишешь свою, а она требует мегабайты данных
И? Какое это отношение имеет к моему утверждению?
p
Ты его только подтверждаешь
p
Не на ту сторону воюешь
p
Либо ты используешь функцию, не соответствующую спецификации, либо пишешь свою, а она требует мегабайты данных
а что не доказал то не верифицировано следовательно проблема не в верификации
CD
а что не доказал то не верифицировано следовательно проблема не в верификации
то есть ты говоришь, что верификация как надо решает все проблемы, при том, что она никогда не работает как надо? Это, безусловно, верное утверждение
CD
следствие из нулевого предиката истинно, да