Re:Concrete Semantics with Isabelle/HOL
by itsphilos on Sunday February 28, 2021 @02:19AM
(#26291348)
I took a university class on said book last year, held by one of the authors Prof. Tobias Nipkow.
Its a fascinating introduction into general program semantics, formal analyses and proofs for program properties.
During the lecture I struggled somewhat as I didn‘t really have sufficient background knowledge for it to run smoothly.
But all the concepts are supported by, well, concrete examples which you can immediately try to solve in Isabelle. So I definitely recommend giving it a go!
It was an eye-opening experience for me, especially since I never really looked into formal program analysis.
Re:Concrete Semantics with Isabelle/HOL
by zaik on Sunday February 28, 2021 @03:11AM
(#26291596)
I am no expert, but Coq and Isabe
le "feel" very similar at first, but Isabelle seems to provide much more powerful tools for proof automation than Coq. Isar, Isabelle's proof language, tries to be close to natural language proofs which makes it more intuitive.
I really wish Coq had equally powerful automation tools and a more intuitive proof language, because it feels much more of a solid language and I really liked that the clear relation of types <-> statements, terms <-> proofs, type checking <-> proof verification; including the ability to print the raw proof terms of theorems.
Re:Concrete Semantics with Isabelle/HOL
by blewboarwastake on Sunday February 28, 2021 @12:41AM
(#26290974)
From the book's introduction:
Concrete?
• The book shows that a semantics is not a collection of abstract symbols on sheets of paper but formal text that can be checked and executed by the computer: Isabelle is also a programming environment and most of the definitions in the book are executable and can even be exported as programs in a number of (functional) programming languages. For a computer scientist, this is as concrete as it gets.
• Much of the book deals with concrete applications of semantics: compilers, type systems, program analysers.
• The predominant formalism in the book is operational semantics, the most concrete of the various forms of semantics.
Its a fascinating introduction into general program semantics, formal analyses and proofs for program properties. During the lecture I struggled somewhat as I didn‘t really have sufficient background knowledge for it to run smoothly. But all the concepts are supported by, well, concrete examples which you can immediately try to solve in Isabelle. So I definitely recommend giving it a go!
It was an eye-opening experience for me, especially since I never really looked into formal program analysis.
What's the difference between TLA+, Coq & Isabelle?
Is there one should I prefer over the other? Or do they individualy satisfy distinctive purposes?
I really wish Coq had equally powerful automation tools and a more intuitive proof language, because it feels much more of a solid language and I really liked that the clear relation of types <-> statements, terms <-> proofs, type checking <-> proof verification; including the ability to print the raw proof terms of theorems.
Concrete?
• The book shows that a semantics is not a collection of abstract symbols on sheets of paper but formal text that can be checked and executed by the computer: Isabelle is also a programming environment and most of the definitions in the book are executable and can even be exported as programs in a number of (functional) programming languages. For a computer scientist, this is as concrete as it gets.
• Much of the book deals with concrete applications of semantics: compilers, type systems, program analysers.
• The predominant formalism in the book is operational semantics, the most concrete of the various forms of semantics.
• Foundations are made of concrete.