| |||
|
|
я представляю это примерно так: https://en.wikipedia.org/wiki/L4_microk https://en.wikipedia.org/wiki/CompCert https://en.wikipedia.org/wiki/Formal_ve ровно та деятельность, которую Воеводский хотел привинтить к математике. есть проблема в том, как сформулировать "невзламываемость". это должен быть, с одной стороны, формальный критерий, который у программы хотя бы теоретически (с любой выч. сложностью) можно проверить, а с другой - отражающий реальную невозможность навредить пользователю при определенных предположениях (понятно, что не при любых: терморектальный криптоанализ, это вот все). думаю, что это вполне реалистично, но, конечно а) над этим надо работать б) это требует гораздо больших трудозатрат в) это не имеет никакого отношения к телеграму Добавить комментарий: |
||||