сейчас наткнулся на подобную штуку, и немного генерализирую.
при написании веб-сервера на coq обнаружим, что рекурсивная функция, читающая http-заголовки, внезапно потребует доказательства завершимости. По идее, оно должно включить в себя конечность числа символов в прочитанных заголовках, либо конечность как числа заголовков, так и длины каждого из них.
здравые ограничения. Не будете же засасывать в память всё, чем кормят по сети. Да даже если читать только избранные заголовки — остальные надо пропускать, а это — затраты по трафику, тогда как очевидно, что нормальные клиенты слишком много заголовков слать не будут, а всякие злодеи — наоборот, будут.
в обычных условиях необходимость подобных ограничений либо приходит с опытом и поваленными серверами, либо предусматривается заранее в логике сервера. Тут же это соображение безопасности следует напрямую из требования "примитивной рекурсии / хорошо-обоснованной рекурсии" (primitive recursion / well-founded recursion), либо из продуктивности корекурсии (ну это смотря как кодить).

#osgisi

add comment recommend bookmark subscribe