Rainy letter about ttfv

letter.txt.diff

--- letter.txt.orig 2012-04-18 02:21:35.122840949 +0400
+++ letter.txt  2012-04-18 02:29:19.317062201 +0400
@@ -2,9 +2,9 @@

 Как-то по так получилось, что по моей неосторожности намечается такой
 длинный до самого упора пока все не разъедутся семинар и крэш-курс по
-теории типов и релейтер штукам.
+теории типов и релейтед штукам.
 У этого мероприятия есть домашняя страница:
-http://oxij.org/activity/ttfv/ на которой имеются ссылки на всякие
+http://oxij.org/activity/ttfv/, на которой имеются ссылки на всякие
 гугльгруппы (если будете вступать, то представляйтесь заодно и своим
 номером группы в комментариях) и прочие интересные вещи.
 Язык самих семинаров русский, наверное, но мне бы хотелось из
@@ -16,12 +16,12 @@

 В этот четверг в 19:30 в районе аудитории 147А будет нечто
 напоминающее первый семинар, где я быстро-быстро расскажу про
-нетипизированное лямбда исчисление, покажу как на этом писать простые
+нетипизированное лямбда исчисление, покажу, как на этом писать простые
 рекурсивные программы на эдаком нетипизированном Haskell.
 По дороге мы докажем какие-то свойства этого исчисления и напишем
 интерпретатор этого исчисления на самом себе.

-После этого мы вдадимся в язык программирования Agda, я покажу как его
+После этого мы вдадимся в язык программирования Agda, я покажу, как его
 использовать в качестве формальной логики для доказательства простых
 арифметических утверждений и простых утверждений о программах.
 Дальше, видимо, я расскажу немного той а-ля "категориальной"
@@ -60,13 +60,13 @@

 С учётом всего вышесказанного, приглашаю присоединиться к нам всех
 достаточно мотивированных, однако первые встречи, содержание которых
-расписано до символа "*" могут оказаться весьма полезными всем
+расписано до символа "*", могут оказаться весьма полезными всем
 студентам.
-Не смотря на то, что они весьма далеки от стандартного курса
+Несмотря на то, что они весьма далеки от стандартного курса
 математики студентов КТ (за исключением, может быть, курса матлогики),
-практика показывает, что, после освоения интуиционистской
+практика показывает, что после освоения интуиционистской
 (конструктивной) логики и её методов доказательств (в нашем случае
-через призму Agda), подход к программированию изменяется в позитивном
+через призму Agda) подход к программированию изменяется в позитивном
 направлении, всякие новомодные фичи языков типа C++ становятся
 тривиальными, а классическая логика даётся значительно проще, что,
 кроме всего прочего, улучшает понимание всяких менее полезных для
@@ -82,7 +82,7 @@
 В остальных случаях требуется (как минимум) готовность начать
 абстрактно и алгебраически рассуждать о привычных вещах и жуткое
 усердие по накачиванию мозгов новыми знаниями (и мотивация покорять
-формальные системы); при этом вам, скорее всего, понадобиться знание
+формальные системы); при этом вам, скорее всего, понадобится знание
 технического английского, много литературы на оном и
 последовательность в её изучении; в предпоследнем я могу помочь, но не
 готов никоим образом участвовать в последнем.
@@ -93,7 +93,7 @@
 значительно чаще, чем хотелось бы (это, очевидно, касается и того, что
 буду рассказывать я), но мы будем стараться быстро исправляться и
 всячески заставлять Agda проверять нас, где возможно.
-* Я думаю, что от сессии никто, ни вас, ни меня, освобождать не будет.
+* Я думаю, что от сессии никто ни вас, ни меня освобождать не будет.
 Так что тут надо аккуратно жонглировать распределением времени.

 С уважением,