Skip to content

Commit

Permalink
Update course desc
Browse files Browse the repository at this point in the history
  • Loading branch information
@dbp
dbp committed Mar 19, 2019
1 parent 8f6855b commit 48672fd
Show file tree
Hide file tree
Showing 5 changed files with 61 additions and 32 deletions.
17 changes: 11 additions & 6 deletions _site/courses/verifcomp/index.html
View file
Expand Up @@ -6,6 +6,11 @@
<title>dbp.io :: Verified Compilers and Multi-Language Software</title>
<link rel="stylesheet" type="text/css" href="../../css/default.css" />
<link rel="stylesheet" type="text/css" href="../../css/syntax.css" />
<style type="text/css">
a {
text-decoration: underline;
}
</style>
</head>
<body>

Expand Down Expand Up @@ -39,18 +44,18 @@ <h3 id="why-this-course"><strong>Why this course?</strong></h3>
<blockquote>
<p>“Can you trust your compiler?” — Xavier Leroy, developer of the Compcert verified C compiler</p>
</blockquote>
<p>Software is written in a variety of languages, and in most cases, in order to run, it must be compiled down to some lower-level target. <strong>But what if that compiler isn’t correct?</strong> Compilers are some of the trickier pieces of software we build, and yet bugs in them are insidious: bugs in compilers mean that one of our most basic debugging strategies, reading source code, may not be helpful, since what ran may not correspond to that source code!</p>
<p>In this setting, we must worry about what the compiler does and how our programs are translated to the target. Much better if the compiler were, essentially, invisible — if the source code fully specified what would happen. But a compiler can only truly be invisible if we can be sure that it does exactly what we expect: if we are sure it is correct. To be absolutely sure, we must prove it correct, and build a <em>verified</em> compiler.</p>
<p>Colliding with the field of verified compilation is the question of how different languages should be able to interact – that interaction, or linking, happens after compilation, in the lower-level target language. But the goal is to write source-level programs, not think about how our various languages compile, and so again, we are left wanting an invisible compiler, a verified compiler.</p>
<p>Software is written in a variety of languages, and in most cases, in order to run, it must be compiled down to some lower-level target. <strong>But what if that compiler isn’t correct?</strong> Compilers are some of the trickier pieces of software we build, and yet bugs in them are insidious: bugs in compilers mean that one of our most basic debugging strategies, reading source code, may not be helpful, since what actually ran may not correspond to that source code!</p>
<p>In the presence of buggy compilers, we must worry about what the compiler does and how our programs are translated to the target, possibly looking at compiler output or stepping through with low-level debuggers. Much better if the compiler were, essentially, invisible — if the source code fully specified what would happen. But a compiler can only truly be invisible if we can be sure that it does exactly what we expect: if we are sure it is correct. To be absolutely sure, we must prove it correct, and build a <em>verified</em> compiler.</p>
<p>Colliding with the field of verified compilation is the question of how different languages should be able to interact — that interaction, or linking, happens after compilation, in the lower-level target of compilation. But when using a variety of source languages, we would like to think in terms of those source languages, not worry about how our various languages compile, and so again, we are left wanting an invisible compiler, a verified compiler.</p>
<p>These are our high-level motivations. The course itself, while motivated with these problems, will be very grounded: we will be <strong>building languages, compilers, and proving them correct</strong>.</p>
<h3 id="how-will-the-course-be-structured"><strong>How will the course be structured?</strong></h3>
<p><strong>Part 1.</strong> We want to produce verified compilers, and so we will use one of the state-of-the-art tools used for this: the <a href="https://coq.inria.fr/">Coq proof assistant</a>. This system allows us to write functional programs, like compilers, and prove properties about them; afterwards we can extract runnable versions of the verified programs. The first section of the course will be dedicated to learning Coq and becoming familiar with the process of <em>mechanized</em> proof — that is, proofs that are checked by a machine. The text that we will use for this section of the course is <a href="https://ilyasergey.net/pnp">“Programs and Proofs” by Ilya Sergey</a>.</p>
<p><strong>Part 1.</strong> We want to produce verified compilers, and so we will use one of the state-of-the-art tools used for this: the <a href="https://coq.inria.fr/">Coq proof assistant</a>. This is a general purpose tool — in addition to being used to build a verified <a href="http://compcert.inria.fr/">optimizing C compiler</a>, in work towards <a href="http://flint.cs.yale.edu/certikos/">certified operating systems</a> and <a href="http://verasco.imag.fr/wiki/Main_Page">other</a> <a href="https://github.com/mit-plv/fiat-crypto">verification</a> <a href="https://jasmin-lang.github.io/">projects</a>. It has also been used in various efforts of formalizing mathematics (most notably, the <a href="https://en.wikipedia.org/wiki/Four_color_theorem">Four Color Theorem</a>). For our purpose, Coq allows us to write functional programs, like compilers, and prove properties about them, like correctness. The first section of the course will be dedicated to learning Coq and becoming familiar with the process of <em>mechanized</em> proof — that is, proofs that are checked by a machine. The text that we will use for this section of the course is <a href="https://ilyasergey.net/pnp">“Programs and Proofs” by Ilya Sergey</a>.</p>
<p><strong>Part 2.</strong> This part of the course will involve designing, in groups, different source languages. These will all likely be simple functional languages, and we will do plenty of design review to ensure that the language design you pick will not cause too much difficulty later on.</p>
<p><strong>Part 3.</strong> The final part will involve building and proving correct compilers from your language to a common low-level target language. All the languages will compile to the same target language, and so once we have compilers, and concurrent with the verification effort, you will experiment building small programs that use a mixture of different student languages.</p>
<h3 id="a-note-on-collaboration"><strong>A note on collaboration</strong></h3>
<p>This will be a highly collaborative course. For the first section, the actual assignments will be done individually, to ensure that you get sufficient practice with theorem-proving, as proof assistants like Coq are not something you can learn without using. Even so, we <em>expect and encourage people to work together throughout the course</em>, beyond just the teams you are working in, provided that the actual work you submit is you own. Once the first section ends, the course will truly become a large collaboration. All of our compilers will be worked on in a shared repository, and while you will be assessed on and be responsible for understanding your own compiler, all are welcome to help any of your classmates. We will do also do group reviews or reviews of one group by another.</p>
<p>This will be a highly collaborative course. For the first section, the actual assignments will be done individually, to ensure that you get sufficient practice with theorem-proving, as proof assistants like Coq are not something you can learn without using. Even so, we <em>expect and encourage people to work together throughout the course</em>, beyond just the teams you are working in, provided that the actual work you submit is your own. Once the first section ends, the course will truly become a large collaboration. All of our compilers will be in a shared repository, and while you will be assessed on and be responsible for understanding your own compiler, all are welcome to help any of your classmates. We will also do group reviews or reviews of one group by another.</p>
<h3 id="requirements"><strong>Requirements</strong></h3>
<p>Intended for advanced undergraduates, you would be well prepared by either having taken CS4400 (programming languages) or CS4410 (compilers). However, if you are interested and haven’t taken either, <strong>please reach out to the instructor</strong>. Additionally, familiarity with typed functional languages (e.g., Scala, Haskell, or OCaml) would be helpful, as would any exposure to formal proof in mathematics.</p>
<p>Intended for advanced undergraduates, you would be well prepared by either having taken CS4400 (programming languages) or CS4410 (compilers). However, if you are interested and haven’t taken either, <strong>please reach out to the instructor</strong>. I’m happy to talk to you about your background, or give you additional information about the type of stuff we’ll be working on to see if it seems like it’ll be a good fit. While not required, familiarity with typed functional languages (e.g., Scala, Haskell, or OCaml) would be helpful, since Coq is related to that class of language, as would any exposure to formal proof in mathematics.</p>
<h3 id="other-question-something-not-clear"><strong>Other question? Something not clear?</strong></h3>
<p>Please reach out to the instructor: Daniel Patterson (<a href="mailto:dbp@dbpmail.net">dbp@dbpmail.net</a>)</p>
<p><br /><br /></p>
Expand Down
2 changes: 2 additions & 0 deletions _site/index.html
View file
Expand Up @@ -61,6 +61,8 @@ <h3 id="publications">Publications</h3>
Joe Gibbs Politz, Alejandro Martinez, Matthew Milano, Sumner Warren, Daniel Patterson, Junsong Li, Anand Chitipothu, and Shriram Krishnamurthi. <br /><em>OOPSLA 2013</em>. <a href="./pubs/2013/lambda-py-oopsla.pdf">PDF</a>, <a href="./pubs/2013/lambda-py-appendix-oopsla.pdf">appendix</a> and <a href="http://cs.brown.edu/research/plt/dl/lambda-py/ae/">code</a>.
</div>
</div>
<h3 id="teaching">Teaching</h3>
<p><strong>Fall 2019: </strong> <a href="./courses/verifcomp">CS4910: Verified Compilers and Multi-Language Software</a></p>
<h3 id="talks">Talks</h3>
<div class="pubs">
<strong>On Compositional Compiler Correctness and Fully Abstract Compilation.</strong>
Expand Down
65 changes: 39 additions & 26 deletions courses/verifcomp.markdown
View file
Expand Up @@ -21,35 +21,45 @@ run, it must be compiled down to some lower-level target. **But what if that
compiler isn't correct?** Compilers are some of the trickier pieces of software
we build, and yet bugs in them are insidious: bugs in compilers mean that
one of our most basic debugging strategies, reading source code, may not be
helpful, since what ran may not correspond to that source code!
helpful, since what actually ran may not correspond to that source code!

In this setting, we must worry about what the compiler does and how our programs
are translated to the target. Much better if the compiler were, essentially,
invisible --- if the source code fully specified what would happen. But a
compiler can only truly be invisible if we can be sure that it does exactly what
we expect: if we are sure it is correct. To be absolutely sure, we must prove it
correct, and build a _verified_ compiler.
In the presence of buggy compilers, we must worry about what the compiler does
and how our programs are translated to the target, possibly looking at compiler
output or stepping through with low-level debuggers. Much better if the compiler
were, essentially, invisible --- if the source code fully specified what would
happen. But a compiler can only truly be invisible if we can be sure that it
does exactly what we expect: if we are sure it is correct. To be absolutely
sure, we must prove it correct, and build a _verified_ compiler.

Colliding with the field of verified compilation is the question of how
different languages should be able to interact -- that interaction, or linking,
happens after compilation, in the lower-level target language. But the goal is
to write source-level programs, not think about how our various languages
compile, and so again, we are left wanting an invisible compiler, a verified
compiler.
different languages should be able to interact --- that interaction, or linking,
happens after compilation, in the lower-level target of compilation. But when
using a variety of source languages, we would like to think in terms of those
source languages, not worry about how our various languages compile, and so
again, we are left wanting an invisible compiler, a verified compiler.

These are our high-level motivations. The course itself, while motivated with
these problems, will be very grounded: we will be **building languages,
compilers, and proving them correct**.

### **How will the course be structured?**
**Part 1.** We want to produce verified compilers, and so we will use one of the
state-of-the-art tools used for this: the [Coq proof assistant](https://coq.inria.fr/). This system
allows us to write functional programs, like compilers, and prove properties about them;
afterwards we can extract runnable versions of the verified programs. The first
section of the course will be dedicated to learning Coq and becoming familiar
with the process of _mechanized_ proof --- that is, proofs that are checked by a
machine. The text that we will use for this section of the course is ["Programs
and Proofs" by Ilya Sergey](https://ilyasergey.net/pnp).
state-of-the-art tools used for this: the [Coq proof
assistant](https://coq.inria.fr/). This is a general purpose tool --- in
addition to being used to build a verified [optimizing C
compiler](http://compcert.inria.fr/), in work towards [certified operating
systems](http://flint.cs.yale.edu/certikos/) and
[other](http://verasco.imag.fr/wiki/Main_Page)
[verification](https://github.com/mit-plv/fiat-crypto)
[projects](https://jasmin-lang.github.io/). It has also been used in various
efforts of formalizing mathematics (most notably, the [Four Color
Theorem](https://en.wikipedia.org/wiki/Four_color_theorem)). For our purpose, Coq allows
us to write functional programs, like compilers, and prove properties about
them, like correctness. The
first section of the course will be dedicated to learning Coq and becoming
familiar with the process of _mechanized_ proof --- that is, proofs that are
checked by a machine. The text that we will use for this section of the course
is ["Programs and Proofs" by Ilya Sergey](https://ilyasergey.net/pnp).

**Part 2.** This part of the course will involve designing, in groups, different
source languages. These will all likely be simple functional languages, and we
Expand All @@ -68,21 +78,24 @@ assignments will be done individually, to ensure that you get sufficient
practice with theorem-proving, as proof assistants like Coq are not something
you can learn without using. Even so, we _expect and encourage people to work
together throughout the course_, beyond just the teams you are working in,
provided that the actual work you submit is you own. Once the first section
provided that the actual work you submit is your own. Once the first section
ends, the course will truly become a large collaboration. All of our compilers
will be worked on in a shared repository, and while you will be assessed on and
will be in a shared repository, and while you will be assessed on and
be responsible for understanding your own compiler, all are welcome to help any
of your classmates. We will do also do group reviews or reviews of one group by
of your classmates. We will also do group reviews or reviews of one group by
another.


### **Requirements**
Intended for advanced undergraduates, you would be well prepared by either
having taken CS4400 (programming languages) or CS4410 (compilers). However, if
you are interested and haven't taken either, **please reach out to the instructor**.
Additionally, familiarity with typed functional languages (e.g., Scala, Haskell,
or OCaml) would be helpful, as would any exposure to formal proof in
mathematics.
you are interested and haven't taken either, **please reach out to the
instructor**. I'm happy to talk to you about your background, or give you
additional information about the type of stuff we'll be working on to see if it
seems like it'll be a good fit. While not required, familiarity with typed
functional languages (e.g., Scala, Haskell, or OCaml) would be helpful, since
Coq is related to that class of language, as would any exposure to formal proof
in mathematics.


### **Other question? Something not clear?**
Expand Down
4 changes: 4 additions & 0 deletions index.markdown
View file
Expand Up @@ -31,6 +31,10 @@ The easiest way to get in touch is via email: <a href="mailto:dbp@dbpmail.net">d
<div class="desc">Joe Gibbs Politz, Alejandro Martinez, Matthew Milano, Sumner Warren, Daniel Patterson, Junsong Li, Anand Chitipothu, and Shriram Krishnamurthi. <br/>_OOPSLA 2013_. [PDF](/pubs/2013/lambda-py-oopsla.pdf), [appendix](/pubs/2013/lambda-py-appendix-oopsla.pdf) and [code](http://cs.brown.edu/research/plt/dl/lambda-py/ae/).</div>
</div>

### Teaching

**Fall 2019: ** [CS4910: Verified Compilers and Multi-Language Software](/courses/verifcomp)

### Talks

<div class="pubs">
Expand Down
5 changes: 5 additions & 0 deletions templates/course.html
View file
Expand Up @@ -6,6 +6,11 @@
<title>dbp.io :: $title$</title>
<link rel="stylesheet" type="text/css" href="/css/default.css" />
<link rel="stylesheet" type="text/css" href="/css/syntax.css" />
<style type="text/css">
a {
text-decoration: underline;
}
</style>
</head>
<body>

Expand Down

0 comments on commit 48672fd

Please sign in to comment.