Our great sponsors
-
> For more information about the technical side of the blog, and how you can contribute to it, please visit the mathematics-and-computation repository at GitHub.
-
F* is also a very cool project, though not technically a proof assistant.
-
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.
-
Regarding which proof assistant to devote time to, it’s a hard choice. But I think getting exposure to any of them is good, it’s kind of like programming languages - they’re all based on a similar core idea with small variations. It seems to me like Coq is the most popular, Lean is the ‘new kid on the block’ with a big corporate backer, and Isabelle has been used on some real-world C programs such as the sel4 OS kernel.
Related posts
- Is there a formally-proven real-time language/computing env. or operating system?
- From L3 to seL4 what have we learnt in 20 years of L4 microkernels? [video]
- On the Costs of Syscalls
- How to write TEE/Trusted OS for ARM microcontrollers?
- Simulation: KI-Drohne der US Air Force eliminiert Operator für Punktemaximierung