Learn You an Agda (opens in new tab)

This is often tedious but can be automated to some extent and has already led to significant achievements. See http://sel4.systems, a proven kernel, done with Isabelle, a tool similar to Agda.

Maybe you are looking for a language with a type system that will force you to write your program in a safe way regarding sockets and the like. This can also be achieved with static analysis, another way of automatically proving properties about programs. I do not know of any for distributed programs but it is probably possible. I would say this is still a research topic as such programs are still so hard to get right.

http://www.wisdom.weizmann.ac.il/~harel/papers.html

Do an in-page search for terms like temporal, behavioral, scenario, LSC, live sequence. By the way, I'm no expert but am interested in similar applications.

You can proof almost anything in agda. Even the most complicated mathematical theorems.

>What I'm most interested in is proofs that, say, in a concurrent environment, a function that closes a socket will never be called as long as there are pending tasks to write to the socket. Or, because I write concurrent data structures, I'm interested to prove that a certain function will eventually release all locks it acquires. Are there any such languages?

You can do this in agda, however, you need to specify semantics of the language you use.

> At the end of the day, programs are written for their side effects

The reason for such a focus on data transformation is that it's very easy to do in these purely functional languages (Agda included). It's so easy, in fact, that "other" things, like side effects, event handling, etc. are represented as data transformations. This is most obvious in Haskell, since laziness decouples definition from computation; eg. making it trivial to represent event streams as infinite lists.

> What I'm most interested in is proofs that, say, in a concurrent environment, a function that closes a socket will never be called as long as there are pending tasks to write to the socket.

The usual approach is to define a datatype of operations you might want to perform (eg. `Write String`, `Read Length`, etc.). Next you define a datatype which can combine these operations together in ways you may want (eg. something like a rose tree, if you want threads firing off threads). This forms an "embedded domain-specific language". We then write a bunch of helper functions for manipulating these datastructures (eg. a "combinator library"), then we use these to write down what we actually want as a combination of operations.

Next we write an interpreter function which opens a socket, performs all of the operations in the tree (possibly in multiple threads), waits for them to finish then closes the socket.

> Or, because I write concurrent data structures, I'm interested to prove that a certain function will eventually release all locks it acquires. Are there any such languages?

You can do the same thing as with the socket example, except you can strengthen the type of your program (operation-combining) datastructure to enforce that locks are released. As a simplified example, we can force a serial computation to release locks by only allowing AQUIRE and RELEASE to be inserted together:

    data Op = Foo | Bar | Aquire ID | Release ID

    data SafeOp = SFoo | SBar

    data Program : Type where
      NoOp : Program  -- Empty Program
      WithLock : Program -> Program  -- Add lock ops to a Program
      PrefixOp : SafeOp -> Program -> Program  -- Add a non-lock Op to a Program
      Interleave : Program -> Program -> Program  -- Combine two Programs

    -- Part of the interpreter, not exposed to the world
    progToOps : Program -> [Op]
    progToOps NoOp = []
    progToOps (WithLock id p) = [Aquire id] ++ progToOps p ++ [Release id]
    progToOps (PrefixOp SFoo p) = [Foo] ++ progToOps p
    progToOps (PrefixOp SBar p) = [Bar] ++ progToOps p
    progToOps (Interleave p1 p2) = interleave (progToOps p1) (progToOps p2)

    interleave [] ys = ys
    interleave (x:xs) ys = [x] ++ interleave ys xs

    [] is NoOp
    [Foo, Bar] is PrefixOp SFoo (PrefixOp SBar NoOp)
    [Foo, Aquire A, Bar, Aquire B, Release A, Foo, Release B] is Interleave (PrefixOp SFoo (PrefixOp SBar NoOp)) (Interleave (WithLock A NoOp) (WithLock B (PrefixOp SFoo NoOp)))

tl;dr: side effects are overrated.

I love to look at unicode, but is it a pain to type it in practice, even given emacs?

I don't think so, but Natural numbers can't be represented as two's-complement "integers"; neither can Integers.

There are many ways to encode such numbers if you really want; the easiest are probably "Fin (2^32)" for a type with 2^32 members (easy to convert to/from unary Naturals), or "Vect 32 Bool" for a list of 32 Booleans (easy to do bitwise stuff). You'd need to decide how to truncate the Naturals though; do you take min(x, 2^32 - 1)? Do you take x % 2 ^ 32?

Also, note that "S (S (S (S Z)))" isn't really a list; to turn it into a list we'd have to associate some trivial data with each constructor, eg. [NULL, NULL, NULL, NULL].

    {-# BUILTIN NATURAL ℕ #-}

> Oh dear. This is a new use of the word elegant I have not encountered before.

The Peano numbers are elegant because they correspond directly with induction. Agda is first and foremost a proof assistant, so it's natural that we lean towards things that help as write our proofs. This is not "Lisp-style" at all, it's a mathematically consistent way of defining natural numbers. The idea extends further with ornamentation to model lists and other data structures.

> Having defined an entirely unworkable method of representing integers because their standard library apparently doesn't do so (?!) they then go on to prove things like 1 + 1 == 2.

I don't know what's "unworkable" about Paeno arithmetic. Yes, it's not the most efficient representation, but you're working in a proof engine, so that is secondary to our concerns. Furthermore, Agda has {-# BUILTIN #-} pragmas that let us switch out this data type with something that is more optimal. We don't use "the number system actually used by humans" (whatever that is) or machines, at least traditionally, because they just make the proofs harder.

> Perhaps in another few decades someone will have bothered to make a dependently typed language that doesn't use untypeable characters as part of its syntax, and has an integer type built in

Yea, some of us did "bother" - you're looking for Idris. But I'd really rather you didn't join us.

If you're interested in a "practical" dependently-typed language, check out Idris:

http://www.idris-lang.org/

http://www.ats-lang.org/Examples.html http://www.idris-lang.org/

    ghci> map (++ "!") ["BIFF", "BANG", "POW"]
    ["BIFF!","BANG!","POW!"]

In a Dependently Typed (DT) language like Agda the language of values and the language of types are one and the same. Thus, a function from types to types is exactly the same sort of thing as a function from values to values. In this case we have a third sort of totally-natural-day-old-kind-of-thing: a function from values of ℕ to types (in Set). It's "just" a function from values to types.

Now, we annotate values with their types. Thus we might have a new top-level definition

    something : zero even
    something = _

In the beginning, there was Set, which is the set of all valid types. It's empty (more or less). Then comes along

    data ℕ : Set

So we must tell it what its members are. We COULD do it like this:

    zero : ℕ
    one : ℕ
    two : ℕ
    three : ℕ

    data ℕ : Set where
        zero : ℕ
        succ : ℕ → ℕ

People see the arrow and they think functions. That's not how I think about it. Functions are great, but when I hear function I think C functions, which are tiny little instructions for tiny little machines and don't make any sense in a dependently-typed world. So instead, when I see the arrow, I think of it as a way of telling the type checker this fact: wherever you see the string "succ n", assign it the type ℕ but ONLY IF "n" is also of type ℕ. Think of the arrow as the lambda abstractor, and the space as the lambda applicator. Maybe that helps a little; maybe it hurts a lot.

We plunge forward!

    _+_ : ℕ → ℕ → ℕ
    zero + n = n
    (succ n) + m = succ (n + m)

We would now like describe even numbers in Agda. Could we just define

    data even : Set?

    data even 0 : Set
    data even 2 : Set
    data even 4 : Set

    data even : ℕ → Set

    data even : ℕ → Set where
        even_everything_is_goddamn_even : (n : ℕ) → even n

    data even : ℕ → Set where
        even_zero : even zero
        even_succ : (n : ℕ) → even n → even (succ (succ n))

It's simply another form of induction, although slightly trickier because we're trying to fill out a proposition.

Anyway. Hope that helps more than it confuses. I think Learn You An Agda makes it more confusing that it really is by not explaining Set and by using that weird postfix notation. Set is just Haskell's asterisk kind "*" if you know Haskell; otherwise it's pretty hard to grok for a while.

You should also check out Benjamin Pierce's textbook on Coq programming, which expands on a lot of these details. (Coq and Agda and Idris are all pretty much are built on the same ideas.)

http://www.cis.upenn.edu/~bcpierce/sf/current/index.html

    module LearnYouAn where
    
      data ℕ : Set where
        zero : ℕ
        succ : ℕ → ℕ
    
      _+_ : ℕ → ℕ → ℕ
      zero + m = m
      (succ n) + m = succ (n + m)
    
      data _even : ℕ → Set where
        ZERO : zero even
        STEP : ∀ n → n even → succ (succ n) even
    
      proof₁ : succ (succ (succ (succ (zero)))) even
      proof₁ = ?

Some excerpts:

> Agda is a programming language that uses dependent types ... you can actually include values inside a type. For example, the List type constructor can be parameterized by both the type of its contents and the length of the list in question ... . This allows the compiler to check for you to make sure there are no cases where you attempt to call head on a potentially empty list, for example.

> If I can come up with a function of type Foo -> Bar (and Agda says that it’s type correct) that means that I’ve written not only a program, but also a proof by construction that, assuming some premise Foo, the judgment Bar holds.

> Proofs work in concurrent scenarios. You can’t reliably unit test against race conditions, starvation or deadlock. All of these things can be eliminated via formal methods.

> Thanks to Curry-Howard, Agda can also be used as a proof language, as opposed to a programming language. You can construct a proof not just about your program, but anything you like.

You might also want to compare to Idris (and maybe Epigram, but its no longer in development).

http://www.quora.com/How-does-Idris-compare-to-other-depende...

http://www.reddit.com/r/haskell/comments/132kg0/agda_epigram...

http://www.reddit.com/r/dependent_types/comments/q8n2q/agda_...

http://stackoverflow.com/questions/9472488/differences-betwe...

All have pros and cons; i like that Idris can compile to JS (https://raichoo.github.io/posts/2014-01-28-improved.html)