Is the Solidity specification still its compiler?

Question

I'm currently reading some literature about verification of smart contracts. One of the papers I read is Defining the Ethereum Virtual Machine for Interactive Theorem Provers by Hirai (pirapira). In the considerations around solidity (Section 2.1) he states that:

Solidity has a reach syntax but no specification. The only definition of Solidity is the Solidity compiler implementation.

I am wondering if it is still so or something has changed in the meantime.

P.S. I see that the team of kframework has begun to define the semantics of solidity with K Framework

Answer 1

The semantics of Solidity change with every update, and the only canonical definition is the compiler itself. Note that there is a distinction between the intended behavior of the compiler and the actual behavior, which sometimes leads to compiler bugs. Maybe then it is more accurate to say that the (informal) definition of the solidity semantics is in the docs.