> Languages that use types for elaborate proofs always seem to me like they only prove the most uninteresting properties of programs, namely the parts that deal with data transformations.
> 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
Notice that progToOps can never output a list containing Aquire without also containing a Release with the same ID. Also notice that we can define arbitrary combinations of the other ops:
[] 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)))
Of course these datastructures would be build up by helper functions instead of by hand, would be tree-like for concurrency, would probably provide guarantees per sub-tree, would allow arbitrary functions (of some suitable type) in place of Foo, Bar, etc.