Eston by mikedidthis

Fastidious Elegance

My name is Aaron Hsu, and I'm a computer scientist. I'm changing the way people look at computing and programming languages, what they can do with them, and how they do it.

Co-dfns Patreon Archives
RSS Email Github Youtube Patreon
Aaron W. Hsu

Playing with Isar

Handwritten versions: Pg. 1, Pg. 2, Pg. 3. Lately I have been playing with the Isabelle proof assistant, and I really like what I have been seeing. Isabelle has a lot of automation, and that is sort of one of my basic prerequisites when investigating proof systems. Isabelle has impressed

formalism isabelle isar proofs
6 years ago