I would be nice to have a document we can rely on and refer to, in case of subtle breakages and bugs. Alternative implementations could also be a possibility down the line. Having a formal spec would also help with code verification, i.e. you basically can't do it unless the language is specified.
#1 is the same as the current situation. With #2, you might get a bit closer but natural language has many ambiguities and idiosyncrasies that can render it useless in various situations.
You can try to define formal semantics, but that is not only hard to create, it's also hard to translate into an implementation, adding significant overhead in both parts of the process. And there can still be bugs, and there can still be edge cases with undefined behavior.
A formal spec would be good enough too. But since he's specifying concrete output and graphics as part of the language, it's rather hard to specify binary-compatibility without a reference implementation.
This is why there are no interpreted languages without a reference implementation that haven't failed miserably.
I would rather have a formal spec as the definitive one. Deriving a formal spec from a readable one seems to hit ambiguous cases all the time. Just look at publications that do that for C or Java.
With a formal spec you could also derive an implementation automatically which is a great useable reference. Look up the K framework for one possibility.
A formal specification would be basically useless, if nothing guarantees that the reference implementation actually follows it. Sharing & contributing to the same test suite is a much more practical approach.
This is a somewhat heretical opinion but I don't think having a formal specification is particularly important for programming languages today.
It was very valuable, say, twenty years ago, when there were most programs were written or compiled using multiple closed source implementations of languages coming from competing companies. There were real economic incentives for the implementations to diverge from each other in ways that harmed the larger ecosystem. A formal spec was a forcing function to make those implementations compatible.
Today, programmers simply won't use a language whose implementation isn't open source with a very permissive license. This makes it very hard for an organization to deliberately make the implementation incompatible with others because other organizations and users are able to either avoid the incompatibility by forking the implementation if they don't like it, or making it compatible by using the implementation if they do.
I still think it's very valuable to have a committee with members of all implementations that helps drive consensus for where the language should go. But the document itself I see as secondary to that human process.
Does this move the bugs from the implementation language to the language of the verification spec? Or is there a way to express some generic requirements such as "don't strand assets"?
Yes, a language specification is just a prerequisite for standardization. However, it's also useful for people who want to write their own implementation or tools. It also makes issue handling a bit smoother, because you can always check what the spec says if two bits of the ecosystem disagree with each other.
.. Or in a language designed for proof of correctness? See e.g. https://mitls.org/ -- I think this is very important work. Imagine only dealing with bugs in the spec?
Maybe one day, when all the hearts are finally bled, something like this will become the default unless and until you have a proven^1 unmet performance requirement, and only then after you've spoken to your lawyers.
You don't need a formal language standard to make Rust usable for safety-critical areas. You do need a formally specified language for the certification, but it doesn't have to be official because heck, you need much more than a mere formally specified language anyway as you've just said. An expanded version of Ferrocene would just fit the bill for example.
I think some people are obsessed about the "formal" specification or the language "standard" because they are misunderstanding their effects. They are absolutely nothing without additional supports. A "formal" specification in this context is not really mathematically formal (like, say, WebAssembly [1]); it merely means that a specification is written in clearly defined terms and logically decomposable statements. A language "standard" is useless if it isn't or can't be enforced, and it doesn't even require the (non-mathematical) formality (though most standard organizations would demand that). As for now, the Rust language specification is "formal" and "standard" enough to be useful for language users, while it remains useful for third-party implementors but they can still find some gaps here and there.
I'm perfectly fine with the idea of code-as-specification like that. And you're right, a lot of these assumptions could probably be so encoded (some I'm not sure about - e.g. how would you static_assert for two's complement, without triggering UB?). But I think this sort of thing would need some official blessing to be widely adopted, regardless of whether it's a written spec or a header.
Well no, the whole point is that the spec is not detailed enough to be code. Of course it leaves out details. I feel like this conversation will diverge to generalities without an example. So, take the WebAssembly spec for example. There's a reason it's written in "spec" language and not just some C code (or any other programming language, for that matter). But that's a very precise spec.
In reality, a loose spec is better than no spec. For example:
1. The loader should be able to parse an input file of up to 100MB in under 1 second.
2. The loader should support XYZ files version 3, 3.2, 3.3, and 4.0.
3. The loader should validate and reject erroneously formatted files.
4. The application should store internal state in robust storage that is independently inspectable.
5. The UI should be able to function if the backend database is down for less than 3 hours.
If you can't write ~1 page of such high-level requirements, why would you expect that you could start writing code? But we do. I mean, even I do!
A formal spec would be great but you're right. Plenty of people have done working layers of Linux in user-mode, etc. The only thing I know with formal specifications was filesystem API's for testing them. There have also been selective ones for things like robust drivers. Personally, I'd love to see one just to document all the state and covert channels. Especially visually. I bet it would be one, big-ass, messy graph. :)
You do not have the right to put words in my mouth, or to claim that your twisted version is what I was saying.
A spec is more detailed and more precise than (other) documentation and design documents. ("Other" because the spec is itself part of the documentation, and one of the design documents.) For the safety-critical software itself, you would demand a full, formal spec, not just "documentation". (At least, if you wouldn't, then others would. and they are right to do so.)
But if you demand that for the software, doesn't it make at least some sense to ask it of the compiler? And even if you don't think it makes sense for the compiler, it seems reasonable that the standard libraries of the language should face the same requirements as the subroutines that are part of the safety-critical software.
My impression is that making everything formally verified is a lot of work and it would be very hard to make formally verified code as easy to write as non-verified code.
Are you thinking of offering to write the formal specifications too, or try to formally verify compliance to a customer's specification?
Does your tool attempt to mechanically create its own proof that the specification is satisfied by the code, or does that involve human effort? (Or both?)
Is this spec actually correct and complete? Shrug...
Does this JavaScript actually implement the spec exactly? LoL!
At least being told what to fix in your code so that it actually implements your spec is a big step up over "staring at your code really hard." Good formal systems make it easy to find inconsistencies and incompleteness in your specs. Very good formal systems should make it easy to test and verify your spec against your intent.
reply