Re: a new language, designed for safety !

["G.B." <rm-dash-bau-haus@dash.futureapps.de>]

On 18.06.14 14:30, Dmitry A. Kazakov wrote:
> On Wed, 18 Jun 2014 11:34:01 +0200, G.B. wrote:
>
>> (Pardon? A contract is a manifest piece from the equivalence
>> class of paper, signed by two parties.
>
> And that does not defines the parties it only constrains them, which was
> the point.

In fact, you declared "contract" to be a

"framework of constraints imposed on the implementations"

which a contract between two legal parties is not.
If things required entail things constrained, then making
it sound as if this was an equality, or even the other way
around is invalid.

There is then nothing that warrants mentioning Hilbert.
Maybe if the two parties have agreed to stop programming
entirely in view of of Hilbert's program.

>>> 2. You cannot have exhaustive contracts.
>>
>> Writing contracts is not a just formal logic, it is about
>> programmers *behaving* responsibly when programming:
>
> Irrelevant.

Essential because behavior of parties is the subject of court rulings.
If it is found that for whatever reason the contract was violated
by programmer X, then programmer X can be held responsible. This
is true even in case some technical detail seems to contradict at
the source level. ("It is found" outweighs formal logic.)

> If you are contracted to smoke one block a day, that might be irresponsible
> on your side, but a contract is a contract.

If I sign a contract with you about doing X, and then I
don't do X, then you can hold me responsible. Whether or
not I actually didn't do X is the matter that a compiler
cannot always decide, but courts will. Whether or not
some Y finds doing X morally irresponsible WRT Y's frame
of reference is indeed irrelevant if Y is not the court.