amautertt · HackerTrans

vor 5 Jahrendiscuss

Aaron Schwartz died for nothing. Ortiz is having an upward legal and political career, while an young and inspiring tech activist died. It didn't even push the envelope on free/open access science journals.

amautertt

vor 5 Jahrendiscuss

Maybe type theory is good to know! I would like to see cutting edge NN libraries for Coq or Lean or Optimization ecosystem like Scipy or Scikit for Agda.

You develop your algorithm and you prove a bunch of theorems about it at the same time, incredibly difficult but totally wild!

There's some scattered projects like this https://github.com/OUPL/MLCert

amautertt

vor 5 Jahrendiscuss

If you are already familiar with Coq or even Ocaml/Haskell style programming.

I really believe, the volume 3 of SF series is a more polished and more approachable book.

https://softwarefoundations.cis.upenn.edu/vfa-current/index....

I am halfway through the first book (doing ALL exercises), I hope by next year end I would really like to finish vol 3.

This Isabelle books seems to cover more ground though.

amautertt

vor 5 Jahrendiscuss

I am further along in the journey, I have been learning formal verification/type theory and logic on my own.

I think these two are excellent books, SF : Logical Foundations for the basics, SF: Verified Functional Algorithms.

Unfortunately there is no royal road in type theory. This subject is incredibly demanding yet satisfying.

Software foundations are excellent books to read even if you aren't interested in verification/program proof.

comments