Тут есть не трудность, а стремление избежать человеческого фактора при переводе содержимого из кода на roqc в pdf. +экономия времени
Формальные доказательства точно не про экономию времени) Пиши сразу на человеческом. Если будет ошибка в доказательстве - будет хорошо, если бы узнаешь об этом, ибо это значит что голова не так настроена.
Всё равно доказательства на формальном языке требуют освоения сразу двух навыков:
1. Умения сформулировать доказательство в голове
2. Умение перевести его на язык машины
mr_secret, если внутри ересь, которая не имеет отношения к предмету и задаче, то тогда конечно примет, но сразу неуд/незачёт пропишет и скажет переделывать)
mr_secret,
1. Попробуй прямо спросить препода, будет ли он принимать подобную работу - может он согласиться в принципе взять исходник с доказательством на coq.
2. В чём трудность руками перевести корректное доказательство на человеческий язык?
Тоесть вы не согласны, что если использовать стандартные подходы, то:
1. Разработчик сможет меньшими усилиями поддерживать документацию
2. Клиент сможет с меньшими усилиями интегрироваться
3. Поддержке реже придётся отвечать на глупые вопросы из-за того что кто-то не дочитал про нюансы
4. Высвободившиеся ресурсы можно будет потратить на что-то более полезное (или хотябы приятное)
Или в чём именно я не прав?
В том что если отдавать 200 OK только при успехе, а 4хх/5хх только при ошибках, то в метриках будет корректно посчитан процент ошибочных запросов?
Зачем вам интерактивное доказательство, если вы собираетесь писать статьи в журнал?
Пишите руками - это даже легче будет, так как можно будет человеческим языком описывать то что нужно.
Если нужны формальные доказательства, то зачем вам тогда pdf, если все эти теоремы должны гоняться на исходниках?
Кажется, вы не тот инструмент себе ищете для какой-то иной неописанной в вопросе проблемы.
Опишите, что именно вы хотите достичь и зачем и тогда можно будет найти решение, которое действительно вам поможет.
Владимир, поправка: нужно будет читать больше и не удастся переиспользовать часть кода, который уже написан.
Опять же и вам, как автору - придётся больше писать и уделять больше внимания тому, чтобы документация была полная, актуальная, и непротиворечивая.
Если ваш API является продуктом, за который потребитель платит - такие препятствия могут сделать ваш продукт менее привлекательным по сравнению с альтернативами.
User-Agent подменял (в т.ч. на полностью идентичный нативному).
А этот user agent другим фингерпринтам соответствует?
Если ты парсишь через chrome, а в user agent пишешь что-то от мобильного браузера, то тогда это будет палиться.
