Why is the lack of a formal language specification bad?

community
1

In a section describing Rust's weaknesses, cheats.rs says:

no formal language specification preventing use in some domains (aviation, medical, ...)

Drew DeVault also raises that point in an article arguing against using Rust as a replacement for C.

This discussion provides great resources for watching that effort progress. But I don't understand why this is bad. So, to my actual questions.

  • in your personal experience, what negative consequences have you seen from languages lacking a formal specification?
  • in the history of software development where has this caused problems and what kind of problems were they?

Feel free to answer either or both.

3 Likes
2

Formal specification of the language is definitely good to have, so lacking of it would be relatively bad, though it doesn't make the language totally unusable.

If the language has formal specification, and if we have mathematically proven compiler which guaranteed to generate code to follow that spec, we can mathematically prove our code that it doesn't violates certain rules. Some domains like airplane engine control system requires such level of safety.

3 Likes
3

The existence of a specification does not mean that the compiler is correctly implemented and free of bugs. Are mathematical proofs really possible when trading with optimization tricks and other weird compiler things? If not, the only way to know if something is ready for aviation is testing a lot.

The lack of specification is a problem if someone wants to implement a new compiler or code parser, or when the examples of the book are not sufficient to explain all the possibilities of using a given feature.

3 Likes
4

But it's extremely relevant to liability, which is a huge deal when you're dealing with (1) things that fly and (2) things that keep people alive. Formal specifications are not just technical documents; they are legal tools that limit liability. If a compiler upgrade causes a plane to crash, a formal specification (in conjunction with a contract that refers to it) can make the difference between "my fault" and "not my fault".

Of course! An optimizer is basically a huge proof engine for theorems of the form "Given the author of this code is following the rules, the observable behavior of this code is the same as that code (which has better performance)." Formalizing the spec is just about defining clearly what those rules and behavior are, so you can make statements like "this code has correct behavior when compiled with any C99 compliant compiler" instead of "eh, if it passes all the tests it'll probably be ok".

4 Likes
5

The compcert C compiler is an mathematically proven optimizing C compiler.

9

This topic was automatically closed 90 days after the last reply. We invite you to open a new topic if you have further questions or comments.