News for hackers. Stuff that matters.
Re:Pyjion – A Python JIT Compiler by aw1621107 on Tuesday November 09, 2021 @02:23PM (#29166200)
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?
Re:Pyjion – A Python JIT Compiler by chrisseaton on Tuesday November 09, 2021 @02:29PM (#29166268)
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.
Re:Pyjion – A Python JIT Compiler by fcurts on Tuesday November 09, 2021 @05:16PM (#29168249)
> 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 (!).

Re:Pyjion – A Python JIT Compiler by chrisseaton on Tuesday November 09, 2021 @05:22PM (#29168315)
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-...

Re:Pyjion – A Python JIT Compiler by fcurts on Tuesday November 09, 2021 @05:29PM (#29168392)
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.
Re:Pyjion – A Python JIT Compiler by c-cube on Wednesday November 10, 2021 @09:29AM (#29174964)
Standard ML certainly has clear specifications and proofs of soundness of the type system.