Hacker News new | ask | show | jobs
by jabl 435 days ago
I'm not familiar at all with the Ferrocene specification, but in general I do wonder if the ISO C/C++/Fortran (singling these out as I'm somewhat familiar with them, not saying there aren't other languages with similar spec processes) process of a prose spec is really the best way to go in this day and age? Those languages certainly have their historical reasons for the specs being the way they are, but I'm not convinced it's the only right way of doing a spec if starting from scratch today.

Say, what about something like a formal machine-parsable spec and/or a testsuite that describes the way the language should behave, rather than a prose description that then each compiler writer interprets to the best of their ability?
3 comments
pklausler 435 days ago
A language standard without a reference implementation or blessed test suite can be a real problem due to ambiguity, contradiction, and omissions. When there are existing implementations of a language that are expected to keep up with an evolving standard that doesn't have these things, you can end up with a messy situation like Fortran has, in which the portability of code across compilers becomes a pragmatic job that's not related much to standard conformance.
link
aw1621107 435 days ago
Wasm sounds right up your alley! From my understanding the Wasm spec is formally specified and they just adopted tooling to generate prose/mechanically-checkable proofs/etc. from the formal spec [0].

[0]: https://webassembly.org/news/2025-03-27-spectec/

link
uecker 435 days ago
You can not really write a formal spec without having prose first. It would be nice to have a formal spec for C, and C is one of the languages where this is feasible (and also partially done by various people).
link
aw1621107 435 days ago
> You can not really write a formal spec without having prose first.

The WebAssembly folks might have done that? From the Wasm SpecTec blog post I linked in a sister comment (emphasis in original):

> In fact, the formal version [of the Wasm spec] was written long before the prose, which was then created by manually transliterating the formal rules into natural language (for some definition of “natural”).

To be fair, I'm sure there was a lot of non-formal discussion in the process of creating the formal spec but I'm not sure whether that counts as "prose" in this context.

link
uecker 434 days ago
It is also clear that you can write a formal spec down before writing down prose, if your language is simple and low-level enough.
link