[TYPES] Grand Challenge Problems?

[Barry Jay]

On Jan 16, 2010, at 5:04 PM, Purush Iyer wrote:

 >If y'all can come up with a list of five to ten challenges I would 
appreciate it very much.


Hi Purush

Here is my suggestion for a grand challenge:

      Automate the Scientific Method

Many of us think of computers as logic machines: input is trivial so 
inference rules!
However, computers now have access to unbounded amounts of data from the 
net, sensor networks and other logical machines.
This *experience* of the world leads to inductive knowledge (think data 
mining) but best results combine this with deduction (logic) using the 
scientific method.
One way of meeting this grand challenge would be to discover some useful 
theory in astronomy or particle physics or biology,
much as automated theorem-proving  was promoted by the first proof of 
the four-colour theorem.
Such systems could then be used to analyse markets or legal systems, to 
discover web-services, etc.

Many of the components of such a system already exist, e.g. data miners 
and theorem-provers.
Also, object-oriented languages are able to incorporate experience while 
functional programming languages automate logic.
The challenge requires us to develop a programming paradigm that 
embraces both experience and logic.
One way of combining these uses our pattern calculus ( 
http://www.springer.com/computer/foundations/book/978-3-540-89184-0 )
Simple observations and hypotheses can be represented as cases built 
from a pattern and a result.
These can be combined within pattern-matching functions to produce 
complex hypotheses.
The ideas above have been elaborated in an informal essay (  
http://www-staff.it.uts.edu.au/~cbj/Publications/psm.pdf  )

Barry Jay