2/18/2023 0 Comments Coq tutorial![]() ![]() v Coq file in Spacemacs, Coq mode should be activated. The first three chapters - Basics, Induction, and Lists - will give you all you need to start being productive. Software Foundations is the best place to start getting your feet wet. Perhaps I’ll do another post about all the editors I use daily - Vim, Sublime, Atom, and Spacemacs - (I’m a mongrel, I know), but for now, I’ll just direct you to some Spacemacs resources. Make sure that the Coq layer activates upon opening a. The Coq integration is a Spacemacs ‘layer’, which is a set of configurations for a specific task. If you’re coming from vim, Spacemacs is a little obnoxious to get set up, though. With company-coq and spacemacs-coq layers, there’s not much more you could ask for. I haven’t tried the default CoqIDE or Coquille in vim, but Emacs’ Coq support is pretty great. I’d heard good things about using Emacs + Proof General for Coq, so I started using Spacemacs, which combines vim’s editing modes and keybindings with Emacs’. This is the first in a series of posts on approaching Coq and formal verification as a complete beginner. I couldn’t fit Adam Chlipala’s FRAP (Formal Reasoning About Programs) into my schedule, but I didn’t want to miss out on Zeldovich and Kaashoek’s PoCS class because it seemed more practical in nature. I’ve been quite curious about the field of formal verification since I first learned about it last semester. The goal of this class is to write the spec, implementation, and proofs for a formally verified RAID filesystem in Coq, then generate Haskell code from it. ![]() It focuses on formal verification of computer systems using Coq, a language for mechanical theorem proving. This class has been offered in various forms over the years, but this iteration is quite different. I’m currently taking the Fall 2017 iteration of 6.826, Principles of Computer Systems. ![]()
0 Comments
Leave a Reply. |
AuthorWrite something about yourself. No need to be fancy, just an overview. ArchivesCategories |