diff --git a/_site/apple/index.html b/_site/apple/index.html new file mode 100644 index 0000000..7f5df78 --- /dev/null +++ b/_site/apple/index.html @@ -0,0 +1,33 @@ + + + + + + dbp.io :: + + + + + +

Campion Apple 16

+

Build Threod with Photos

+

Time Log

+ + + diff --git a/_site/artifacts/funtal/codemirror.js b/_site/artifacts/funtal/codemirror.js index 7191dac..272fcd2 100644 Binary files a/_site/artifacts/funtal/codemirror.js and b/_site/artifacts/funtal/codemirror.js differ diff --git a/_site/artifacts/funtal/matchbrackets.js b/_site/artifacts/funtal/matchbrackets.js index a04842f..31f1201 100644 Binary files a/_site/artifacts/funtal/matchbrackets.js and b/_site/artifacts/funtal/matchbrackets.js differ diff --git a/_site/artifacts/funtal/runmode.js b/_site/artifacts/funtal/runmode.js index a32b78b..42ec6df 100644 Binary files a/_site/artifacts/funtal/runmode.js and b/_site/artifacts/funtal/runmode.js differ diff --git a/_site/artifacts/funtal/simple.js b/_site/artifacts/funtal/simple.js index 55dee44..f49ee6e 100644 Binary files a/_site/artifacts/funtal/simple.js and b/_site/artifacts/funtal/simple.js differ diff --git a/_site/artifacts/funtal/web.js b/_site/artifacts/funtal/web.js index 2996285..11b2b9d 100644 Binary files a/_site/artifacts/funtal/web.js and b/_site/artifacts/funtal/web.js differ diff --git a/_site/courses/verifcomp/index.html b/_site/courses/verifcomp/index.html deleted file mode 100644 index 68478c3..0000000 --- a/_site/courses/verifcomp/index.html +++ /dev/null @@ -1,260 +0,0 @@ - - - - - - dbp.io :: Verified Compilers and Multi-Language Software - - - - - - -

Verified Compilers and Multi-Language Software

- - - - - - - - - - - - - - - - - - - - - - - - -
CourseCS4910 (CRN 17946): Verified Compilers and Multi-Language Software
SemesterFall 2019
MeetingMonday/Thursday, 11:45AM-1:25PM
InstructorDaniel Patterson (dbp@dbpmail.net)
OfficeWVH 308
-

Why this course?

-
-

“Can you trust your compiler?” — Xavier Leroy, developer of the Compcert verified C compiler

-
-

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. 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 actually ran may not correspond to that source code!

-

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 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. This is a general purpose tool — in addition to being used to build a verified optimizing C compiler, in work towards certified operating systems and other verification projects. It has also been used in various efforts of formalizing mathematics (most notably, the 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.

-

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 will do plenty of design review to ensure that the language design you pick will not cause too much difficulty later on.

-

Part 3. 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.

-

A note on collaboration

-

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 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 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.

-

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. 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.

-

Schedule

- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
WeekDateTopicReadingAssignment
09/5Course structure, intro to Coq / mechanized mathematics, Coq setup.
19/9
9/12
29/16
9/19
39/23
9/26
49/30
10/3
510/7
10/10
610/14NO CLASS
10/17
710/21
10/24
810/28
10/31
911/4
11/7
1011/11NO CLASS
11/14
1111/18
11/21
1211/25
11/28NO CLASS
1312/2
-

Other question? Something not clear?

-

Please reach out to the instructor: Daniel Patterson (dbp@dbpmail.net)

-



- - - diff --git a/_site/static/apple/IMG_0195.jpeg b/_site/static/apple/IMG_0195.jpeg new file mode 100644 index 0000000..6834775 Binary files /dev/null and b/_site/static/apple/IMG_0195.jpeg differ diff --git a/_site/static/apple/IMG_0232.jpeg b/_site/static/apple/IMG_0232.jpeg new file mode 100644 index 0000000..6470f7a Binary files /dev/null and b/_site/static/apple/IMG_0232.jpeg differ diff --git a/_site/static/apple/IMG_0235.jpeg b/_site/static/apple/IMG_0235.jpeg new file mode 100644 index 0000000..b815d52 Binary files /dev/null and b/_site/static/apple/IMG_0235.jpeg differ diff --git a/_site/static/apple/IMG_0237.jpeg b/_site/static/apple/IMG_0237.jpeg new file mode 100644 index 0000000..87db82f Binary files /dev/null and b/_site/static/apple/IMG_0237.jpeg differ diff --git a/_site/static/apple/IMG_0239.jpeg b/_site/static/apple/IMG_0239.jpeg new file mode 100644 index 0000000..c9ce600 Binary files /dev/null and b/_site/static/apple/IMG_0239.jpeg differ diff --git a/_site/static/apple/IMG_0254.jpeg b/_site/static/apple/IMG_0254.jpeg new file mode 100644 index 0000000..ee4ffcd Binary files /dev/null and b/_site/static/apple/IMG_0254.jpeg differ diff --git a/_site/static/apple/IMG_0261.jpeg b/_site/static/apple/IMG_0261.jpeg new file mode 100644 index 0000000..15e0203 Binary files /dev/null and b/_site/static/apple/IMG_0261.jpeg differ diff --git a/_site/static/apple/IMG_0262.jpeg b/_site/static/apple/IMG_0262.jpeg new file mode 100644 index 0000000..69e9e90 Binary files /dev/null and b/_site/static/apple/IMG_0262.jpeg differ diff --git a/_site/static/apple/IMG_0271.jpeg b/_site/static/apple/IMG_0271.jpeg new file mode 100644 index 0000000..4136c77 Binary files /dev/null and b/_site/static/apple/IMG_0271.jpeg differ diff --git a/_site/static/apple/IMG_0274.jpeg b/_site/static/apple/IMG_0274.jpeg new file mode 100644 index 0000000..da6a552 Binary files /dev/null and b/_site/static/apple/IMG_0274.jpeg differ diff --git a/_site/static/apple/IMG_0277.jpeg b/_site/static/apple/IMG_0277.jpeg new file mode 100644 index 0000000..28ef2a1 Binary files /dev/null and b/_site/static/apple/IMG_0277.jpeg differ diff --git a/_site/static/apple/IMG_0281.jpeg b/_site/static/apple/IMG_0281.jpeg new file mode 100644 index 0000000..086906c Binary files /dev/null and b/_site/static/apple/IMG_0281.jpeg differ diff --git a/_site/static/apple/IMG_0282.jpeg b/_site/static/apple/IMG_0282.jpeg new file mode 100644 index 0000000..2167ce5 Binary files /dev/null and b/_site/static/apple/IMG_0282.jpeg differ diff --git a/_site/static/apple/IMG_0285.jpeg b/_site/static/apple/IMG_0285.jpeg new file mode 100644 index 0000000..3ab7117 Binary files /dev/null and b/_site/static/apple/IMG_0285.jpeg differ diff --git a/_site/static/apple/IMG_0286.jpeg b/_site/static/apple/IMG_0286.jpeg new file mode 100644 index 0000000..93e4580 Binary files /dev/null and b/_site/static/apple/IMG_0286.jpeg differ diff --git a/_site/static/apple/IMG_0290.jpeg b/_site/static/apple/IMG_0290.jpeg new file mode 100644 index 0000000..b6f06f3 Binary files /dev/null and b/_site/static/apple/IMG_0290.jpeg differ diff --git a/_site/static/apple/IMG_0293.jpeg b/_site/static/apple/IMG_0293.jpeg new file mode 100644 index 0000000..287a22c Binary files /dev/null and b/_site/static/apple/IMG_0293.jpeg differ diff --git a/_site/static/apple/IMG_0294.jpeg b/_site/static/apple/IMG_0294.jpeg new file mode 100644 index 0000000..82df7d0 Binary files /dev/null and b/_site/static/apple/IMG_0294.jpeg differ diff --git a/apple.markdown b/apple.markdown new file mode 100644 index 0000000..a417148 --- /dev/null +++ b/apple.markdown @@ -0,0 +1,7 @@ +## Campion Apple 16 + +[Build Threod with Photos](http://forum.woodenboat.com/showthread.php?259432-Campion-Apple-16-Build) + +## Time Log + + diff --git a/site b/site index 51e7e70..8954fee 100755 --- a/site +++ b/site @@ -119,6 +119,12 @@ main = hakyllWith config $ do >>= loadAndApplyTemplate "templates/default.html" (pageCtx "") >>= relativizeUrls + match "apple.markdown" $ do + route $ constRoute "apple/index.html" + compile $ pandocCompiler + >>= loadAndApplyTemplate "templates/default.html" (pageCtx "") + >>= relativizeUrls + match "404.markdown" $ do route $ setExtension ".html" compile $ pandocCompiler diff --git a/static/apple/IMG_0195.jpeg b/static/apple/IMG_0195.jpeg new file mode 100644 index 0000000..6834775 Binary files /dev/null and b/static/apple/IMG_0195.jpeg differ diff --git a/static/apple/IMG_0232.jpeg b/static/apple/IMG_0232.jpeg new file mode 100644 index 0000000..6470f7a Binary files /dev/null and b/static/apple/IMG_0232.jpeg differ diff --git a/static/apple/IMG_0235.jpeg b/static/apple/IMG_0235.jpeg new file mode 100644 index 0000000..b815d52 Binary files /dev/null and b/static/apple/IMG_0235.jpeg differ diff --git a/static/apple/IMG_0237.jpeg b/static/apple/IMG_0237.jpeg new file mode 100644 index 0000000..87db82f Binary files /dev/null and b/static/apple/IMG_0237.jpeg differ diff --git a/static/apple/IMG_0239.jpeg b/static/apple/IMG_0239.jpeg new file mode 100644 index 0000000..c9ce600 Binary files /dev/null and b/static/apple/IMG_0239.jpeg differ diff --git a/static/apple/IMG_0254.jpeg b/static/apple/IMG_0254.jpeg new file mode 100644 index 0000000..ee4ffcd Binary files /dev/null and b/static/apple/IMG_0254.jpeg differ diff --git a/static/apple/IMG_0261.jpeg b/static/apple/IMG_0261.jpeg new file mode 100644 index 0000000..15e0203 Binary files /dev/null and b/static/apple/IMG_0261.jpeg differ diff --git a/static/apple/IMG_0262.jpeg b/static/apple/IMG_0262.jpeg new file mode 100644 index 0000000..69e9e90 Binary files /dev/null and b/static/apple/IMG_0262.jpeg differ diff --git a/static/apple/IMG_0271.jpeg b/static/apple/IMG_0271.jpeg new file mode 100644 index 0000000..4136c77 Binary files /dev/null and b/static/apple/IMG_0271.jpeg differ diff --git a/static/apple/IMG_0274.jpeg b/static/apple/IMG_0274.jpeg new file mode 100644 index 0000000..da6a552 Binary files /dev/null and b/static/apple/IMG_0274.jpeg differ diff --git a/static/apple/IMG_0277.jpeg b/static/apple/IMG_0277.jpeg new file mode 100644 index 0000000..28ef2a1 Binary files /dev/null and b/static/apple/IMG_0277.jpeg differ diff --git a/static/apple/IMG_0281.jpeg b/static/apple/IMG_0281.jpeg new file mode 100644 index 0000000..086906c Binary files /dev/null and b/static/apple/IMG_0281.jpeg differ diff --git a/static/apple/IMG_0282.jpeg b/static/apple/IMG_0282.jpeg new file mode 100644 index 0000000..2167ce5 Binary files /dev/null and b/static/apple/IMG_0282.jpeg differ diff --git a/static/apple/IMG_0285.jpeg b/static/apple/IMG_0285.jpeg new file mode 100644 index 0000000..3ab7117 Binary files /dev/null and b/static/apple/IMG_0285.jpeg differ diff --git a/static/apple/IMG_0286.jpeg b/static/apple/IMG_0286.jpeg new file mode 100644 index 0000000..93e4580 Binary files /dev/null and b/static/apple/IMG_0286.jpeg differ diff --git a/static/apple/IMG_0290.jpeg b/static/apple/IMG_0290.jpeg new file mode 100644 index 0000000..b6f06f3 Binary files /dev/null and b/static/apple/IMG_0290.jpeg differ diff --git a/static/apple/IMG_0293.jpeg b/static/apple/IMG_0293.jpeg new file mode 100644 index 0000000..287a22c Binary files /dev/null and b/static/apple/IMG_0293.jpeg differ diff --git a/static/apple/IMG_0294.jpeg b/static/apple/IMG_0294.jpeg new file mode 100644 index 0000000..82df7d0 Binary files /dev/null and b/static/apple/IMG_0294.jpeg differ