At the end of the day, programs are written for their side effects (unless your program is a compiler, which is the classical example of an "interesting", non-trivial data transformation, and possibly the only example). 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?

I've heard of effect systems, but I couldn't find enough information on them. Are effect systems capable of the kind of proofs I'm interested in? Are there practical programming languages with powerful effect systems?

EDIT: Some Googling yielded this: http://lambda-the-ultimate.org/node/4768 tldr: Not yet.

EDIT: At least the lock proof seems to be implemented as one of Java 8's pluggable type systems: http://types.cs.washington.edu/checker-framework/current/che...

It lets you add a type (Java 8's pluggable types are intersection types) to a function called @EnsuresLockHeld(locks...) that proves some locks will be held when a function returns and even @EnsuresLockHeldIf(locks..., result) that proves a function grabs certain locks if its boolean result is equal to the one specified in the type.

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.

    fun list () =
            rows <- queryX (SELECT * FROM tab AS T)
                           (fn (fs : {T : $([Id = int] ++ map fst M.cols)}) => <xml>
                             <tr>
                               <td>{[fs.T.Id]}</td>
                               {@mapX2 [fst] [colMeta] [tr]
                                 (fn [nm :: Name] [t ::_] [rest ::_] [[nm] ~ rest] v col => <xml>
                                   <td>{col.Show v}</td>
                                 </xml>)
                                 M.fl (fs.T -- #Id) M.cols}
                               <td>
                                 <a link={upd fs.T.Id}>[Update]</a>
                                 <a link={confirm fs.T.Id}>[Delete]</a>
                               </td>
                             </tr>
                           </xml>);

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.

And I think that's the thing that makes Agda interesting. If you limit Agda to proving things about computer programs, it doesn't sound that special. People are using Agda to prove things about, for example, topology.

> 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)))

The fact that your DSL is represented as an immutable datastructure by the host is really not important. Any code you write is going to be turned into a datastructure at some point. The immutability should be read as "the context in which this result is valid has been made fully explicit", where "context" includes "things that mutate over time". You don't loose in expressivity, you just can't forget to handle special cases.

Checker (Java 8's pluggable intersection type-system framework) is able to do that (define side-effect types), but isn't a single general type system. I.e. you need to write a different type system for each property (of course, they can all work together). Maybe that's the only known way to do that. Searching for more general solutions, I've come up empty handed (the problem is well known, but the solutions are all in early stages of research).

The idea of such a type system needs to be something like: each function has a set of types associated with it, and a function's type interacts with the types of the functions it calls in some ways. So the most primitive example is, of course, checked exceptions, where the type of a function is a simple union of the types of its callees. But the interactions can, and should be more interesting, and take into account the order in which the callees are called etc.

> a type system limitation that every type describing side effects [...] can only be used in the context of a compiler/interpreter.

A type system is just a logic description of a property that a program might have. It specifies how the language constructs interact with this property []. The fact that compilers use a type system is independent of your ability to write your custom type system, or to use it in a different context (IDE, toolchain, ..).

[] Are you saying that a type system shouldn't be concerned by the AST of the language?

An external type checker for Haskell: http://goto.ucsd.edu/~rjhala/liquid/haskell/blog/blog/2013/0... And the various type checkers for the not statically typed languages (python, ..)

Also, I don't understand why you distinguish "typing side effects" as something different from the rest?

> you need to write a different type system for each property

But you do have to define your type system at some point? Are you thinking of something like Mezzo, where some userland properties can be defined without going down the type-system-definition road? https://protz.github.io/mezzo/

> But the interactions can, and should be more interesting, and take into account the order in which the callees are called etc.

That's why type systems are defined with respect to the language construct, by rules on the AST (? I'm confused because of the earlier [*] here).

To go back to Agda significance for a custom type system, it's not enough to define a type system. You generally want to prove that your definition is valid: If your "checked exceptions" says that a program `P` can't fail due to an exception, you want to check that you didn't forget anything by verifying the type checker with respect to the actual semantic of the language.

You can also embed your custom property into Agda type system (isn't that what you want?).

I will be able to define a type "locks A" and "locks B", and the kind "locks" will be ordered, so that the type of a function that locks A and locks B, will be "locks A and then locks B". Also, I will be able to define interactions between types so that unlocking A will undo the effect, so that a function that simple locks A will have the type "locks A", but one that locks and later unlocks will have the type "holds A". Of course, these types intersect arbitrarily.

Well, to describe a side effect, you need to, uh, describe the side effect. Which requires understanding the compiler/interpreter, and a description of the things the compiler/interpreter does, expressed as machine-readable data.

It sounds like what you're after is something like a standard library where all the effects are carefully enumerated? i.e. something like Haskell, but where rather than the IO "sin bin", every effectful function would be very explicit about its effects? A bit like how Ada(IIRC) shipped with quite high-level concurrency operations as part of the language spec (which then lead users to reimplement low-level concurrency primitives on top of them, but maybe we can hope that history wouldn't repeat)?

Some libraries are taking us in that direction, but it's slow going. E.g. doobie seems to be gaining some momentum, as a principled way of expressing database access. Maybe in 10 years' time (if anyone is still using scala...) this will be "the" standard way of writing any program that uses a database, and the sort of thing that deserves to be in the standard library (whatever that means - IMO with modern dependency management tools a language standard library should only contain those primitives that need direct compiler support, anything else can be a regular library. But that's a whole 'nother argument). But right now it would be very premature to say that the algebra doobie uses is the correct one. Often the appropriate interpreter for a particular problem depends on that particular problem; just as it's good to construct your datatypes bottom-up, writing a program can feel like writing a succession of interpreters that get closer to your domain and capture more of the laws - basic Haskell gives you "thing that does any kind of I/O", then you have a library for "thing that sends complete messages to sockets", a higher-level library on top of that for "thing that does database operations", and so on.

And honestly standardization isn't that important, as long as the language makes it easy to let your code handle it generically. Doobie itself allows a couple of different implementations for your lower-level effect-capturing monad (scalaz Task, IO), or allows you to provide a simple adapter. So if two libraries use the equivalent of a different checker, a different "type system", that's not really any worse than e.g. two C++ libraries using two different String classes - that is to say, it's annoying, but not impossible to work with. User-level code can do the same thing - I've got a generic "report" process that can use a doobie database call, an async call to a web service, or something else. As and when the community reaches a consensus on the right way to express a particular kind of effect, I'd expect more higher-level libraries to standardize on that. But in the meantime, as long as types are first-class values and you can manipulate them as easy as any other values (which these kind of languages get you), multiple "type systems" are no more of a problem to work with than multiple types.

[1]: for example, the type of the caller can be: "this function locks A, then B, then unlocks B, then unlocks A". This type can arbitrarily intersect other effect types, such as: "this function writes to socket X" and also "mutates variable V"

Isn't chriswarbo's example that? Since your Ops are generic they can be other effect types. The interleaving is the tricky part, but e.g. Haskell's extensible-effects is practical enough that it's used in real programs.

That's the key idea ;)

If I write some Java like `DB.connect(credentials).select("users").where("name", "Kevin")`, am I using "some new language"? As far as Alan Kay is concerned, yes; that was one of his main inspirations for OOP:

> My math background made me realize that each object could have several algebras associated with it, and there could be families of these, and that these would be very very useful.

From http://www.purl.org/stefan_ram/pub/doc_kay_oop_en

The only difference between that Java example and my earlier Haskell/Agda example is that the functional version operates in two phases: calculating which operations to perform (building a `Program` containing `Ops`) is separate to performing those operations (applying an interpreter function to a `Program`).

However, keep in mind that we're not doing imperative programming, so there's is no inherent notion of time: we get the same result no matter which order we evaluate stuff in (that's the Church-Rosser Theorem). Hence these two "phases" are logically distinct, but not necessarily temporally distinct. In practice, we tend to define our `Program` lazily, so it gets constructed on-demand by the interpreter.

This is a bit like having a `main` loop containing a `switch`, for example (forgive mistakes; I've never used function pointers in C):

    void main(op* instruction, int* length, void* callback) {
        socket* s = set_up_socket();
        int close = 0;
        char* data;
        while (!close) {
            switch(*instruction) {
                case READ:
                    // Read logic
                    data = read_from_socket(s, *length);
                    *callback(instruction, data);  // Update instruction based on data
                    break;
                case WRITE:
                    // Write logic
                    data = *callback(instruction);  // Update instruction and return data
                    write_to_socket(*length, data);
                    break;
                case CLOSE:
                    // Close logic (ignores any other instructions)
                    close = 1;
                    break;
        }
        close_socket(s);
    }

Does this mean that those callbacks are in "some different language" to C? No; everything is regular C except that we just-so-happen to be labelling some ints as `READ`, `WRITE` and `CLOSE`. Likewise, in Haskell/Agda/etc. we have the full breadth of the whole language available to us; we just-so-happen to be returning values of type `Op` and `Program`. All of our logic, concurrency, etc. is done in the "host" language; we only define `Op`s for the things we want to restrict, like `Read` and `Write`; there's absolutely no point defining operations for boolean logic, arithmetic, string manipulation, arrays/lists, etc. because that's available already. Of course, once we've finished defining our socket library, that too will be available to everyone (if we release it); just because it might use some crazy `Op`, `Program` and `runSocket` things internally doesn't mean anyone has to care about that; it's just an implementation detail.

Notice that this is very similar to an OOP dynamic dispatch system, where `READ`, `WRITE` and `CLOSE` are method names and the callbacks just-so-happen to be kept together in a struct which we call an "object". Just like Alan Kay said.

(forgive mistakes; I've never used function pointers in C)

You mostly got it right; the function declaration would look like this (I moved the * for pointers onto the parameter name for stylistic reasons related to how C declares types):

    void main(op *instruction, int *length, void (*callback)(...))

tl;dr: side effects are overrated.

Let's take CAD as an example. We've got a source language: a constructive solid geometry, for simplicity. Pretty much everything a CAD does boils down to various transforms of this language - into an optimised octree for rendering purposes, into G-code slices for production, into, say, SVG for blueprints, etc.

CRUD stuff boils down to transforms between different semantic domains - a relational structure at one end and workflow graphs and document trees on another.

It's really hard to come up with any practically important problem domain which would not benefit from being represented in terms of languages and transforms.

I have no reason why but I just like the freaking pictures. It keeps me going. It's like a children book but it also teaches me the subject I like, programming languages.

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

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

What happens in Data.Bool is that we have the function from values to types `T` such that `T true` and `T false` are types equal to top and bottom respectively. This value-to-type encoding is called a "universe" and allows us to talk about propositions which are based on boolean function results like

    theorem1 : T (1 - 1 == 0)

    theorem2 : 1 - 1 = 0

[0] http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Docs.Unicod...

Type the following into an emacs buffer, and then type C-c C-l (use \_1 to type the subscript symbol ₁):

  proof₁ : suc (suc (suc (suc zero))) even
  proof₁ = ?

I then tried restarting emacs and opening a new .agda file so I get agda mode. Loaded the earlier module and then tried loading this, and it didn't seem to know about suc in the context of this buffer/file. So now I'm lost.

    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₁ = ?

What's the distinction between C-c C-space and C-c C-r? It looks like the former computes proof obligations for ?s, but what does the latter do? And why couldn't we use the latter in the first instance, to deduce the outermost STEP ? ?

Edit: never mind, that did work.

Beats the hell out of me. Here's the docstring for agda2-give (bound to C-c C-SPC):

    Give to the goal at point the expression in it

    Refine the goal at point.
    If the goal contains an expression e, and some "suffix" of the
    type of e unifies with the goal type, then the goal is replaced
    by e applied to a suitable number of new goals.
    
    If the goal is empty, the goal type is a data type, and there is
    exactly one constructor which unifies with this type, then the
    goal is replaced by the constructor applied to a suitable number
    of new goals.

In case the compiler can do that conversion: is it is programmed to do that for some subset of numeric types or can it infer an optimal binary representation of a value somehow?

On the other hand, if they really were represented as lists then I presume this language is intended as purely academic work and has no application in a production environment. Am I wrong?

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 ℕ #-}

    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

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

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)

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.

By the way, Z notation rocks.

Because I'm probably going to stick with Coq for its tooling.

Hackernews always gets so much more comments.

Think eric raymond and too bad that perl is just another dead language -- your wisdom though as recompense. When you are older, it becomes EASIER for crunchfit and yes, it sometimes becomes harder to exercise to point of vomit - "ad nauseum' in Latin, but the pain is much easier. Don't you do three hundred (300) pushups a day?

So, the routine is simple. Get stuck running Haskell (another bump on the road to the true language of Coq) - go ahead and flame - do the pushups. Then laugh cause it releaxes and then refrshed back to AGDA.

PS. Engineering school was arduous and graduate school. The personal private books/research were just hobbies and no I will not mention my name. Even the so-called Yourdon 'death marches' are just a bump on the road.

It's worse than some females - over the period of a 'big city man.' - go ahead flame - Just take code from arxiv, run it in Haskell and Agda and there are only three explanations 1.)the programmer is stupdi - yup that's me 2.)scientific fraud - always possible 3.)the 'compiler' or the strange AMD CPU is fickle in a feminine way? 4.)the language paradigm is 'slightly broken.' 5.) all of the above

Fair Warning and Serpents be Here. Haskell, Agda and even Coq are DEFINED as EXPERIMENTAL RESEARCH Languages. Of course, you can always go Python (which version?) and Javascript, which is the bubble gum and string that holds together the Internet.. along with BAsh shellshock.

It this why they call it a bit of 'hacking'? PPS. learn to ride bicycle in big city and survived with most of my fingers intact.

> 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.

_Agda is a programming language_

That's the standard it sets right from the first chapter. It then goes on to say that this programming language doesn't have numbers.

If the book had said, "Agda is a proof assistant for CS and mathematics researchers to research inductive logic" then I'd have been much less harsh on it, but whilst this book is claiming it's a tool for programmers I will judge it by that standard. And by that standard representing numbers and even forcing you to type them in as (suc (suc (suc (zero))) is not elegant.

The early examples you see with inductive structures such as Nat are about learning the foundations, and you can't go on to do anything especially interesting without a solid understanding of the foundations. Its structure often also turns out to have a convenient correspondence with more realistic data structures, such as lists (their length) and trees (their depth).

I do sometimes wonder if we should start using something more obviously useful as an introductory example though. There's plenty of possibilities, and programmers aren't generally going to be using Nats in practice (I rarely do).

I don't use Agda myself (I use Idris, which is similar but is more directly aimed at general purpose programming) but I do know that it has primitive types...

Anyway, there's all kinds of interesting work going on at the minute which goes way beyond these introductory examples. For example, we're working on a way of specifying and verifying implementations of communication protocols (https://github.com/edwinb/Protocols), which we'd like to apply to cryptographic protocols when we've made some more progress. You can hear me waffling on about that, as well as about how we deal with stateful systems in general, here: https://www.youtube.com/watch?v=rXXn4UunOkE&feature=youtu.be

I post this mainly because I suspect I'm one of the wonks who was researching dependently typed programming at your university ten years ago. At the time, there was lots of foundational work to do, and there is still lots to do before it's industrial strength, but we've made a lot of progress, and I think the goal is worth striving for.

> _Agda is a programming language_

Well, that's because programming languages and formal systems (proof languages) are the same thing ( http://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspond... ).

Agda is well-suited to computing with values that carry around various formally-checked properties. That's useful to some people for some tasks. If it's not suited to whatever you're doing, then don't use it; I presume your projects don't all use Java, Bash, Prolog, Python, COBOL, Pure, Unlambda and MATLAB at the same time; well, just add Agda to that list.

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/