David Tagatac, M.S.

Proving Program Correctness via Type Checking

2011-05-25T15:42:00.002-04:00

(Type checking):(Programs)::(Dimensional analysis):(Theorems)

In studying OCaml at the University of Maryland, I have recently become very attuned to the parallels between type checking and dimensional analysis. In the same way that dimensional analysis is an "orthogonal" way of reasoning about mathematical and physical theorems, type checking is "orthogonal" to the program. I use the word "orthogonal" here to mean loosely that the two methods are independent of each other (i.e. dimensional analysis is "orthogonal" to proof by induction for example).

Proving Theorems Using Only Dimensional Analysis

Immediately then, I began to think about ways that dimensional analysis has been used to prove mathematical and physical theorems from start to finish. See, for example, Proof of the Pythagorean theorem.

Proving Program Correctness Using Only Type Checking?

The obvious next question. I have a feeling that this can be done, but I still have a lot of reading to do :) Stay tuned. Comments are welcome.

Currently reading: Foster, J.S., Johnson, R., Kodumal, J., Aiken, A.: Flow-Insensitive Type Qualifiers. Trans. on Programming Languages and Systems. 28(6), 1035–1087 (2006)

DC Bloggers Meetup

2009-05-21T16:23:00.000-04:00

Well, after attending a DC Bloggers Meetup, I feel compelled (from within and by the other attendees) to start blogging again. I'll start with a blogroll of the other attendees:

http://jadxia.livejournal.com/ -- a retired specialty performance artist, novelist, and internet editorialist
http://blogpharm.com -- a pharmacy related blog
http://swordandthescript.blogspot.com/ -- a tech PR guy full-time, infantry officer part-time, Pats fan all the time, political news junkie anytime
http://notionscapital.com -- commentary and smart remarks on news, events, and culture
http://tbarbeeweb.com/theweblady -- blog devoted to helping small business owners utilize software and technology they already possess

It was fun to talk tech and blogging with other enthusiasts. If you're a blogger, come check it out: http://www.meetup.com/dcbloggers/

How to exclude Eclipse/Aptana preview views from Google Analytics results

2008-12-13T05:31:00.000-05:00

For those of you who use Aptana within the Eclipse IDE to edit your websites, you may have noticed that previewing your site using the Built-in Preview Server (bound to the Jaxer Internal Server) introduces new pages to the content report in Google Analytics. This appears to be due to the Jaxer server setting up relative paths based on the project path within Eclipse.

I believe that I have a way to fix this via a Google Analytics filter. First, check the details for your Built-in Preview Server in Eclipse for the Host field. Mine was set by default to "127.0.0.1". (You can also check this value from the Content section of your Google Analytics report - Just click on the extraneous page(s) and select "Hostname" from the Dimensions pulldown menu. Now, set up a custom Exclude filter for your Google Analytics profile, select "Hostname" as the Filter Field, and set the Filter Pattern to the hostname you found in Eclipse above. Note that that field accepts regular expressions, so be sure to use the regular expression characters properly. For my hostname of 127.0.0.1, I entered "^127\.0\.0\.1$":

Unfortunately, Google Analytics doesn't refilter old data, so I will have to wait a couple days to see if the filter is working properly, so stay tuned and I'll post back with the verdict. In the meantime, if anyone sees a flaw in my method, please comment :)

*UPDATE 12/18/08*
It looks like that filter does the trick. No new hits to the "phantom" Jaxer pages :-D