Это история, в которой Хиллел Уэйн пытается ответить на вопрос, почему все больше программистов не используют формальные методы?

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

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

Затем Хиллель написал следующее, говоря о спецификации дизайна (один из многих формальных методов):

Но между фанатами и аутсайдерами существует большое несоответствие. Для фанатов самое большое преимущество состоит в том, что процесс написания дизайна заставляет вас понимать, о чем вы пишете. Когда вам нужно формально выразить то, что делает ваша система, внезапно многие тонкие ошибки становятся до боли очевидными. Это совершенно неубедительно для посторонних.

Это так верно, что меня бесит.

Позвольте мне попытаться рассказать вам историю о том, как я превратился из аутсайдера в инсайдера.

Я изучаю степень магистра права на юридическом факультете Университета Альберты в области вычислительного права. На одном из моих занятий у меня был проект по кодированию Закона о взаимозависимых отношениях взрослых, SA 2002 c A-4.5 [AIRA], на языке программирования ErgoAI.

Этот процесс почти полностью аналогичен идее создания проектной спецификации для части программного обеспечения. Закон - это программа. Кодировка закона - это проектная спецификация, сделанная на более формальном языке.

[NB: это не относится ко всем методам кодирования законов. И большинство инструментов, доступных для этого, либо слишком устрашающи для юристов, либо не имеют необходимых функций. Это одна из причин, по которой я работаю на www.Blawx.com.]

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

Например, чтобы закодировать правило «никаких транспортных средств на траве», компьютеру необходимо понимать, что такое «транспортное средство», что означает «на траве» в данном контексте и что такое «трава». Все эти вещи понимают люди, автоматически читающие версию на естественном языке (при условии, что она хорошо составлена), но компьютер не может понять ни одну из них. Вы должны создать термины, понятные компьютеру, прежде чем вы сможете произносить правила.

Этот процесс принятия того, что неявно, и превращения его в явное не происходит, когда вы пишете сам закон или когда вы читаете его в абстрактном виде. Когда вы смотрите на закон таким образом, вы видите его по-другому.

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

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

Когда я кодировал AIRA, одна из неявных идей, которые я обнаружил, заключалась в том, что есть несколько способов, которыми могут начаться отношения по общему праву, и несколько способов, которыми они могут закончиться. Эти два понятия, исходное событие и завершающее событие, прямо не указаны в законе. Но для того, чтобы компьютер мог ответить на вопросы о том, состоят ли два человека в настоящее время в отношениях, основанных на общем праве, компьютеру нужны явные неявные идеи.

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

А потом это случилось. Я понял, что для соглашения, заключенного при совместном проживании, не было никакого события, но совместное проживание никогда не начинается.

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

Теперь, если вы юрист из Альберты, знаком с AIRA и уже знаете, сообщите мне об этом. Потому что я поспрашивал. И никто из моих коллег не догадывался, что эта лазейка существует, пока я не предложил ее. Я определенно не подозревал, что это было, пока не попытался закодировать Акт.

Почему? Все мы плохие юристы? Мы просто не читаем внимательно? Нет. Это потому, что мы люди, а законы сложны. Это то, чего вы ожидаете, и большинство юристов считают такую ​​лазейку своего рода неизбежным злом (или добром, в зависимости от вашей точки зрения).

Но так ли это необходимо? Если бы люди, написавшие этот закон, использовали эту технику, существовала бы эта лазейка? Я не ожидал. Потому что это было бы совершенно очевидно, хотя раньше было совершенно невидимым.

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

Есть много вещей, которые мы можем сделать с закодированными законами. Мы можем использовать формальные методы, которые позволят нам генерировать случайные сценарии фактов и искать странные юридические результаты. Некоторые люди ищут возможность математически доказать определенные вещи, касающиеся правил высокого риска, таких как смарт-контракты.

Но посмотрите, что говорил Гиллель:

процесс написания дизайна заставляет вас понимать, что вы пишете

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

Не потому, что вы хотите автоматизировать юридическое обоснование. Хотя это также позволит вам это сделать. Но потому что это заставляет лучше понимать, что вы читаете и пишете.

Обучение программированию с помощью таких инструментов заставляет вас научиться думать по-другому. Это формальный метод юридического анализа. И это явно лучше, чем «думать как юрист», которому нас сейчас учат. Я знаю, потому что лучше понимаю законы, когда их использую. Я вижу то, чего не видит никто.

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

Это позор.