August 8th, 2010

Реформа милиции и theorem provers

Как известно, реформа милиции проходит в очень необычном, инновационном даже (нановаторском?) режиме. Текст закона обсуждается на сайте zakonoproekt2010.ru, и на данный момент собрал несколько сотен комментариев.

И вот что подумалось — посмотрите-ка на комментарии! Это же типичная фаза формализации задачи — уточнения, устранения неоднозначностей, противоречий. В этом громадный шаг в сторону законов, определённых полностью формально и доступных для машинной верификации. В пределе законы должны описываться в какой-то особой законотации, верифицируемой сразу, без промежуточных моделей.

Идея формальных верификаций законов древняя, и, похоже, недостижимая, но я не на этом делаю акцент сейчас. Суть в том, как чётко начинает нести корректностью и непротиворечивостью от закона, до которого допустили публику. Он не станет от этого корректен, но вектор изменений очевиден.

Во-первых, важно, что процесс настолько продвигает закон в сторону автоматической верификации. Конечно, даже до публичного обсуждения логично было бы предположить, что заинтересованные лица начнут его расширять и как-то изменять. Но чтобы вектор был преимущественно и подавляюще в направлении «уточнять» и «формализировать» — это априори ниоткуда не следовало. Nice to see.

Во-вторых, если столько дерьма извлекается из запланированного публичного популистского законопроекта на этапе запланированной публичной движухи вокруг него, то несложно представить, что творится в порождаемых ежедневно остальных законах, вступающих в силу без подобного публичного обсуждения.

В-третьих, если так делать с каждым законопроектом, то законотворческая активность встанет колом.