From b51c53eded82eb7fad53b11d3079bd48b16f6ab8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Marko=20Grdini=C4=87?= Date: Mon, 6 Jan 2020 12:50:19 +0100 Subject: [PATCH] "11:05am. I am still deep in thought. I've internalized most of my motivation, but I just have that last 10% or so left. Let me review. I think it really is okay to lose hope in math at this point. Mainstream math is pretty much an enemy - their practitioners are merely posers who cannot even into numbers properly. And constructive math can be expected to be too difficult to give me any sort of insight into the problems that I am facing. While working in Coq or Agda, I've yet to do even a single proof that gave me insight I did not have before. The one time I did get insight was that first CFR proof where I switched to randomized testing and did in 5 days what I could not do in a month in Lean and Agda. So I think I am justified in leaving math aside based on practical experience. This was my mode of operation even before I learned formal theorem proving. Going forward, what is going to change is that I am not going to take any of the proofs seriously unless they are computable and I can do things like write randomized tests for them. But any proofs for ML are likely to be too trivial to really tell me anything of importance. https://stackoverflow.com/questions/59263530/how-to-prove-that-the-halving-function-over-positive-rationals-always-has-an-exi/59304233 Programs being proofs means that a program is half of a proof already. PLL explained to me how to satisfy the termination checker here, but is what he suggested really an improvement over the original? I am not sure. There is something suspicious about having to prove termination in some inexpressive sideways mechanism. But given how difficult even this simple thing would be, how could anybody prove anything of important for the CFR algorithm or anything other ML related? I have no idea. 11:15am. As a method of doing science, randomized testing really is the way to go. I am going to lean on it when it comes to doing paper proofs. Let me go to the next point. I think that as a method of getting better at AI, making better libraries and languages does make sense. Quantity is its own quality, and might turn out to be the primary driver not just for us weak humans, but in the post-Singularity era. Maybe the lofty height I'll reached in Spiral v0.2 might turn out to be an ideal. This was one of my motivations for starting work on the original Spiral. The next point. I've been thinking - suppose I have only six months or two years to live? What would I do? Would I live out the remaining days playing games or having fun? Or would I work on Spiral? I would definitely work on Spiral. I would regret not being able to witness the Singularity, but I would complete the language and hope it is helpful to whomever reaches it. The next point. As I've said, I really am no longer motivated by any specific thing like I was before. I already did the agent and the ML library, so that does not enthuse me anymore. Even though I said that I would work on Spiral, what I really want is to make gains in AI. Spiral is secondary in mind to this. AI. It all comes to AI. I want to exploit AI. I want to make its power my own. Accepting that there will be severe limits on how well ML algorithms can be understood is a gain in its own right. I will never be able to understand them as well as regular programs, but processes will have their own way of handling. 11:25am. I need to fire up my competitive spirit once more. My competition are ultimately Pythonlings, and a bunch of posers who can't even bear to deal in actual numbers and constantly make stuff out of thin air. 11:30am. Forget what came before. Forget the past mistakes. Do it harder, faster, more powerfully next time. 11:35am. Since the best way to get better at the whole is to get better at the basics, I really do need to level up that one last time by completing Spiral v0.2. But what will really keep me going is the resurrection of my dreams. They will give me the strength to keep fighting. 11:40am. Can I really be the best in the world, can I really defeat them by going to Python? Of course not. You don't get to be the best by accepting limitations that can be avoided. Doing more and not cutting corners, really is always better than taking the easy way. I am not really creating a language here, but my own power that will sustain me. 11:45am. It is not really that I am going to be relying on the others to come up with all the innovations. I had have my own ideas. But after 2018, I suffered a loss faith in just what exactly can I elucidate about them. If I change my mindset from wanting to formally prove things about them, to testing them is a really big arena, maybe I could accomplish something. ... Yeah, that is right. I made that agent, but then got peeved that once I increased the sequence length, the performance of NNs just fell of a cliff. I had it in my mind that I had to make a GPU library from the onset. I had it in my mind what needed to work, and got disillusioned when my experiments rather than clearing up the ideas only created ambiguity. I just had no idea how to deal with this. 11:50am. It became a wound that I've been carrying all this time. It is time that it heals. 11:55am. I am going to stop here for breakfast. I think it might be fine that for the first time in 5 years, I take an extended break for a week or so just to stoke this fire. 12:45pm. Done with breakfast. Let me just rest for a while. Yeah, I cannot accept formal theorem proving as a means of understanding. Suppose you have some program and you want to understand it - formal theorem proving requires writing a more complicated program in order to encapsulate that. This really a problem. Because if you do not understand the original thing, you won't be able to write the proof either. And if you understand the original thing then actually proving things about it is superfluous. As a method of generating understanding, FTP really has much to be desired." --- The Spiral Language v0.2/Script1.fsx | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/The Spiral Language v0.2/Script1.fsx b/The Spiral Language v0.2/Script1.fsx index e02abfc9b..5f282702b 100644 --- a/The Spiral Language v0.2/Script1.fsx +++ b/The Spiral Language v0.2/Script1.fsx @@ -1 +1 @@ - + \ No newline at end of file