Программирование - и есть математика, ибо является формальной записью алгоритмов и структур данных, изучаемых в курсе дискретной математики и иных дисциплин, являющихся частью математики. Что самое странное ,программирование и было изобретено математиками: Тьюрингом, Черчем, Клини, Карри, Генценом, Говардом и прочими. Но фантазировать никто не запрещает :)
Да не из логики наука вылезла, а из философии и алхимии, логика тут была на вторых ролях, ибо объясняла чуть менее, чем ничего. А религия - от безграмотности и желания управлять массами.
А, то есть, существует "просто логика", как некая универсальная сущность? :)
Вынужден разочаровать: логика состоит из мат. логики и силлогистики, замещенной матлогикой и логикой Лукасевича (введением неоднозначностей).
Увы, никаких универсальных самостоятельных идей, исключающих математику, нет - все давно хорошо записывается формально и преподается в вузах.
Не совсем понятно желание отвергать математику, являющуюся мощным инструментом и первым помощником в разработке софта. Ниасилятор, што ле? :)
Вот когда компьютеры будут понимать философские категории вместо формальных определений, тогда можно будет заниматься словоблудием. А пока - дискретка, теория типов и теория пруфов.
А логика - это раздел чего ? Пропозиционная логика - часть курса дискретной математики, если что :) А потом начнутся логика второго порядка, высшего порядка (доказательство кода и моделирование систем на ней основаны, а кое-где подключается вышка лямбда-куба - исчисление конструкций, а то и вообще HoTT/кубики) .
В некоей отечественной финтех-конторе технари аппрувят кандидата после слова "Coq" (умение или готовность его изучить и применить). Если добавить "Rust" (лучше - реальный скилл) - Вы приняты (если не запорете интервью с менеджментом) :)
Большой молодец, пишите еще, спасибо! Lean4 нравится тем, что готов к употреблению как ЯП с завтипами, а как пруф-ассистант мила Изабелла: AFP и seL4 весьма хороши и полезны
Пора брать Coq или Isabelle/HOL, Lean4, автор явно движется в правильном направлении :)
Выпил - отключи ингтернет (ц)
Программирование - и есть математика, ибо является формальной записью алгоритмов и структур данных, изучаемых в курсе дискретной математики и иных дисциплин, являющихся частью математики. Что самое странное ,программирование и было изобретено математиками: Тьюрингом, Черчем, Клини, Карри, Генценом, Говардом и прочими. Но фантазировать никто не запрещает :)
Да не из логики наука вылезла, а из философии и алхимии, логика тут была на вторых ролях, ибо объясняла чуть менее, чем ничего. А религия - от безграмотности и желания управлять массами.
А, то есть, существует "просто логика", как некая универсальная сущность? :)
Вынужден разочаровать: логика состоит из мат. логики и силлогистики, замещенной матлогикой и логикой Лукасевича (введением неоднозначностей).
Увы, никаких универсальных самостоятельных идей, исключающих математику, нет - все давно хорошо записывается формально и преподается в вузах.
Не совсем понятно желание отвергать математику, являющуюся мощным инструментом и первым помощником в разработке софта. Ниасилятор, што ле? :)
Вот когда компьютеры будут понимать философские категории вместо формальных определений, тогда можно будет заниматься словоблудием. А пока - дискретка, теория типов и теория пруфов.
А логика - это раздел чего ? Пропозиционная логика - часть курса дискретной математики, если что :) А потом начнутся логика второго порядка, высшего порядка (доказательство кода и моделирование систем на ней основаны, а кое-где подключается вышка лямбда-куба - исчисление конструкций, а то и вообще HoTT/кубики) .
Очень хороший пост, спасибо. Писателям хелловорлдов и формошлепам математика, разумеется, не нужна.
Не сказал бы, что очень долго и дорого, но воля Ваша. Ну что ж, пока потренируюсь, а потом можно будет и Isabelle :)
TLA+ не пробовали ?
Большое спасибо, пишите еще!
Мимо. Это не финтех. Еше попытка! :)
Знают, и очень хорошо. Начинается на "Ex... "
В некоей отечественной финтех-конторе технари аппрувят кандидата после слова "Coq" (умение или готовность его изучить и применить). Если добавить "Rust" (лучше - реальный скилл) - Вы приняты (если не запорете интервью с менеджментом) :)
Большой молодец, пишите еще, спасибо! Lean4 нравится тем, что готов к употреблению как ЯП с завтипами, а как пруф-ассистант мила Изабелла: AFP и seL4 весьма хороши и полезны
Молодец! СНГ! Пишите еще!
Да, все в порядке, моментально.
Очень хорошо, спасибо, ждем следующую часть. Тем временем, ковыряем Изабеллу и TLA+ :)
Большой молодец!
И это меня со столяркой на балконе и кожевенной мастерской дома называют сумасшедшим... :) Автору - всяческих успехов!
Шведский изучать надо обязательно - акторная модель ибо. Хаскелл и всё ML -семейство интересны, Lean4, Isabelle/HOL, Coq, Rust