I gave up on this goal before mid-year. One major setback was that the tutorial I was using taught you one thing, but then when you actually tried using the software it used a different syntax than what the tutorial taught. There was a whole other book on the syntax that’s actually used, so I started going through that. The main thing that caused me to abandon the goal, though, was that there was not a clear interface between the logic system and its implementation. The Isabelle mathematics libraries are built up as a bunch of files, and theories that depend on previous theories include the files that contain the previous theories. The problem is that, if you trace some mathematical theory to its roots through the included files, you find that some of the facts that the theory depends on are low-level ML statements rather than Isabelle statements. At a low level, Isabelle and ML are mixed together and there is no clear boundary between what is mathematics and what is programming implementation. This was driven home for me when I tried to prove some simple statement like 1000000000000+1000000000000=2000000000000 and found that Isabelle wasn’t able to prove it right off the bat like it can with machine-sized integer statements like 1+1=2. I’m sure the first statement is provable within the framework provided by Isabelle, but it was disappointing to see that Isabelle handled the two proofs differently even though mathematically they are equivalent. The original idea was for Isabelle to be an aid to mathematical proofs, but in the end it seems like it would be more of a hinderance. I came away from the experience with the belief that Isabelle is not yet ready for widespread use. To be fair, the author never claimed that it was, and at least one expert in proof assistants stated as much. I guess I had to see it for myself to believe it.
greenbreen's Life List
1. Translate the English Calculus wikibook into Spanish
2. Decide on a CAD program to learn
3. Practice Spanish everyday in 2013
How I did it: Ever since I found out that chemical hand warmers contain vermiculite, which I want to avoid for ethical reasons, I have been looking for a way to keep my hands from freezing when I ride to work on my bike in the winter here in Montana. Every commercial solution I looked at had some aspect that I didn't like. After looking at making my own chemical warmers, I finally decided on a battery-powered electric version. Here's … Read how I did it…
Since my last entry, the design of these handwarmers has changed considerably. I decided on an electric handwarmer. Thumbwarmer is really a better description. The only part of my hands that gets really cold when I’m wearing my mittens is the tips of my thumbs. I created a pair of thumbwarmers by sewing a coil of 30 gauge wirewrap wire inside of a “thumb cot” that I made. Then I wrapped the wire around some thicker wire and attached that to a battery holder, covering the wire with heat shrink tubing. The thicker wire is folded over on itself several times and sewn to the thumb cot to provide some strain relief. I tried them out under realistic conditions, and they did OK. The original design had the battery disconnectable from the cot, but in practice I found that the gloves would disconnect accidentally, so I removed the connectors and tied the cot directly to the battery. I also found that the warmers get hotter than is comfortable. That’s where the project is right now. I’ve ordered some switches and I plan to add them to the circuit to allow the warmers to be turned on and off as needed. I also need to add some redundancy because I found that the thin wires occassionally broke during testing. I may also want to add some test points to make it easier to diagnose problems with the warmers.
The idea is to improve my Spanish. I’ve tried learning on my own, but my Spanish really hasn’t improved much. I think part of the problem is a lack of sustained practice, and part of it is a lack of exposure to situations where I need to use Spanish. To address these issues I plan to sign onto conversationexchange.com or a similar site every day and spend at least half an hour chatting with the Spanish-speaking denizens there. At the end of the year, I will call this resolution a success if I have practiced Spanish in this way for at least 300 days of 2013 and I have accumulated at least 182.5 hours of time devoted in this way.