Prolog for smart contracts and blockchain technology

[Markus Triska]

Dear all,

a few days ago, millions of Ether were stolen due to an oversight in a
"smart contract", which is a contract expressed as a computer program.

In the course of the discussion, a Microsoft engineer highlighted
several flaws of the underlying language that is currently used to
implement such "smart contracts" (i.e., programs) in Ethereum:

https://news.ycombinator.com/item?id=14810008

Many of these issues could have been avoided in a language like Prolog.
In fact, said Microsoft engineer himself pointed towards Prolog later as
a possibly more sensible alternative to implement smart contracts:

https://news.ycombinator.com/item?id=14809743

There are already some projects that are pioneering the use of Prolog
for blockchain technology, for example:

https://github.com/datavetaren/prologcoin

To quote:

Prolog has also a concept of back-tracking which is similar to
"exception handling" in traditional languages. This amounts to go
back in time and undo things. Again, this is a perfect fit for the
so called reorganization problem that also occurs in blockchains.

Therefore, my question towards Prolog researchers, implementors and
programmers: Are any of you already working on Prolog projects related
to smart contracts and blockchain technology? To me, the language seems
very suitable for such projects, and I have heard of prior projects that
aimed to express law texts in Prolog. If you know more about these
subjects, please respond: I hope that we can work on this together.

Thank you very much!
Markus

--
comp.lang.prolog FAQ: http://www.logic.at/prolog/faq/
The Power of Prolog: https://www.metalevel.at/prolog

[burs...@gmail.com]

Hi,

But Prolog alone is very weak as a language that
allows program verification. You would need to
pair a declarative language such as Prolog, Haskell,
etc.. with a theorem prover.

You can also pair imperative languages Java etc..
with a theorem prover. Theorem provers that can
do that and that can reflect the verified languages,
are HOL/Isabelle, Coq, etc..

So I consider the claims made about Prolog and
e-Coins some crazy marketing hype that might cause
more harm than good. Its just bull shit. You can
make the same errors with or without Prolog

backtracking, and other programming languages also
allow backtracking for example Haskell you can use
some continuation, and in Java you might even use
simple loops. It was just yesterday that I

implemented Xpath (the small subset from the XSLT
prototype) via Java loops (with an fixed array keeping
the choice points):

/**
* <p>Find a first dom element.</p>
*
* @param pos The child number.
* @param e The child dom element.
* @return The found dom element, or null.
*/
private DomElement findFirst(int pos, DomElement e) {
if (!locs.get(pos).checkElement(e))
return null;
if (pos == locs.size() - 1)
return e;
DomNode[] children = e.snapshotChildren();
for (int i = 0; i < children.length; i++) {
DomNode child = children[i];
if (!(child instanceof DomElement))
continue;
e = findFirst(pos + 1, (DomElement) child);
if (e != null) {
LocationHit hit = hits.get(pos);
hit.setChildren(children);
hit.setPos(i);
return e;
}
}
return null;
}

/**
* <p>Find a next dom element.</p>
*
* @return The found dom element, or null.
*/
private DomElement findNext() {
int pos = hits.size() - 1;
while (pos >= 0) {
LocationHit hit = hits.get(pos);
DomNode[] children = hit.getChildren();
for (int i = hit.getPos() + 1; i < children.length; i++) {
DomNode child = children[i];
if (!(child instanceof DomElement))
continue;
DomElement e = findFirst(pos + 1, (DomElement) child);
if (e != null) {
hit.setPos(i);
return e;
}
}
pos--;
}
return null;
}

Unfortunately CLP(*) can never replace a theorem prover.
In a theorem prover you have quantifier rules and semi-
automatic guidance (human interaction to complete a proof),
which so far I don't see many CLP(*) implementations offering.

Their aim is different.

Also to reflect portions of the verified language typically a
higher order logic is used and some calculus of construction,
this is all terrain that would need to find its way into
Prolog, only found in prototypes such as λ-Prolog (*).

So ordinary Prolog has already lost the game.

Bye

(*) One way or the other you would need to implement
some higher order unification.

[j4n bur53]

So initiatives such as:

the science of (deep) specification
https://deepspec.org/main

Might have a bigger impact here.
Maybe forget about the deep.

burs...@gmail.com schrieb:

[burs...@gmail.com]

For example this is a nice idea:

> And whenever we want to spend the coin we just bind ValidatedValue to
> something that proves we own it. Binding this variable will trigger
> the goal to evaluate to true. If it's unable to prove it, then it's
> not true and will not be accepted by the blockchain.

But this is already a mixture of pure Prolog and CLP(*) ideas.
For example in pure Prolog a goal, with an unbound variable
is allowed to succeeds (if there is a proof from the program):

?- q( ... unbound var ... ). /* this might succeed */

Here is an example:

Welcome to SWI-Prolog (threaded, 64 bits, version 7.5.8)
SWI-Prolog comes with ABSOLUTELY NO WARRANTY. This is free software.

?- append([X],L,R).
R = [X|L].

The above proof result says that we can append any X wrapped
into a singleton list to any L and will get [X|L]. This
was proved, and something with unbound variables proved.

The idea to delay goals with unbound variables, comes from
goal suspension and subsequently is also used in CLP(*). But
a non-ground goal can also have a truth value.

For more details see for example J. W. Lloyd logic programming,
to see what happens when a non-ground query/goal is answered via a
resultion theorem proof.

If you suspend because some facts are missing, you also depart
from the world of pure Prolog, because then predicates are
not anymore subject to CWA (closed world assumption).

But CLP(*) doesn't support suspension because of missing facts,
CLP(*) typically looks at variables and not facts. The typically
attribute variable implementation is triggered by variables,

so waiting for facts, is a different thingy, not sure how to
combine the two concepts CLP(*) and non-CWA. But anyway, please
go on and make all kinds of experiments.

I don't say THIS is bad, such experimentation is probably
rather welcome.

Am Sonntag, 23. Juli 2017 10:13:46 UTC+2 schrieb Markus Triska:

[Dhu on Gate]

back in the early '90s I was involved in some projects in the SU and
found that the disconnect in legal systems made for contractual problems
so we used prolog programs to describe contract execution...

Dhu

> subjects, please respond: I hope that we can work on this together.
>
> Thank you very much!
> Markus





--

Je suis Canadien. Ce n'est pas Francais ou Anglaise.
C'est une esp`ece de sauvage: ne obliviscaris, vix ea nostra voco;-)

http://babayaga.neotext.ca/PublicKeys/Duncan_Patton_a_Campbell_pubkey.txt

[Julio Di Egidio]

On Sunday, July 23, 2017 at 10:13:46 AM UTC+2, Markus Triska wrote:
<snip>

> << Prolog has also a concept of back-tracking which is similar to
> "exception handling" in traditional languages. This amounts to go
> back in time and undo things. Again, this is a perfect fit for the
> so called reorganization problem that also occurs in blockchains. >>

Utter nonsense.

Julio