Magos Logis Logan @jmw150@qoto.org

Proofs about the correctness of C code are now much easier. There is a software tool chain using "Verifiable C" to make systems safer.

Here is a tutorial on it, and general proof code writing. It is fully verified in Coq.

https://softwarefoundations.cis.upenn.edu/

Maybe 100 years ago mathematicians could hide in ivory towers and treat the subject like a liberal art. But in 2021 engineers are right at the gate.

Engineers want more algebras for their intricate software, more analysis for their haptic feedback systems, more topology and algebraic geometry for their robots and artificial intelligence systems.

If mathematicians do not publish about it, engineers will publish. Where mathematicians refuse to be rigorous, engineers and logicians will invent languages that automate writing proofs.

It is the end of an era. It is like seeing the Catholic religion split into the multitude of other Christian religions.

You are a cyborg.

Take good care of yourself by keeping your software bug free and up to date.

What even IS intelligence?

Knowing optimizations in a space is just mathematical knowledge. You don't have to be intelligent to pretty much utilize everything that would count as intelligence.

So what could it be in 50 years? Possibly ownership of GPU cores and the latest and greatest optimization software.

Have to say I am pretty fond of systems science, particularly software engineering.

Programs are these formal structures. They do not rust or anything like that. But they still age in a way that all complex systems age.

One such consequence of this is that systems with a hardy design can last pretty much forever. There is a lot of "brown field" and a bunch of time is spent rebuilding especially important systems out of stronger logic.

But two areas that software seems to change, even in such bullet proof systems, is security problems and new hardware. Interfacing can mitigate upkeep costs from hardware growth. But security issues tend to cause rewrites. What fixes security upkeep requirements are small edge cases of mathematical purity. But I think most systems can never be so clean.

I recommend this reading list. There are a lot of great topics in here for a budding analytic philosopher.

https://fuckyeahlogical.tumblr.com/post/128964910533/analytic-philosophy-reading-list-for-the-self

So good. lol

https://en.wikipedia.org/wiki/Boolean_Pythagorean_triples_problem

Anybody here interested in mathematical logic?

A brilliant class by Dr. Favonia on type theory that needs more attention.

https://youtube.com/playlist?list=PL0OBHndHAAZrGQEkOZGyJu7S7KudAJ8M9

I really like Wolfram's theory of physics. It is easy to understand. At its core it is a bunch of graph theory with hints of everything else in the universe.

But I am biased because I am also a language designer, and we are both math literate. So I think in a lot of the same ways he does.

https://www.wolframphysics.org/

I am having a great time with calculus of computation. It reads like a math logic book, but there is a solid proof system that comes as a companion to it.

http://theory.stanford.edu/~arbrad/pivc/book.html

Type systems are pretty great. I am fond of these compilers

http://theory.stanford.edu/~arbrad/pivc/download/index.html

https://compcert.org/

Some great stuff.

https://llvm.org/docs/tutorial/index.html

https://purpl.cs.purdue.edu/

Purdue, and others are also trying out "Software 2.0". The idea is that programmers design a nice solid type system, proof code if you will. Underneath this are many machine learning algorithms to accomplish the difficult task of implementation.

Get it while its hot. Mathematical logic is a common element of compiler and formal language design.

https://engineering.purdue.edu/~xqiu/ece663/

A machine learning course that is more rigorous than average while still being not purely theoretical. Partake in the story of the world my friends, or whatever Descartes said.

https://engineering.purdue.edu/ChanGroup/ECE595/project.html