> Excellent, Colin! Yeah, if you're not getting strange bugs, you should
> conclude this.
This seems to be the case: I've been working through the Tutorial, and only
receiving the returns printed there.
> > What are you using HOL Light in order to do?
>
> I'd like to code up an early auction theory result due to Vickrey
> as a worked example for a PhD workshop I'm giving next month.
>
> Sounds really cool! Feel free to explain to us how proof assistants
> are going to help out with Economics.
This is exactly what I'm trying to understand. The obvious answer (or,
perhaps, SPEC) is "they'll help in the same way that the help in mathematics
more generally".
More specifically, as you've noted, social choice (e.g. Arrow's theorem) has
had most of the attention so far due to the discrete maths involved. Auction
theory is two steps away, so should also largely use techniques that are quite
amenable to formalisation.
Beyond this, I had started looking at HOL due to John's use of it at Intel:
economists use econometric packages, and finance houses use trading or risk
management packages that may contain a lot of infelicities - JP Morgan, for
example, has blamed their recent 'London Whale' trading losses on change in
their VaR ('value at risk') model.
> So you're the chairman of the
> Mathematical Finance Department of Economics University of Birmingham?
I'm the programme director for the MSc in Mathematical Finance, which is shared
between Economics and Mathematics. I'm an economist by training, but became
interested in ATP/ITP through my co-author, Manfred Kerber, in Computer Science
in Birmingham.
> I downloaded your paper
> http://www.springerlink.com/content/e47110g182480115/fulltext.pdf from
> your web page http://www.socscistaff.bham.ac.uk/rowat/ It looks
> interesting. How does Theorema compare to HOL Light?
Manfred and Wolfgang did the Theorema coding: Wolfgang is one of its
developers, and is currently in the process of re-implementing it.
The most obvious superficial difference is that Theorema uses the Mathematica
UI. Thus, it is 'prettier', and can read more naturally, but requires
Mathematica. Beyond this, Theorema differs from HOL in terms of its
strictness: external - possibly incorrect - theorems can be asserted rather
than building only from a small, established ruleset; the input language is
untyped.
Best,
Colin
------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
