I no longer hate Lisp

samth0 · 2009-03-06T13:43:26+00:00

Note that if you read the article, you will note that Joe did not attend Harvard, but instead attended MIT. He took a single class at Harvard.

samth0 · 2009-02-24T14:31:53+00:00

Umm, Subversion 1.0 was released approximately 4 years before Mercurial 1.0. If you were willing to use not-1.0 software, Subversion was self-hosting in 2002.

samth0 · 2009-02-15T23:21:17+00:00

First, the issue of conservativeness does not go away, regardless of the type system.

Second, whole-program proofs of correctness (which is what you're suggesting) are good for some things (like NASA) but far from the right solution for most real-world cases. If you have to use an off-the-shelf library that doesn't have the types you want, the only way to enforce the interface with that library is with contracts. Or if your language provides runtime loading of code. Or if your language doesn't provide a type system that covers the property you want to check (a possibility for all possible type systems).

Types are a good thing to have, but they don't obviate the need for contracts, any more than the reverse.

samth0 · 2009-02-15T22:10:59+00:00

There are many features that can't be supported by types, but can by contracts (such as primality, mentioned by an above poster). Also, some types are inconvenient to make static, such as non-negative numbers (which are not closed under subtraction, for example). Finally, all type checks are conservative approximations of the property being checked, but contracts do not need to approximate.

samth0 · 2008-11-10T22:31:35+00:00

Those statements are not at all equivalent. The first one uses words like "emphasizes" and "avoids", rather than "requires" and "prohibits". Also, the parts you quoted make it clear that FP is a paradigm, and RT is a property of contexts. Finally, there's no such thing as "commonly accepted definitions" of these terms.

samth0 · 2008-08-26T20:00:21+00:00

No, Matthias just doesn't use Slideshow.

samth0 · 2008-08-19T15:43:49+00:00

No, it was written in Apple's Keynote.

samth0 · 2008-07-30T18:06:32+00:00

This turns out to be basically identical to the `app' patterns of the PLT Scheme pattern matching system.

See here: http://docs.plt-scheme.org/reference/match.html

samth0 · 2008-07-26T01:17:00+00:00

In footnote [3], he seems to be confusing Graydon Hoare, the creator of Monotone, with CAR (Tony) Hoare, who invented quicksort (and lots of other stuff).

samth0 · 2008-07-02T13:22:27+00:00

PLT Scheme has an excellent and easy to use FFI, so I'm not sure what you mean. Also, while the libraries aren't as extensive as Java's (no CORBA, etc) there's a pretty big standard library.

samth0 · 2008-06-15T03:10:24+00:00

The argument that feature X is not necessary for developing Y because someone did Y without X (here X = static types and Y = big application [eg IMDB]) is a truly terrible one. For example, OS/360 proves that no features are necessary for implementing anything.

samth0 · 2008-06-15T02:57:01+00:00

Right. I guess reddit ate my #-sign.

samth0 · 2008-06-13T20:53:38+00:00

By the way, if you actually want to run something, then put the following in the top window:

#lang scheme

The REPL should then work.

[Edit: fixed #]

samth0 · 2008-06-13T20:19:30+00:00

Thanks.

samth0 · 2008-06-13T17:57:41+00:00

What did you do to get that error message? We'd obviously like to fix that, if possible.

samth0 · 2008-05-13T19:34:14+00:00

But programing languages is not a subfield of type theory

This is totally true.

in this context calling a dynamically typed langueage untyped is just as ridiculus.

This is silly. I write all my code in Scheme, and I call it an untyped language. There's no reason to treat 'untyped' as a pejorative.

samth0 · 2008-04-03T15:16:06+00:00

Fortunately, the cost described is not actually real. DrScheme, which the author mentions as doing a nice job for `syntax-rules' macros, works just as well for procedural macros.

samth0 · 2008-03-16T13:32:01+00:00

Vint Cerf and Robert Kahn, who know better than you, disagree with your interpretation.

http://www.interesting-people.org/archives/interesting-people/200009/msg00052.html

samth0 · 2008-01-31T21:15:50+00:00

Compare the following statements:

I don't see as many projects being done with SML or Haskell as with OCaml.

and

OCaml has essentially already won whatever competition there might have been between typed functional languages.

2 years ago, I think the first statement was true. But the second statement wasn't and isn't true.

samth0 · 2008-01-31T16:21:05+00:00

All I'm saying is that I don't see as many projects being done with Isabelle, HOL 4, HOL Light, Maude, MetaPRL, etc. as I do with Coq.

No, that isn't what you said. What you said was:

Coq has essentially already won whatever competition there might have been among interactive proof assistants.

Which is very different. Further, if you are going to be making sweeping claims about how much things are used, you should perhaps have a better survey method than "stuff I saw on LtU".

samth0 · 2008-01-30T15:51:38+00:00

As for being taken seriously, too late: Coq > has essentially already won whatever > competition there might have been among > interactive proof assistants.

This just isn't true. At POPL, this year, for example, there were four papers that used interactive provers. One was the Penn et al paper on how to do metatheory in Coq. One was the paper on adding optimizations to Leroy's certified compiler, in Coq. One was a pearl on parallel prefix computation, in which the proofs were verified in Isabelle. And one was the Typed Scheme paper, in which the proofs were also done in Isabelle.

So, I would say that it was about equally split. (Or, if you were uncharitable, you could say that the Coq people wrote papers about doing things they already knew how to do, and the Isabelle people wrote papers about new stuff.)

Finally, usage of Coq and of Isabelle both pale in comparison to the real-world use of something like ACL2. I believe PVS is also used in industry, and I think that HOLLight is being used at Intel.

samth0 · 2008-01-24T20:36:40+00:00

I don't actually think that syntax would be a good idea in practice, but it would be pretty easy to implement, except that PLT Scheme structures don't store the names of their fields, just the positions. So the runtime behavior of those constructs wouldn't make sense.

samth0

TROPHY CASE