Are there any provable real-world languages? (scala?)
I was taught about formal systems at university, but I was disappointed how they didn't seem to be used in the real word.
I like the idea of being able to know that some code (object, function, whatever) works, not by testing, but by proof.
I'm sure we're all familiar with the parallels that don't exist between physical engineering and software engineering (steel behaves predictably, software can do anything - who knows!), and I would love to know if there are any languages that can be use in the real word (is asking for a web framework too much to ask?)
I've heard interesting things about the testability of functional languages like scala.
As software engineers what options do we have?
Answer
Yes, there are languages designed for writing provably correct software. Some are even used in industry. Spark Ada is probably the most prominent example. I've talked to a few people at Praxis Critical Systems Limited who used it for code running on Boings (for engine monitoring) and it seems quite nice. (Here is a great summary / description of the language.) This language and accompanying proof system uses the second technique described below. It doesn't even support dynamic memory allocation!
My impression and experience is that there are two techniques for writing correct software:
Technique 1: Write the software in a language you're comfortable with (C, C++ or Java for instance). Take a formal specification of such language, and prove your program correct.
If your ambition is to be 100% correct (which is most often a requirement in automobile / aerospace industry) you'd be spending little time programming, and more time proving.
Technique 2: Write the software in a slightly more awkward language (some subset of Ada or tweaked version of OCaml for instance) and write the correctness proof along the way. Here programming and proving goes hand in hand. Programming in Coq even equates them completely! (See the Curry-Howard correspondence)
In these scenarios you'll always end up with a correct program. (A bug will be guaranteed to be rooted in the specification.) You'll be likely to spend more time on programming but on the other hand you're proving it correct along the way.
Note that both approaches hinges on the fact you have a formal specification at hand (how else would you tell what is correct / incorrect behavior), and a formally defined semantics of the language (how else would you be able to tell what the actual behavior of your program is).
Here are a few more examples of formal approaches. If it's "real-world" or not, depends on who you ask :-)
- The Coq Theorem Prover: Programming with Coq (technique 2)
- ESC/Java (technique 1, neither sound nor complete though)
- Spec# (technique 1, neither sound nor complete though)
- Why / Krakatoa (technique 2, based on Java)
I know of only one "provably correct" web-application language: UR. A Ur-program that "goes through the compiler" is guaranteed not to:
- Suffer from any kinds of code-injection attacks
- Return invalid HTML
- Contain dead intra-application links
- Have mismatches between HTML forms and the fields expected by their handlers
- Include client-side code that makes incorrect assumptions about the "AJAX"-style services that the remote web server provides
- Attempt invalid SQL queries
- Use improper marshaling or unmarshaling in communication with SQL databases or between browsers and web servers