Show newer

@niconiconi Could do a pattern match, replace it with clean splines, and then do another jpeg. :ablobblewobble:

Well I woke up raging against the smallness of elementary number theory, and wanting to listen to Infected Mushroom. That coffee must have been strong. :blobfoxcofeglare:

youtu.be/bnsUkE8i0tU

Are you a cat-top-phys-logicist?

5 way Rosetta stone of physics-topology-categories-logic-computation, for the luls.

arxiv.org/abs/0903.0340

"a general science of systems and processes" is, admittedly, not very catchy though.

@freemo Okay. The stuff on your pages and posts, is pre-college level for some people though. So it sounds especially odd.

I would change that to just mathematics in general. It sounds less obnoxious to me. As a professional, hearing "research" math, "theoretical" math, or "advanced" math, feels like either putting on airs, or other-ing. 😅

@freemo when you say advanced mathematics, what do you mean?

Optimistic rant 

@zpartacoos Machine learning and program synthesis are related fields, but not completely the same. Program synthesis is also not completely separate from FM either.

It is an intro graduate course, so it is a good place to start from scratch. But to brush up, some survey research papers would be better.

Program synthesis (as of 2017)
microsoft.com/en-us/research/w

Also FM and ML being used together (this April)
arxiv.org/pdf/2104.02466.pdf

Happy I took time to study some topology this summer. Algebraic topology is all the things I hoped for.

I am not sure I quite get it yet, but a topology of something seems to be usable as a definition to a lot of geometric notions. All of analysis work seems to just be applied topology. And with homotopy type theory, all sorts of data science, machine learning, and statistics work could be made easier and more precise.

Cubical type theory, (a computation friendly HOTT) is not even 2 years old. It is going to be big.

cs.cmu.edu/~cangiuli/thesis/th

Optimistic rant 

@zpartacoos It is a new decade. There have been some serious breakthroughs.

The common programmer might have a tough time competing with data assisted program synthesis, and programmers that can wield the dependent types to control that synthesis.

Excellent course, the future of solid software looks bright.

frap.csail.mit.edu/main

"What's it all about?

Briefly, this course is about an approach to bringing software engineering up to speed with more traditional engineering disciplines, providing a mathematical foundation for rigorous analysis of realistic computer systems. As civil engineers apply their mathematical canon to reach high certainty that bridges will not fall down, the software engineer should apply a different canon to argue that programs behave properly. As other engineering disciplines have their computer-aided-design tools, computer science has proof assistants, IDEs for logical arguments. We will learn how to apply these tools to certify that programs behave as expected."

There is so much research to do.

Including people doing research outside of academia I would approximate there are about 25 million researchers worldwide. Not sure what it was 100 years ago, but I only see that number growing.

richardprice.io/post/128555616

@AgathaSorceress Arch has a toxic culture and should be avoided anyway.

@lupyuen odd if the Chinese government doesn't buy up most of this equipment for themselves.

@freemo it is more like a database.

Systems like Coq are more fun though I think. The standard library is proofs for a bunch of undergrad math like the dedikind cut construction of reals. Real numbers at your fingertips. 😁

@freemo could polish us.metamath.org from set theory

Or there are several systems in type theory.

Another day.. another 10 hours to dump into type theory studies.

For the logic gods.

Huh, that is kind of cool. Removing noise for physical sensors. It is like learning to see at a base level.

arxiv.org/pdf/2106.11936.pdf

Show older
Qoto Mastodon

QOTO: Question Others to Teach Ourselves
An inclusive, Academic Freedom, instance
All cultures welcome.
Hate speech and harassment strictly forbidden.