A simple way to write this specification is to describe an environment of the program which reacts to a single event: the printing of the message “Hello world!” on the terminal. The specification of this program is very straightforward: the program only prints “Hello world!” and quits (here the specification is as long as the program itself, but this is not always the case). This should display Hello world! on the terminal. We compile and run this file: ocamlbuild main.native -use-ocamlfind -package io-system To compile the hello_world program we add: Definition main := Extraction.launch hello_world. The command line arguments are given in the list of strings argv, but not used here. The return type is C.t System.effect unit, which means this is a impure computation with System effects and returning a value of type unit. We load some libraries and write the hello_world program by calling the System.log function. You can now write the Hello World: Require Import .ĭefinition hello_world (argv : list LString.t) : C.t System.effect unit := Using OPAM for Coq, install the package coq-io-system: opam repo add coq-released This technique was popularized by the Haskell programming language. However, we can still encode inputs-outputs by defining a monad. This constraint is there to preserve the logical consistency of the system. This means that no effects can be done, in particular no inputs-outputs. In Coq this is more complicated because the language is purely functional. The Hello World program exists in almost every languages, including in White Space.
COQ TUTORIAL HOW TO
We will explain how to compile, run, and certify interactive programs in Coq. We will present the classic Hello World program in Coq.
0 kommentar(er)
