I agree that this is one of the best books that is (freely!) available from one of the most respected researchers of the area.
To me, Curry-Howard duality is one of the most intriguing aspects of type theory, but it requires a lot of meditation and getting used to before one can productively think about it.
Sophisticated type theory is obviously a very important stepping stone to develop provably correct programs, but it may be one of the crucial ingredients to generate new programs automatically, and therefore to self-modifying AI. An interesting (but not the first) paper in this direction is:
Maybe it’s just me, but I found the paper a total fail. Impatient readers should skip to sections 5.1 and 5.2 right away. Basically, the authors are trying to “evolve” simple functions by combining and recombining typed terms. First they “evolve” boolean-xor, sum-of-list and product-of-list, tweaking the “evolution” parameters until they get the right answer. Then they attempt to “evolve” increment-all-elements-of-list-by-one and fail.
Results like this are why I left computer science and started programming for money.
I agree that this is one of the best books that is (freely!) available from one of the most respected researchers of the area.
To me, Curry-Howard duality is one of the most intriguing aspects of type theory, but it requires a lot of meditation and getting used to before one can productively think about it.
Sophisticated type theory is obviously a very important stepping stone to develop provably correct programs, but it may be one of the crucial ingredients to generate new programs automatically, and therefore to self-modifying AI. An interesting (but not the first) paper in this direction is:
http://www.site.uottawa.ca/~afelty/dist/gecco08.pdf
which utilizes the System F and the C-H-correspondence to achieve a reasonable performance in program-generation in simple limited cases.
Maybe it’s just me, but I found the paper a total fail. Impatient readers should skip to sections 5.1 and 5.2 right away. Basically, the authors are trying to “evolve” simple functions by combining and recombining typed terms. First they “evolve” boolean-xor, sum-of-list and product-of-list, tweaking the “evolution” parameters until they get the right answer. Then they attempt to “evolve” increment-all-elements-of-list-by-one and fail.
Results like this are why I left computer science and started programming for money.
Which is what you would have had to do anyway if you’d stayed in computer science. So, good call.