A bit about lecture 5.

Dress shows arrogance |

I wonder if Justin Curry would go to a job interview in that Club Med outfit. Students are paying customers ( and a pool of cheap labor for lucrative research deals the university makes ) deserving respect from teaching staff.

Formal number theory ( as in M381 ) |

Justin talks about Typographic Number Theory, ( formal number theory in M381 ). For example $$\forall x ( \neg x = \mathbf{0} ( \exists y x = y') )$$ can be interpreted as

"Every x that is not equal to 0 is the successor of some y."Leibniz was the first to propose a formal language for number theory. He asked whether it was true that an algorithm could decide if a statement in number theory was true. - Although in M381 this question is answered negatively that does not mean computers can not play a role in proving mathematical propositions. There is an abundance of ( open source ) software for proving theorems.

( Not in video: ) Isabelle a formal proof theory assistant has been used in testing an operating system kernel written in C and assembler. It not only verified that the spec was implemented correctly but it also discovered hundreds (...) of programming and design (...) errors which were not found by traditional testing methods.

Previous posts on the series:

- Lecture 1

- Lecture 2

- Lecture 3

- Lecture 4

## No comments:

## Post a Comment