Formal Language / Category Theory


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 is pursuing some ideas. He’s trying to unify dapp programming and Ethereum contract programming with a single sweep.


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.


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!

  • 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.


Axiomatic semantics is the form like this;


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;


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 might be designed to exclude infinite loops of contract call.
( or include in some ordinary way like described in #EIP771 )


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


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



This is the standard textbook for programming language semantics (operational, axiomatic, denotational)