wisnesky

Hydra is a programming language that uses mathematical abstraction to model graphs within the language itself. It’s an open-source project spearheaded by Josh Shinavier, co-creator of Apache TinkerPop. In Josh’s own words: “In Hydra, programs are graphs, and graphs are programs.”

An open source project to search SQL code 'semantically': up to the meaning of parse trees. For example, searching for 'select from A,B' matches 'select from B,A'.

There is a partial solution to this problem: use formal methods such as symbolic logic and theorem proving to check the LLM output for correctness. We are launching a semantic validator for LLM-generated SQL code at sql.ai even now. (It checks for things like missing joins.) And others are using logic and math to create LLMs that don't hallucinate or have safety nets for hallucination, such as Symbolica. It is only when the LLM output doesn't have a correct answer that the technical issues become complicated.

Yes; categories extend traditional graphs with systems of equations. Hypergraphs extend traditional graphs by allowing edges to be between multiple nodes. Most operations on categories are formally undecidable because of the systems of equations; most operations on graphs/hypergraphs are decidable. This makes working with categorical databases a lot like doing computer algebra in e.g. Mathematica and provides a huge increase in expressive power (you can e.g. encode Turing machines with equations.)

Yes, at least with a strong enough arithmetic (such as Peano's), but that is usually more complicated; for example, you might have to create a Godel numbering or some other "deep embedding" to represent each set as a number. There's also so-called "reverse mathematics", which tries to determine the weakest axiom system capable of establishing a particular result.

A foundation for mathematics is any formalism sufficient to prove the results typically taken as axioms in practical mathematics. For example, in ZFC you can define numbers as sets in many different ways and prove that 1+1=2 for each of them - other foundations include higher order logic, topos theory, other set theories, etc.

Yes, although Dijkstra was interested in proving programs correct in general, not just in how lambda calculi correspond to logics correspond to categories (a proof technique for program correctness, among other things).

We've used Poly to prove results about functorial data migration.

Yes, in the sense that "math is programming paper instead of computers", being better at one translates to being better at the other. This intuition can even be made precise via the "Curry-Howard isomorphism", upon which "proof assistants" such as Coq are built.