Formal Language / Category Theory


#1

I am afraid that such a powerless man could make a topic on this research page and it can be really harmful for those who are really specially talented because this particular instance of the topic may be getting ordinarily talented, non revolutional and usually very slowly developing.

But from 2014, when Vitalik said about POS and already published white paper, Dr Gavin published yellow paper and Mr Jeffery developed useful go client and user-interface, and so many… , I was eager to learn Haskell, OCaml and Category Theory;

  • minimal OCaml may be developed with reading ‘Types and Programming Languages’
  • It is just entrance of functional programming.
  • SKI combinators are Turing Complete ( I think it can make another kind of VM )
  • I am not clear about the possibility of Axiomatic Semantics with Ethereum State Chain.

There are a lot of things to do, for the purpose of this topic, and just I wanted to try to clarify.
I do not know even it is suitable for this community. There are a lot of other communities. And Blockchain enables them. But I just thought that open discussion might not cause a bad future anywhere.

Ethereum is open low level infrastructure such that I am afraid this topic is really mixing higher level and lower level in a bad manner.


#2

https://github.com/MaiaVictor/ is pursuing some ideas. He’s trying to unify dapp programming and Ethereum contract programming with a single sweep.


#3

Wow, really nice crazy person.
The reduction optimization is the main topic for SKI combinator (or λ-calculus) and I thought the process needs much calculation as finding prime numbers. For that, he refers;

This is one really interesting topic.

And there might be another approach of just building axiomatic semantics on current opcodes.
This could have much reality.


#4

with ewasm we try to use a restricted subset of webassembly to eliminate/limit all non-deterministic behaviour, thus making formal verification easier.

Eyecandy: You currently can write wasm with S-expressions, lispers gather!


#5
  • With shared memory, the result of load operators is nondeterministic

This might be helpful for evm.

  • Discussions about NaN

It seems that we could put it outside discussion of evm language because evm may not have floating numbers, doesn’t it?

Their approach seems to be really along ‘axiomatic semantics’, which determines PRECONDITION and POSTCONDITION of variables and requests programs to terminate.
Really nice approach I think.

And I had confused that
’axiomatic semantics’ and ‘dependent type’ were related each other in some region.
But now it seems that they are completely independent concepts.

This means, if we have the system which has the unique type such as lisp, we can develop ‘axiomatic semantics’ on it, and vice versa.


#6

Axiomatic semantics is the form like this;

PRECONDITION program POSTCONDITION

Ethereum has state which is changing even when we are writing a contract.
So, we have to handle 2 points of state over time.
1st point is an assumption with a set of variables called pre-PRECONDITION which is used when we start writing a contract.
2nd point is real-PRECONDITION which with check-precondition-function we verify that the deployed contract with real-PRECONDITION has the same effect with that with the pre-PRECONDITION. (If check-precondition-function returned false, the contract is designed to refund suitably and then self-destruct. )

so it is like;

pre-PRECONDITION real-PRECONDITION contract POSTCONDITION

and ethereum real-PRECONDITION that I assume is not stable as it were seen in the incident of library bugs.
( It might be false to say it is PRECONDITION but the Genesis Block be. )
In ethereum PRECONDITION is really changing with mining blocks.

Then we should set the definition a bit more formally.
evm-PRECONDITION consists of 3 components, PRECONTRACTS, pre-PRECONDITION, and real-PRECONDITION. And we also have ordinary PRECONDITION.
A (*)-PRECONDITION is a small set of variables of evm state trie which is required for a contract.
Each contract made by the formal language has a ‘checkPrecondition’ function and every time the contract is called it is designed to return error and refund all back to suitable accounts if real-PRECONDITION is changed.
Without PRECONTRACT, the ‘contract’ part can have the side effect such as calling another contract. Such side-effects all must be situated in evm-PRECONDITION,so I added PRECONTRACTS as a part of evm-PRECONDITION.

In this way, just I think even #EIP156 might not be needed if we have this kind of formal language which will take the role at a higher level. (I never say that lower level safety is not a must.)

PRECONTRACTS pre-PRECONDITION real-PRECONDITION PRECONDITION contract POSTCONDITION

PRECONTRACTS might be designed to exclude infinite loops of contract call.
( or include in some ordinary way like described in #EIP771 )


#7

For the introduction of Aximatic Semantics,
I found Hoare’s paper, maybe it is too famous and seems very nice.

http://sunnyday.mit.edu/16.355/Hoare-CACM-69.pdf


#8

I am afraid I would suggest This should be in the;

#ReadingList


#9

This is the standard textbook for programming language semantics (operational, axiomatic, denotational) https://mitpress.mit.edu/books/formal-semantics-programming-languages


#10

I have just found Type Theory Tips :

Also I would like to put the link of Spivak’s
Temporal Type Theory
which handles ‘time’ in a beautiful way.


#11

In that paper, time is real numbers. What happens when we replace reals with a partial order showing, say, “for this block’s validity, that block’s validity is necessary”?


#12

Ah you mentioning a partial order which is not total.
Ah, I did not see that. It’s a good point!


#13

Your question sounded like ‘Is there a polymorphism from Tree A to List A which will do a breadth first search (which is determined by timestamps), where A denotes for a total ordered number ?’

And I am not sure but there might be a kind of manager who is selected based on RANDAO, so locally ( I mean in some small time,) the POS sharding system can be regarded as a centralized system.

This might be wrong.


#14

#15

NATURAL ROUGH SKETCH

contract guaranteed programming language

A formal contract must not be a game of the language by which it is written.
So, formal language on evm MUST have an abstract interface which define The Formal Language, i.e. the behavior, and in case it did an unexpected behavior which happens outside the formal language, i.e. lower level bug, it allows to be double-checked.

In this sense, " CODE is LAW " would be achieved in a higher (formal) programming language which is human readable and highly structured more than machine codes.

how to do that ?

Simply every time when ‘ether’ of the contract moves, the original source code written by formal language is checked. The checking process will consume much more gas than that without guarantee. Formal way will cost literally.