Our great sponsors
-
-
SurveyJS
Open-Source JSON Form Builder to Create Dynamic Forms Right in Your App. With SurveyJS form UI libraries, you can build and style forms in a fully-integrated drag & drop form builder, render them in your JS app, and store form submission data in any backend, inc. PHP, ASP.NET Core, and Node.js.
-
isabelle-lambda-calculus
A formal definition and verification of System F. To be extended to System Fc
With this new goal in mind, I again searched around and found a pure python library that could write the metadata, so I could replace subler and have a pure python plugin that could run on any operating system! I forked and cloned the repository (I already used git for my personal code) and got the changes done rather quickly. It worked well enough on the Linux NAS, so I shared my work in order for others to benefit from it. Knowing not much about programming and good code style, I basically just copy pasted the python library into the project and commited that. You can see the horror that is the PR here. Apparently I missed some stuff or there are differences in the metadata for different operating systems, so it never got merged (I also did not really care about it as it was working well enough for myself).
From now on I was on what I would call a typical open source trajectory. I used the Cycle.js framework to rewrite my frontend and in that process I hit some walls. I eventually figured that the error was on my side and that I was just missing some information to avoid the error. To spare others the hours of debugging I started to contribute small patches to the documentation. At the same time I also found some missing features that I voiced in GitHub issues.
I got more into theorem proving, i.e. using a programming language to write mathematical proofs and have them checked by a compiler. Step by step I am working on a machine checked proof of type safety of System Fc, the intermediate language of the Haskell compiler.