Alexander Chichigin gabriel-fallen

Вступление

Во-первых, это моё мнение, и я его никому не навязываю. Во-вторых, список не обязательно исчерпывающий. В-третьих, он ориентирован на определённую "философию", которая тоже не является исчерпывающей или абсолютно правильной. Поэтому, если Вам эти рекомендации не подходят -- не следуйте им.

Философия такова. Для того чтобы осмысленно программировать на начальном этапе не нужно знать Computer Science, теорию алгоритмов и сложности вычислений или детально разбираться в устройстве и работе компьютера. Достаточно хорошо делать две вещи:

алгоритмизировать решение задачи (разбивать его на простые последовательные шаги: сначала это, а потом вот это),
знать, понимать смысл и назначение, использовать и подгонять друг к другу стандартные элементы решений (условия, циклы, структуры данных, алгоритмы и прочие "паттерны")

Презентации и справочники

https://docs.google.com/file/d/0B3gcGsPmNL0VT2RjLVZybTNkclE/edit

Задание 1

Установить сервер Apache Tomcat (или другой servlet-compatible сервер)

Статьи против Программ

На днях заметил, что читать статьи (по computer science) гораздо сложнее, чем читать/писать программы. Кажется парадоксальным, но вполне объяснимо — всё дело в пресловутом управлении сложностью.

Как известно, объём "кэша" у человека сильно ограничен — одновременно можно думать всего о 5-9 вещах. Может быть, некоторые могут думать об 11 вещах одновременно, но едва ли больше. Если учесть, что как правило нужно помнить не только отдельные объекты, но и связи между ними, то получится удержать в сознании всего 3 (+ 3 связи = 6) или 4 (+ 6 связей = 10) сущности.

	# in ~/.fluxbox/keys
	# change KB layout
	# Mod4 k e # English
	Mod4 45 26 :Exec setxkbmap us
	# Mod4 k r # Russian
	Mod4 45 27 :Exec setxkbmap ru


	(declare-sort Type)
	(declare-sort Term)
	(declare-fun HasType (Term Type) Bool)

	(declare-fun string () Type) ; type of strings of a programming language
	(declare-fun nat () Type) ; type of natural numbers of a programming language
	(declare-fun list () Type) ; type of lists should be parametrized by type of elements but we ignore it for simplicity

	(declare-fun BoxString (String) Term)

	theory GCD
	imports Main
	begin

	fun gcd :: "nat ⇒ nat ⇒ nat" where
	"gcd m 0 = m" \|
	"gcd m n = gcd n (m mod n)"


	theorem gcd_dvd_both: "(gcd m n dvd m) ∧ (gcd m n dvd n)"

	module SampleTheorems

	%default total

	reverse' : List a -> List a
	reverse' [] = []
	reverse' (x :: xs) = reverse' xs ++ [x]

	append_nil : xs ++ [] = xs
	append_nil {xs = []} = Refl

	#lang racket/gui

	;;; Files part

	(define (image-files-list dir)
	(filter (lambda (p) (let ([ext (bytes->string/utf-8 (path-get-extension p))])
	(or (string-ci=? ext ".jpg") (string-ci=? ext ".jpeg") (string-ci=? ext ".png"))))
	(directory-list dir #:build? #t)))

	(define images-top (map read-bitmap (image-files-list "top")))

	theory Demo
	imports Predicate_Compile Extraction
	begin

	datatype 'a list = Nil
	\| Cons (head: 'a) (tail: "'a list")
	for map: lmap

	primrec append :: "'a list ⇒ 'a list ⇒ 'a list" where
	"append Nil ys = ys"