Why Scientists Don’t Write Poetry

A pillow’s softness, from how it behaves:
To forces it reacts yet it conforms.
The patient repitition of a wave,
Transforming an atom from form to form.
How everything existing had begun,
Matter from matter moving fast away.
How everything is hidden in the sum
Of amplitudes of all the different ways.
Yet all the things I do ’till now express
Are mere fragments of a deeper core.
How would I love to faithfully address
The full wonders with all of their galore.
Yet when I try those feelings to compose
My poetry is hightened into prose.

Advertisements

Propositions as types in Foundations to Constructive Analysis

I was reading Foundations of Constructive Analysis by Errett Bishop, and I came across this intersting passage:

It is not strictly correct to say that a real number is an element of . An element of consists of a real number and a positive integer , such that , because an element of is not presented until both and are given. One and the same real number can be associated with two distinct (but equal) elements of . Nevertheless we shall continue to refer loosely to a positive real number . On those occasions when we need to refer to an for which , we shall take the position that it was there implicitly all along.

In other words, the proposition really stands for the type
of all with . Bishop does not appear to be aware of the
propositions-as-types interpretation in this book, but he uses it implicitly.