Are there any provable real-world languages? (scala?)

Question

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 1

Typed languages prove the absence of certain categories of fault. The more advanced the type system, the more faults they can prove the absence of.

For proof that a whole program works, yes, you're stepping outside the boundaries of ordinary languages, where mathematics and programming meet each other, shake hands and then proceed to talk using Greek symbols about how programmers can't handle Greek symbols. That's about the Σ of it anyway.

Answer 2

You can investigate purely functional languages like Haskell, which are used when one of your requirements is provability.

This is a fun read if you're interested about functional programming languages and pure functional programming languages.

Answer 3

You're asking a question a lot of us have asked over the years. I don't know that I have a good answer, but here are some pieces:

• There are well-understood languages with the possibility of being proven in use today; Lisp via ACL2 is one, and of course Scheme has a well-understood formal definition as well.

• a number of systems have tried to use pure functional languages, or nearly pure ones, like Haskell. There's a fair bit of formal methods work in Haskell.

• Going back 20+ years, there was a short-lived thing for using hand-proof of a formal language which was then rigorously translated into a compiled language. Some examples were IBM's Software Cleanroom, ACL, Gypsy, and Rose out of Computational Logic, John McHugh's and my work on trustworthy compilation of C, and my own work on hand-proof for C systems programming. These all got some attention, but none of them made it much into practice.

An interesting question to ask, I think, is what would sufficient conditions be to get formal approaches into practice? I'd love to hear some suggestions.

Answer 4

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 allow 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. Programming and proving goes hand in hand (the Curry-Howard correspondence even equates them completely!)

  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 1, 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

Answer 5

Scala is meant to be "real world", so no effort has been made to make it provable. What you can do in Scala is to produce functional code. Functional code is much easier to test, which is IMHO a good compromise between "real world" and provability.

EDIT ===== Removed my incorrect ideas about ML being "provable".

Answer 6

real world uses of such provable languages would be incredibly difficult to write and understand afterwoods. the business world needs working software, fast.

"provable" languages just dont scale for writing/reading a large project's code base and only seem to work in small and isolated use cases.