Learn You an Agda

Post by pron » Tue, Dec 02, 2014, 11:54 PM UTC

michaelsbradley wrote: post #15

pron wrote: post #9

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. Not that data transformations aren't important, but the properties they need to preserve are usually easy to be convinced of without any assistance by the compiler. At the end of the day, programs are written for their side effects (u…

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.

Post by rspeer » Wed, Dec 03, 2014, 12:06 AM UTC

solomatov wrote: post #18

pron wrote: post #9

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. Not that data transformations aren't important, but the properties they need to preserve are usually easy to be convinced of without any assistance by the compiler. At the end of the day, programs are written for their side effects (u…

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

Post by Gigablah » Wed, Dec 03, 2014, 12:12 AM UTC

Dewie wrote: post #14

wlesieutre wrote: post #6

Earlier quoted context omitted.

On top of the pictures, the examples are a lot more fun than foo and bar. Here's (part of) how Learn You a Haskell introduces map: ghci> map (++ "!") ["BIFF", "BANG", "POW"] ["BIFF!","BANG!","POW!"]

I hate foo/bar for some reason. I think it's because it is supposed to be "this is just whatever", and yet they force me to think about Kung Fu, the Foo Fighters and crowbars.

Post by evincarofautumn » Wed, Dec 03, 2014, 12:23 AM UTC

mcbuilder wrote: post #20

lelf wrote: post #12

I like to show you the immense beauty of the Agda standard library: http://agda.github.io/agda-stdlib/html/README.html (all clickable and…you'd better have proper unicode fonts).

Even something as mundane as Data.Bool is beautiful, defining False in terms of bottom. I love to look at unicode, but is it a pain to type it in practice, even given emacs?

Post by cies » Wed, Dec 03, 2014, 12:32 AM UTC

kxyvr wrote: post #24

Is there any reason to use Agda over Coq or vice versa?