Learn You an Agda

Wow, you are just radiating ignorance; I don't even know why I'm wasting my breath. Nonetheless,

> 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 we can construct a value of a certain type, we have simultaneously constructed a proof that the theorem encoded by that type holds.

    data _even : ℕ → Set where

I do not understand how to interpret this passage. _ even, given a number, returns a type? in this case, zero even is a type, but we have not created any value with that type. What am I missing?

Sounds like you are interested in applications of temporal logic for formal verification in software development, which is an area of active research. Prof. David Harel works in that field:

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.

Given formal semantics of your programming language and some time, I think you can use Agda to prove interesting properties about correct programs you write in that language. Semantics, the behaviour of objects such as sockets, can be encoded in types the theorem prover can understand. It can look like this for a basic imperative language: https://github.com/Twey/imp-agda/blob/master/IMP/Semantics/O.... You can then define the property you are interested in and get your proof by combining these types together.

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.

Oh, nice! Indeed I'm not sure that's what I want, but this seems like the first statically-typed FP language I like. I especially like how you can program the type level with constructs similar to the program level.