Are there any provable real-world languages? (scal

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

In order to answer this question, you really need to define what you mean by "provable". As Ricky pointed out, any language with a type system is a language with a built-in proof system which runs every time you compile your program. These proof systems are almost always sadly impotent — answering questions like String vs Int and avoiding questions like "is the list sorted?" — but they are proof systems none-the-less.

Unfortunately, the more sophisticated your proof goals, the harder it is to work with a system which can check your proofs. This escalates pretty quickly into undecidability when you consider the sheer size of the class of problems which are undecidable on Turing Machines. Sure, you can theoretically do basic things like proving the correctness of your sorting algorithm, but anything more than that is going to be treading on very thin ice.

Even to prove something simple like the correctness of a sorting algorithm requires a comparatively sophisticated proof system. (note: since we have already established that type systems are a proof system built into the language, I'm going to talk about things in terms of type theory, rather than waving my hands still more vigorously) I'm fairly certain that a full correctness proof on list sorting would require some form of dependent types, otherwise you have no way of referencing relative values at the type level. This immediately starts breaking into realms of type theory which have been shown to be undecidable. So, while you may be able to prove correctness on your list sorting algorithm, the only way to do it would be to use a system which will also allow you to express proofs which it cannot verify. Personally, I find this very disconcerting.

There is also the ease-of-use aspect which I alluded to earlier. The more sophisticated your type system, the less pleasant it is to use. That's not a hard and fast rule, but I think it holds true for the most part. And as with any formal system, you will often find that expressing the proof is more work (and more error prone) than creating the implementation in the first place.

With all that out of the way, it's worth noting that Scala's type system (like Haskell's) is Turing Complete, which means that you can theoretically use it to prove any decidable property about your code, provided that you have written your code in such a way that it is amenable to such proofs. Haskell is almost certainly a better language for this than Java (since type-level programming in Haskell is similar to Prolog, while type-level programming in Scala is more similar to SML). I don't advise that you use Scala's or Haskell's type systems in this way (formal proofs of algorithmic correctness), but the option is theoretically available.

Altogether, I think the reason you haven't seen formal systems in the "real world" stems from the fact that formal proof systems have yielded to the merciless tyranny of pragmatism. As I mentioned, there's so much effort involved in crafting your correctness proofs that it's almost never worthwhile. The industry decided a long time ago that it was easier to create ad hoc tests than it was to go through any sort of analytical formal reasoning process.

Answer 2

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 3

My (controversial) definition of "real-world" in the context of provably-correct code is:

• It must involve some degree of automation, otherwise you're going to spend far too much time proving and dealing with messy little details, and it's going to be totally impractical (except maybe for spacecraft control software and that sort of thing, for which you might actually want to spend megabucks on meticulous checks).
• It must support some degree of functional programming, which helps you write code that is very modular, reusable and easier to reason about. Obviously functional programming isn't needed for writing or proving Hello World, or a variety of simple programs, but at a certain point, functional programming does become very useful.
• While you don't necessarily have to be able to write your code in a mainstream programming language, as an alternative, you should at least be able to machine-translate your code into reasonably efficient code written in a mainstream programming language, in a reliable way.

The above are relatively more universal requirements. Others, such as the ability to model imperative code, or the ability to prove higher-order functions correct, may be important or essential for some tasks, but not all.

In view of these points, many of the tools listed in this blog post of mine may be useful - although they are nearly all either new and experimental, or unfamiliar to the vast majority of industry programmers. There are some very mature tools covered there though.

Answer 4

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 5

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.

Answer 6

How about Idris and Agda? Real world enough?

As a good real life example, there's a project that aims to provide a verified HTTP REST library written in Agda, called Lemmachine: https://github.com/larrytheliquid/Lemmachine