Is there a programming language for lawyers?

Question

Programming

Gentlemen, I have a theoretical question.
We are all educated people here and we know that there are natural and formal languages.
The question is this:
If legislation and jurisprudence require accuracy in wording and work with such concepts as logic and conclusions and evidence, then why has not a single programming language been created so far that would have the ability to convert program code into the text of contracts, laws and other documents ?
Why do all lawyers still use natural language instead of formal language in their work?
If there are such languages, it would be very interesting to give examples in the comments.
If not, what fundamental problems prevent the creation of such a language? If this is not possible, then why?
The possibilities are simply amazing: automatic construction of proofs, automatic generation of conclusions, verification of statements for consistency, and so on.
I would like to hear the community's opinion on this topic.

Answer 1

Look in the direction of deontic logic, maybe something has already been invented there.

Answer 2

Have you ever been to court?) I was, there is no smell of logic there!
But seriously, jurisprudence is still very far from any automation. It's all too clumsy. Besides, where have you seen humanists who would be friends with programs more complicated than Word?)

Answer 3

Even children know this language.
Execution cannot be pardoned .

Answer 4

Do you know .. But I even write little by little abstracts on this subject in a notebook. Years 5-7 slowly.
In my opinion, yes it is possible. For most cases anyway.
The problem is that no one needs it. More precisely, it is undesirable for those who make such decisions.
Well, in fact - will the deputies want to replace themselves with a program, even if it will be objectively better and cheaper to work? So the legislators will not allow it.
What they wrote to you above "have you ever been to court at least once" was rude, but in fact it is true. The question is not that a law can be described by a logical equation. The issue is that the Court is ruled not by the Law, but by the application of the law.
Have you heard the story (I don’t know how true) about automatic cameras that some officials were unhappy with, because they send fines, despite the fact that “I am the law”? This is part of the problem.

Answer 5

I think. that the problem here is the immensity of the subject base. That is, lawyers operate with a large number of high-level (i.e., each person has some idea of ​​​​what a given word means in context, but there is no strict definition) natural language concepts ("person", "action", "deliberately ", etc), sometimes quite bizarrely interacting, which makes strict formalization difficult.
On the other hand, it would be very interesting to look at attempts to get closer to solving this problem. Laws that operate in accordance with formal logic - it's cool!

Answer 6

Partly it is.
Those. there is an expert system in their heads - at least in criminal cases.
Citizen A tried to steal the property of citizen B.
switch(steal)
case:
secretly;
crime=THEFT;
case:
with violence;
crime = Plunder;
case:
with a weapon;
crime = ROBBING;
TERM=f(crime)
But... in practice it is more and more difficult
. Is citizen A identical to the citizen who committed the crime?
Did the property of citizen B really belong to him?
And so on... If the investigation did a good job and everything is clear to everyone, then the case is considered in a special simplified procedure and that's it.

Answer 7

In general, the question is interesting.
We have already created sites where they give extracts from all sorts of licenses. For. so to speak, the inhabitants.
90% of the text in each jur. document - water, which is required by law.
Indeed, for typical documents, you can easily write a generator that will stamp thousands of them.

Answer 8

Such a language cannot exist. The language of lawyers is not the language of mathematics or physics. Lawyers have a problem of interpretation of norms. They write something in a law or an agreement, and then they argue about what it means. And everyone understands as he wants. In short, lawyers use simple human language, it’s just that sometimes there are various legal terms in it, but in general this language has the same drawbacks as ordinary human language - what is written can always be “turned upside down” and understood this way and that, and how you like it. Therefore, in fact, there are still lawyers.

Answer 9

Perhaps IBM Watson will do something similar after some time. In jurisprudence, there are a lot of similar cases where the law is applied in the same way with minor clarifications - for example, loan debts.
Judges such automation could help because. they are not always up to date with the latest jurisprudence, and overturning a judge's decision at a higher level damages reputation.
Here is an example of how IBM Watson answers questions. https://vimeo.com/76324047

Answer 10

The natural language of lawyers, with all its formalization, is a double-edged weapon of defense and attack, the flexibility of the language allows a lot.
As for logic, any lawyer, even at the beginning of training, immediately has a lot of situations that are not at all easy to solve binary.

Answer 11

I googled this thread because I found it extremely difficult to defeat GrK. Repetitive words and cumbersome constructions, necessary due to the traditions and norms of writing such documents, make the text simply overloaded and inconvenient to read.
I had an idea to rewrite the GrK, purely for myself, in order to keep the meaning, but reduce the volume through the use of mathematical, incl. logical, operators\symbols, and also, possibly, some constructions from programming.
My goal is not to automate legal proceedings, but to squeeze out all the water and make the text readable for people who did not study to be "swimmers" in law schools and are already drowning on the fifth page of the code.
Perhaps my approach and notation will be universal for any codex.
If someone wants to help me, I will be extremely happy. I am not a programmer or a mathematician by education at all, and therefore my system cannot, by definition, claim to be harmonious.