-
-
InfluxDB
Power Real-Time Data Analytics at Scale. Get real-time insights from all types of time series data with InfluxDB. Ingest, query, and analyze billions of data points in real-time with unbounded cardinality.
-
Personally I treat Coq like an extension of my brain. Whenever I'm uncertain about something, I formalize it in Coq. I have a repository of proofs with GitHub Actions set up in such a way forbids me from pushing commits containing mathematical mistakes. I've formalized various aspects of category theory, type theory, domain theory, etc., and I've also verified a few programs, such as this sorting algorithm. Lately I've been experimenting with a few novel types of graphs, proving various properties about them with the aim of eventually developing a way to organize all of my data (files, notes, photos, passwords, etc.) in some kind of graph structure like that.
Check out Lean (https://leanprover-community.github.io/) if you want a theorem prover with a strong mathematics community. Or if you don't, Lean is cool.
I am currently working on implementing your second link: https://github.com/jvanbruegge/master-thesis
But I suspect that will improve (they're all very new projects). I'm also keeping an eye on Dafny which looks pretty neat and avoids the "oh sorry we don't support traits" issue.