-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathindex.html
188 lines (171 loc) · 9.81 KB
/
index.html
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
<!doctype html>
<html>
<head>
<meta charset="utf-8">
<title>The Little Typer reading group (Stellenbosch 5 March 2025)</title>
<link rel="shortcut icon" href="https://funexists.github.io/favicon.ico" />
<!-- github style -->
<meta name="viewport" content="width=device-width, initial-scale=1, minimal-ui">
<meta name="color-scheme" content="light dark">
<link rel="stylesheet" href="./github-markdown.css">
<style>
body {
box-sizing: border-box;
min-width: 200px;
max-width: 980px;
margin: 0 auto;
padding: 45px;
}
@media(prefers-color-scheme: dark) {
body {
background-color: #0d1117;
}
}
</style>
</head>
<body>
<article class="markdown-body">
<h1 align="center">
The Little Typer reading group (Stellenbosch 5 March 2025)
</h1>
<p align="center">
<a href="http://thelittletyper.com">
<img alt="The Little Typer Book" title="The Little Typer Book" height="400" src="./thelittletyper.jpeg" />
</a>
</p>
<p align="center">
Join our <a href="https://discord.gg/jPfjBAkEtV">Discord</a>
</p>
<p>
The Little Typer provides an introduction to the field of writing programs that are proofs.
It explains all the foundational concepts you will need to write proofs in Proof Assistants or program in a Dependently Typed Programming Language.
Examples of these languages include: <a href="https://lean-lang.org">Lean</a>, <a href="https://www.idris-lang.org">Idris</a>, <a href="https://wiki.portal.chalmers.se/agda/pmwiki.php">Agda</a> and <a href="https://coq.inria.fr">Coq</a>.
These tools allow us to not only prove that our critical code is correct, but also to write mathematical proofs that are automatically checked, so we can collaborate with other authors on github.
If you would like a larger taste of the topic, see our <a href="https://medium.com/better-programming/a-taste-of-coq-and-correct-code-by-construction-111bf74d3b98">blog post</a> or video:
</p>
<p align="center">
<iframe width="560" height="315" src="https://www.youtube.com/embed/-NHWF4ntc1I?si=kMzIlT1xX1NK-wsi" title="YouTube video player" frameborder="0" allow="accelerometer; autoplay; clipboard-write; encrypted-media; gyroscope; picture-in-picture; web-share" referrerpolicy="strict-origin-when-cross-origin" allowfullscreen></iframe>
</p>
<h2>Requirements</h2>
<p>
Anyone can join, if you meet the following requirements:
<ul>
<li>You have had some experience using recursion in the past.</li>
<li>You have a computer to install and run <a href="https://github.com/the-little-typer/pie">Pie</a></li>
</ul>
</p>
<p>
You <b>do not need</b> to be an experienced programmer or be a able to write or read mathematical proofs.
You <b>do need</b> to be able to write code that uses recursion.
If you were able to, at some point in the past, write a program that calculates the length of a linked list using recursion, then you meet the requirements.
If you have never done any recursion, then we recommend reading <a href="https://mitpress.mit.edu/9780262560993/the-little-schemer/">The Little Schemer</a> first.
</p>
<p>
You <b>will need</b> to <a href="https://github.com/funexists/2025-stellenbosch">install</a> and write code in Pie on a computer.
The Little Typer uses a language called <a href="https://github.com/the-little-typer/pie">Pie</a>, which is a very simple <a href="https://en.wikibooks.org/wiki/Scheme_Programming/A_taste_of_Scheme">Scheme like programming language</a>.
It has very little syntax or language features, which allows us to focus on understanding the core concepts of calling functions, writing functions and typing functions, which will be applicable in all Proof Assistants/Dependently Typed Programming Languages.
</p>
<h2>What will you Learn</h2>
<p>
This reading group will teach you:
<ul>
<li>that programming is writing proofs and type annotations are propositions.</li>
<li>what Algebraic Data Types are.</li>
<li>how to write proofs using induction, that are automatically checked by the computer.</li>
<li>programming with Dependent types, for example how to receive a type (not just a value) as a parameter and return a modified type from a function, as if that type was just a value.</li>
<li>how to write proofs that programs are equal and then use those equalities to rewrite inside propositions.</li>
</ul>
</p>
<h2>Examples industry use cases and mathematical proofs</h2>
<p>
<ul>
<li><a href="https://en.wikipedia.org/wiki/Four_color_theorem">Four Colour Theorem</a></li>
<li><a href="https://www.cl.cam.ac.uk/~caw77/papers/mechanising-and-verifying-the-webassembly-specification.pdf">Formalized Web Assembly Spec</a></li>
<li><a href="https://www.lambdadays.org/static/upload/media/161639788325786adamchlipalacorrectbyconstructioncryptographicarithmeticincoq.pdf">Cryptographic Arithmetic for Chrome and Firefox</a></li>
<li><a href="https://arxiv.org/abs/1910.12320">Perfectoid Spaces - Kevin Buzzard, et al.</a></li>
</ul>
</p>
<h2>Examples of people that might be interested</h2>
<p>
<ul>
<li>
<a href="https://medium.com/better-programming/a-programmers-regret-neglecting-math-at-university-9d937655752b">
You are a Computer Science student, but struggle to find the motivation to understand mathematical proofs
</a>
</li>
<li>You are a student of Mathematics trying to understand how their skills can be applicable for programming in industry.</li>
<li>You are a Professor looking for a new class to teach or subject to enhance with formal verification.</li>
<li>You are a working programmer looking for a new challenge.</li>
<li>You are a Mathematician looking for a better way to collaborate.</li>
<li>Anyone with a basic understanding of recursion.</li>
</ul>
</p>
<h2>Schedule</h2>
<p>
Each Wednesday 18:00 - 20:00 starting 5 March 2025 we will discuss chapters we have read and exercises we completed for that week.
The schedule is quite intense. It is not a lot to read, but it is a lot to grasp and each week has a few exercises.
We estimate that this will be about 4 hours of work per week for 10 weeks.
More details of the schedule can be found on the <a href="https://github.com/funexists/2025-stellenbosch">github repository</a>.
</p>
<h2>Location</h2>
<p>
<a href="https://maps.app.goo.gl/qqBeakhFgFemaeLu8">Decanting Facility, 2nd floor, Hammanshand Rd, Stellenbosch</a>, close to the LaunchLab.
</p>
<h2>Presented By</h2>
<p>
<ul>
<li><a href="https://www.linkedin.com/in/awalterschulze/">Walter Schulze</a>: Taking a break from 10+ years programming at Meta, eBay, Vastech and Entersekt to do a PhD in Informatics at Stellenbosch using Coq and Lean.</li>
<li><a href="https://www.linkedin.com/in/keeganperry/">Keegan Perry</a>: Master's student at Stellenbosch University working on the formal verification of software using Lean.</li>
<li><a href="https://www.linkedin.com/in/brink-van-der-merwe/">Brink van der Merwe</a>: Professor in Computer Science at Stellenbosch University, with an interest in using Lean in his own reseach and the research of his postgraduate students.</li>
</ul>
</p>
<h2>Sponsored By</h2>
<p>
<a href="https://nithecs.ac.za">
<img
alt="The National Institute for Theoretical and Computational Sciences"
title="The National Institute for Theoretical and Computational Sciences"
src="./nithecs.png"
height="48"
style="vertical-align:middle;"
/>
</a>
<a
href="https://nithecs.ac.za"
style="text-align:center;display:inline-block;">
The National Institute for Theoretical and Computational Sciences
</a>
</p>
<h2>Costs</h2>
<p>
It is free. We will provide the book for the first 20 successful #s on <a href="https://discord.gg/jPfjBAkEtV">Discord</a> with full name. Other attendees might need to <a href="https://www.loot.co.za/product/the-little-typer/wxjk-5519-g050">buy the book</a>.
</p>
<h2>Join Us!</h2>
<p>
<ul>
<li>
<a href="https://discord.gg/jPfjBAkEtV">
<img
alt="Join our Discord"
title="Join our Discord"
src="./discord.svg"
height="24"
width="24"
/>
</a>
Join our <a href="https://discord.gg/jPfjBAkEtV">Discord</a> if you want to join our reading group or have any questions.
</li>
<li>
If you are having any trouble joining Discord and want to reserve your spot, you can send an email to <b>awalterschulze @ gmail</b>.
</li>
<li>
<a href="https://github.com/funexists/2025-stellenbosch">
<img alt="GitHub" title="GitHub" height="24" width="24" src="./github.svg" />
</a>
More Information can be found on our <a href="https://github.com/funexists/2025-stellenbosch">Github</a>.
</li>
</ul>
</p>
</article>
</body>
</html>