Comments 15
Все, как и мода, возвращается )))
Э.Дейкстра "Дисциплина программирования"
Д.Грис "Наука программирования"
Все то же самое, но подробнее, математичнее и систематичнее
За Гриса люто плюсую.
Мне особо доставляет перевод на русский язык Непейводы/Ершовой. Помимо того, что переводчик исправляет ошибки в материале, он ещё и комментирует, вроде такого:
Надо иметь в виду, что на английском программистском жаргоне ошибка называется словом bug (клоп), а отладка (debugging) в буквальном смысле означает «выведение клопов» — процедура сколь неизбежная, столь и малорезультативная.
https://youtu.be/PMj1dC5UP0U?t=1h52m9s одно из толкований происхождения именно слова "bug" (6мин)
А какие ещё есть версии происхождения термина кроме этой?
Что мне "нравится" в русскоязычных форумах/комментариях/обсуждениях: тема была одна (в данном случае доказательство правильности программ), но фокус обсуждения резко смещается в побочном направлении. То-ли сказать нечего, то-ли просто не интересно. Чем заниматься лингвистическими изысками, может все-таки, вернемся к теме? )))))
Да без проблем. Статья мне не понравилась, обобщение опыта может и хорошее, но на публику близко к бесполезному. Что из опыта один-к-одному сразу смог соотнести с текстом -- то и понятно было. Остальное - хотелось бы именно примеров и объяснений, а не тридесятое определение того, что такое рекурсивная функция.
Лично я начал заниматься математикой уже давно
Оно и видно. Подвёл всю статью под свою внутреннюю систему абстракций и понимания. Может быть я по обозначенным им лекалам неосознанно и работаю, но комментарий @Filipp42мне показался полезнее. Сам уже думаю в ту сторону, что надо (пусть не те логически строгие языки), но Haskell, да Rust распробывать. В конце концов, что в статье -- "мягкие" наставления для логики. И напротив: когда компилятор заставляет тебя жесткими правилами мыслить так, а не иначе.
Ещё Джон Бентли — «Жемчужины программирования» (глава 4).
механизм пошаговых рассуждений даст плоды, только когда вы сможете делать это на бессознательном уровне
Многие так и кодят.
Приветствую!
Существует язык программирования Lean 4. Он предназначен в первую очередь для того, чтобы при помощи него доказывать математические теоремы. Возможно, его использование может стать хорошей разминкой для ума.
Вот книжка по Lean и математической логике: https://suhr.github.io/tmath/
Вообще, есть такая штука, как зависимые типы. Они позволяют в типах выразить практически любое утверждение о программе, и чтобы программа скомпилировалась, выполнение этих свойств порой придётся доказывать. Это языки Idris, Lean, Coq, Agda. Lean мне кажется самым практичным из всех, хотя я трогал только Idris.
Тут главное не бояться! Это весело!
По Lean кстати есть и компьютерная игра: https://adam.math.hhu.de/
В ней нужно доказывать простые теоремы о натуральных числах и множествах.
Зачем в уме? IDE и язык должны предоставлять средства для этого.
Хотите эффективнее программировать? Учитесь строить в уме пошаговые доказательства