What running and type theory means.

Well, welcome, I guess. Not that I expect readership. But I do have an expectation of personal growth and understanding. I do expect some sort of fuller comprehension, through exposition, of who I am, what I do, and perhaps most importantly why I do it. The topics will not be limited to running, nor type theory. Especially in the coming months. I have a whole plate of personal topics that I want to write about. There is no security in this medium, no privacy, so I am sort of putting myself out on the line. What are these topics I wish to cover, how do I identify myself, and what is currently on my plate that I am hoping to improve, change, or eliminate through this place?

I am a runner. Which seems counter-indicated because most people who know me also would point out that I am a smoker. This latter tidbit is something I hope to change soon. Tomorrow, at latest count. I point out that I am in fact a runner first and foremost because that is how I want people to see me. The smoking bit, well, that does not play as well in the hubris department. I am a marathon runner and I hope to keep this up for a very long time. Identifying myself as a runner is not particularly easy under such a dichotomy. Yet, it is a much more ... inspiring label than smoker. Quittng smoking is not easy, and it a if I lose a friend (of sorts) every time I do it. I have searched out support, answered all of the questions, and I suppose accepted the fact that I do need to quit. I would rather not have the qualified label of
runner who smokes, but simply runner.

I am also a type theorist. Type theory in this case being the study of types (collections of objects with a method by which we can tell if an element is in that collection or not. Natural numbers for instance.) as a foundation of logic, mathematics, and in particular to my own work, the field in the science of computation and programming languages. One of my short comings is being able to explain the complex and difficult concepts of computer science and in particular my own research into using type theory as a tool for formally verified software, formal verification. What I hope to post here are expositions of type theory, some are my research, some are topics from the foundations of the field I find interesting, some are simply things I am trying to find a way to explain. Corrections, additions, or constructive criticisms are always welcome.

There are many other things I am trying to improve about myself. My work ethic. Understanding my motivation for my work. My communications. My hobbies (which are more than just running). I do hope this forum, forum of one really, will be a tool I can use to start to make some of those improvements. The fact that it is a public forum gives a certain obligation beyond a personal statement. A responsibility to the reader to make good on what I say.