<p>this paper by Yves Bertot, Benjamin Gr´egoire, and Xavier Leroy builds an optimizing compiler for a C-like language based purely on the Coq specification.  some of this technology is apparently utilized in the <a href="http://compcert.inria.fr/" rel="nofollow noreferrer">CompCert C compiler</a>.</p>

<p><a href="http://gallium.inria.fr/~xleroy/publi/proofs_dataflow_optimizations.pdf" rel="nofollow noreferrer">A structured approach to proving compiler
optimizations based on dataflow analysis</a></p>

<p>it considers the correctness of two optimizations, constant propagation (CP) and common subexpression elimination (CSE), section 4. these optimizations are more advanced than those that are associated with the non Coq-based compiler(s) for the same language. see eg this <a href="http://compcert.inria.fr/compcert-C.html#perfs" rel="nofollow noreferrer">benchmark chart</a> compared to gcc. (the Coq-based compiler is presumably <em>slower</em> to compile although this is rarely mentioned!) </p>

<blockquote>
  <p>An original aspect of ConCert is that most of the compiler is written directly
  in the Coq specification language, in a purely functional style. The executable
  compiler is obtained by automatic extraction of Caml code from this specification.</p>
</blockquote>

<p>however at the end of the paper they do note that there are some compiler optimizations in real compilers that cant be modelled in their framework.</p>

<p>improved optimization is not the only element of consideration here, another aspect is that compiler optimization logic can be subject to subtle defects esp due to its complex nature. over the years gcc has been found to have bugs in its numerous optimization logic routines. eg <a href="https://stackoverflow.com/questions/83962/do-i-have-a-gcc-optimization-bug-or-a-c-code-problem">gcc bug?</a></p>

CC BY-SA 3.0
2013-02-06T20:23:54.233Z
2013-02-06T21:09:16.157Z
2017-05-23T12:40:09.333Z
vzn
<blockquote>
  <p>Can I prove certain properties (that are guaranteed to hold) for a
  program (e.g., a subroutine is non-entrant and can never call itself)
  that allow to perform optimizations that are not usually possible.</p>
</blockquote>

<p>It is equivalent to extending the typechecker to provide some properties of a program to the optimizer. I believe Tsuyoshi Ito is right and you may be little misguided about Coq. It is great tool for providing a bug-less compiler, but in the case you describe, it does not provide more power to the static analyses.</p>

<p>The only thing I can think about strengthening static analyses with Coq, is to equip your language with assertions containing some user-written proofs. -- If the compiler itself would be translated into a language including a feather for dynamic typechecking, and if the user-written proofs would be convertible to functions, then it would be possible to apply those functions as prerequired properties for some subtypings or optimizations. -- This indeed, would provide more power to the compiler.</p>

<p>However, as far I can see, it would be rather useful for strengthening subtyping. -- It is hard to make a programmer to know, what property in what place would be helpful for the optimizer.</p>

CC BY-SA 3.0
2013-05-19T16:05:25.037Z
2013-05-19T16:05:25.037Z
Number47
<p>I am interested in verified compilers formalized in Martin-Löf type theory, i.e. Coq/Agda. At the moment I’ve written a small toy example. Therewith I can prove that my optimizations are correct. For example that additions with zero can be eliminated, i.e. expressions like "x + 0".</p>

<p>Are there optimizations that are difficult to perform with a regular compiler, that would serve as a good example? Is it possible to prove certain properties of a program that allow optimizations that are not possible to perform with a regular compiler? (i.e. without the inference that is possible with a theorem prover)</p>

<p>I would be interested in ideas or examples and also references on the topic.</p>

<p>A related question:
<a href="https://cstheory.stackexchange.com/questions/10547/compiler-correctness-proofs/">Compiler correctness proofs</a> </p>

<p>edit:
As Tsuyoshi nicely put it in the comments:
I am looking for optimization techniques which are difficult to implement if a compiler is written in (say) C but easier to implement if a compiler is written in (say) Coq. As Agda compiles to C (via haskell) it is possible to do everything that is possible in Agda also in C. Probably the only benefit of theorem provers like Coq/Agda is that the compiler and the optimizations can be verified.</p>

<p>edit2:
As suggested by Vijay D I write what I've read so far.
I mainly focused on Xavier Leroy and the CompCert project at INRIA (there is a 80 pages paper that is a good read, I think).
A second interest was in the work of Anton Setzer on interactive programs. I though that perhaps his work could be used to prove properties about IO programs and bisimulation of IO programs. 
Thanks for mentioning Sewell. I've heard his talk "Tales from the jungle" at ICFP and read perhaps 2-3 of his papers. But I haven't specifically looked at his work and that of his coauthors.<br>
I did not yet find out where to start or look for papers on optimizing compilers; e.g., which optimizations would be interesting to look at in the setting of a verified compiler. </p>

CC BY-SA 3.0
2013-01-29T17:26:26.160Z
“Are there optimizations that are difficult to perform with a regular compiler”: Isn’t that impossible?  If I remove a proof of correctness from a verified compiler, I would get a regular compiler.  Therefore, anything that a verified compiler can do can be done also by a regular compiler.  The point of a verified compiler is that it _cannot_ perform an optimization which is incorrect.  (My knowledge about compilers and program verification is minimal.  Excuse me if I am missing the point.)
Tsuyoshi Ito
CC BY-SA 3.0
2013-01-29T18:40:40.810Z
@Tsuyoshi thank you for your comment. I meant: Can I prove certain properties (that are guaranteed to hold) for a program (e.g., a subroutine is non-entrant and can never call itself) that allow to perform optimizations that are not usually possible. Some invariants might be hard to verify for a program and perhaps these optimizations are not performed by commonly used compilers. But perhaps I am completely wrong.
mrsteve
CC BY-SA 3.0
2013-01-29T18:45:11.540Z
Are you talking about a compiler _written in_ Coq/Agda or a compiler _for_ Coq/Agda?  I thought that your question was about a compiler written in Coq/Agda, but then I do not think that a compiler written in Coq/Agda can prove any more properties about target programs than a compiler written in C.
Tsuyoshi Ito
CC BY-SA 3.0
2013-01-30T04:33:45.570Z
It would be good to add what you have read to the question. Are you familiar with work on verified compilation - that of Xavier Leroy, for example? Or that of Peter Sewell and collaborators?
Vijay D
CC BY-SA 3.0
2013-02-01T17:20:35.963Z
There are no such optimizations, unless you further restrict your question. In the extreme case the C compiler can secretly implement a theorem prover in its bowels (and most actually do it in a limited way). I think it is unclear what you mean by "regular compiler".
Andrej Bauer
CC BY-SA 3.0
2013-02-13T23:40:08.257Z
@didierc that's an interesting point. I don't have a background in theoretical computer science. At the moment, object oriented programs including inheritance, perhaps, seem to be too much. I guess (not sure), it should be possible to proof the equality between to imperative programs via bisimulation. Perhaps for while-languages like IMP, it should be okay. Then you could proof that after an particular optimization, the programs before and after optimizations are equal. Or not? I am just interested in imperative/oop languages. http://www.cs.ru.nl/B.Jacobs/CLG/JacobsCoalgebraIntro.pdf
mrsteve
CC BY-SA 3.0
2013-02-13T23:40:59.597Z
ps: there is a paper from anton setzer about oop programs in martin löf type theory.
mrsteve
CC BY-SA 3.0
2013-02-13T23:49:13.427Z
pps: ...  proof the equality between *two* imperative programs
mrsteve
CC BY-SA 3.0
2013-02-14T00:55:41.593Z
Thank you for the pointer and interesting question btw. I don't have much knowledge in theorical computer science either (lack of practice). Disregard my comment which wasn't very much in sync with your question it seems.
didierc
<reference-request><pl.programming-languages><type-theory><semantics><compilers>
Certified compiler and optimizations in Coq/Agda
mrsteve
# Certified compiler and optimizations in Coq/Agda

(Asked by: username_0 on 2013-01-29)

I am interested in verified compilers formalized in Martin-Löf type theory, i.e. Coq/Agda. At the moment I’ve written a small toy example. Therewith I can prove that my optimizations are correct. For example that additions with zero can be eliminated, i.e. expressions like "x + 0".

Are there optimizations that are difficult to perform with a regular compiler, that would serve as a good example? Is it possible to prove certain properties of a program that allow optimizations that are not possible to perform with a regular compiler? (i.e. without the inference that is possible with a theorem prover)

I would be interested in ideas or examples and also references on the topic.

A related question:
[Compiler correctness proofs](https://cstheory.stackexchange.com/questions/10547/compiler-correctness-proofs/)

edit:
As Tsuyoshi nicely put it in the comments:
I am looking for optimization techniques which are difficult to implement if a compiler is written in (say) C but easier to implement if a compiler is written in (say) Coq. As Agda compiles to C (via haskell) it is possible to do everything that is possible in Agda also in C. Probably the only benefit of theorem provers like Coq/Agda is that the compiler and the optimizations can be verified.

edit2:
As suggested by username_2 I write what I've read so far.
I mainly focused on Xavier Leroy and the CompCert project at INRIA (there is a 80 pages paper that is a good read, I think).
A second interest was in the work of Anton Setzer on interactive programs. I though that perhaps his work could be used to prove properties about IO programs and bisimulation of IO programs.
Thanks for mentioning Sewell. I've heard his talk "Tales from the jungle" at ICFP and read perhaps 2-3 of his papers. But I haven't specifically looked at his work and that of his coauthors.  
I did not yet find out where to start or look for papers on optimizing compilers; e.g., which optimizations would be interesting to look at in the setting of a verified compiler.

**Tags:** reference-request, pl.programming-languages, type-theory, semantics, compilers

> **Comments:**
> **username_1**: “Are there optimizations that are difficult to perform with a regular compiler”: Isn’t that impossible?  If I remove a proof of correctness from a verified compiler, I would get a regular compiler.  Therefore, anything that a verified compiler can do can be done also by a regular compiler.  The point of a verified compiler is that it _cannot_ perform an optimization which is incorrect.  (My knowledge about compilers and program verification is minimal.  Excuse me if I am missing the point.)  
> **username_0**: @Tsuyoshi thank you for your comment. I meant: Can I prove certain properties (that are guaranteed to hold) for a program (e.g., a subroutine is non-entrant and can never call itself) that allow to perform optimizations that are not usually possible. Some invariants might be hard to verify for a program and perhaps these optimizations are not performed by commonly used compilers. But perhaps I am completely wrong.  
> **username_1**: Are you talking about a compiler _written in_ Coq/Agda or a compiler _for_ Coq/Agda?  I thought that your question was about a compiler written in Coq/Agda, but then I do not think that a compiler written in Coq/Agda can prove any more properties about target programs than a compiler written in C.  
> **username_2**: It would be good to add what you have read to the question. Are you familiar with work on verified compilation - that of Xavier Leroy, for example? Or that of Peter Sewell and collaborators?  
> **username_3**: There are no such optimizations, unless you further restrict your question. In the extreme case the C compiler can secretly implement a theorem prover in its bowels (and most actually do it in a limited way). I think it is unclear what you mean by "regular compiler".  
> **username_0**: @username_4 that's an interesting point. I don't have a background in theoretical computer science. At the moment, object oriented programs including inheritance, perhaps, seem to be too much. I guess (not sure), it should be possible to proof the equality between to imperative programs via bisimulation. Perhaps for while-languages like IMP, it should be okay. Then you could proof that after an particular optimization, the programs before and after optimizations are equal. Or not? I am just interested in imperative/oop languages. http://www.cs.ru.nl/B.Jacobs/CLG/JacobsCoalgebraIntro.pdf  
> **username_0**: ps: there is a paper from anton setzer about oop programs in martin löf type theory.  
> **username_0**: pps: ...  proof the equality between *two* imperative programs  
> **username_4**: Thank you for the pointer and interesting question btw. I don't have much knowledge in theorical computer science either (lack of practice). Disregard my comment which wasn't very much in sync with your question it seems.  

---

## 2 answers

### Answer by username_5 on 2013-02-06. Score: 5

this paper by Yves Bertot, Benjamin Gr´egoire, and Xavier Leroy builds an optimizing compiler for a C-like language based purely on the Coq specification. some of this technology is apparently utilized in the [CompCert C compiler](http://compcert.inria.fr/).

[A structured approach to proving compiler
optimizations based on dataflow analysis](http://gallium.inria.fr/~xleroy/publi/proofs_dataflow_optimizations.pdf)

it considers the correctness of two optimizations, constant propagation (CP) and common subexpression elimination (CSE), section 4. these optimizations are more advanced than those that are associated with the non Coq-based compiler(s) for the same language. see eg this [benchmark chart](http://compcert.inria.fr/compcert-C.html#perfs) compared to gcc. (the Coq-based compiler is presumably *slower* to compile although this is rarely mentioned!)

> An original aspect of ConCert is that most of the compiler is written directly
> in the Coq specification language, in a purely functional style. The executable
> compiler is obtained by automatic extraction of Caml code from this specification.

however at the end of the paper they do note that there are some compiler optimizations in real compilers that cant be modelled in their framework.

improved optimization is not the only element of consideration here, another aspect is that compiler optimization logic can be subject to subtle defects esp due to its complex nature. over the years gcc has been found to have bugs in its numerous optimization logic routines. eg [gcc bug?](https://stackoverflow.com/questions/83962/do-i-have-a-gcc-optimization-bug-or-a-c-code-problem)


---

### Answer by username_6 on 2013-05-19. Score: 3

> Can I prove certain properties (that are guaranteed to hold) for a
> program (e.g., a subroutine is non-entrant and can never call itself)
> that allow to perform optimizations that are not usually possible.

It is equivalent to extending the typechecker to provide some properties of a program to the optimizer. I believe username_1 is right and you may be little misguided about Coq. It is great tool for providing a bug-less compiler, but in the case you describe, it does not provide more power to the static analyses.

The only thing I can think about strengthening static analyses with Coq, is to equip your language with assertions containing some user-written proofs. -- If the compiler itself would be translated into a language including a feather for dynamic typechecking, and if the user-written proofs would be convertible to functions, then it would be possible to apply those functions as prerequired properties for some subtypings or optimizations. -- This indeed, would provide more power to the compiler.

However, as far I can see, it would be rather useful for strengthening subtyping. -- It is hard to make a programmer to know, what property in what place would be helpful for the optimizer.


---

