> Curry-Howard executable version of the claim

I don't see how the code provided has any relation to the Curry-Howard correspondence, which is a statement relating types and proofs.

The original CH mapping, that is, "a proof is a program, the formula it proves is a type for the program" is quite hard to achieve because it tries to demonstrate that a particular statement is true. It is much easier to honestly fail in demonstrating that it is false.

Then why bother using Heroku at all? GitHub Pages supports Jekyll.

Good point. I hadn't seen / used github pages before, and it looks like they let you set up a custom domain so might be a comparable solution.

I use github pages with jekyll and I'm pretty satisfied with it.

I have an additional wrinkle - I have a jekyll plugin I wrote that I want to use, so I have to run jekyll on my own machine and then commit the plain html output to a separate repository. Once it was set up though it doesn't look much different though, just one extra step (running ./push_site_live.sh) after I'm done.

Another alternative is also just hosting directly off S3, which, combined with cloudfront, should eliminate any possibility of folding.

Because you can't use plugins (RSS, Read More, etc)

Sounds a bit like Fat Dog Exchange. Does anyone know what happened to that site?

Also similar to Hollywood Stock Exchange: http://en.wikipedia.org/wiki/Hollywood_Stock_Exchange

Hollywood Stock Exchange also holds a patent for the core principles behind prediction market games like these (http://www.google.ca/patents?id=n2sXAAAAEBAJ).

And the BBC's now defunct CelebDAQ

I tried to find out what happened to that site. Doesn't seem to be much info out there.

You could use yubnub or bunny1 to do this.

I think it was meant that the marginal cost function isn't continuous.