Hacker News Reader

Out of curiosity, how many languages would meet those criteria? Only one I can think of off the top of my head is CompCert's C dialect. Are there others?

View on HN

It's a spectrum - some languages do it a lot better than others. Not having anything more than a conversational English description of what it does is definitely the lower end of the spectrum. I'm sure very few are doing it perfectly, but for example Java has a formal semantics.

> but for example Java has a formal semantics.

I don't think that's really true. The Java language specification is entirely prose. The book you linked to was written by "outsider" authors and published in 1999 (!).

That was just one example of many - there's a whole cottage industry of writing formal semantics for Java.

https://fsl.cs.illinois.edu/publications/bogdanas-rosu-2015-...

None of them are official, and I bet they make major simplifications (the one you just linked to is for Java 1.4). I doubt actual language/tooling implementors benefit much from them.

Standard ML certainly has clear specifications and proofs of soundness of the type system.

Reply on news.ycombinator.com