newsBooleanAlgebrasIntro2 - News

 
 

New Shift

Item posted by Daniel Wyckoff <deluger> on Fri 11 Dec 2020 09:08:54 PM UTC.

Partial algebras will still be the math focal point of this
project, because it's ready to go, but there's lots of more important general algebraic math that has to be done on pencil and paper for society's sake, as I hope that financial alchemists will donate a couple thou anonymously to my checking to cover a new computer, as my online laptop uses proprietary WiFi drivers that glitch at too much math, and my last cheapie offline computer broke recently, and I just can't afford to put too much money in this.  So, I won't be committing regularly for the next year or so, as I work out important math on paper for the computer science and technological aspect of this project. 

The good news is that the overall focal point of this project (Coq) will shift towards certification of embedded devices.  I'll use the downtime to read up on using Coq to certify Verifiable C with CompCert, and this direction will be more profitable to me and industry.  The great thing about universal algebra is that it can all be used to certify electronics one specification at a time.  There's just a big layer of government and industry that hides the interface between math and CS.  The simple chain is, write embedded device code in C, extract Coq program from C code with CompCert, choose specifications that you want to guard against in your electronics, program these in Coq, and prove them using general CS and math libraries like bool2 that involve natural structures in CS.

So, I'm still a lifer Coq-hacker, but on this 44th year of my life, I'll be dusting off the embers of proprietary drivers and bad technology with more practical transcendent forms of formalization. 

No Alpha Release this year, as there's still a key proof that has to be done for it to be better than last year's.  But, I've updated to Coq 8.9.0, etc.

Back to the top

Powered by Savane 3.15-e6e5.
Corresponding source code