dragonwasrobot

"[…] the tools we are trying to use and the language or notation we are using to express or record our thoughts, are the major factors determining what we can think or express at all!"

“If you detect a needlessly complex style when you read, look for characters and actions so that you can unravel for yourself the complexity the writer needlessly inflicted on you.” – Joseph M.

“We are our choices.” – Jean-Paul Sartre 1.

“All for one and one for all, united we stand divided we fall.” – Alexandre Dumas, The Three Musketeers 1.

“‘Begin at the beginning’, the King said, very gravely, ‘and go on till you come to the end: then stop.’” – Lewis Carroll, Alice in Wonderland 1.

“One chord is fine.

“The trick, William Potter, is not minding that it hurts.” – Robert Bolt, Lawrence of Arabia (1962) 1.

1.

1.

“It might be worth-while to point out that the purpose of abstracting is not to be vague, but to create a new semantic level in which one can be absolutely precise” – Edsger W.

“The poet doesn’t invent.

1.

1.

1.

1.

1.

“What makes the desert beautiful,” said the little prince, “is that somewhere it hides a well…" – Antoine de Saint-Expuéry, The Little Prince 1.

“Beware of bugs in the above code; I have only proved it correct, not tried it.” – Donald Knuth Introduction In this post, we give a short primer on interactive theorem proving in the [Coq Proof Assistant (or simply, Coq) with the guiding example of natur…