Файл: Мертвые языки программирования Гудушаури Отари 10А.pptx

Следующий слайд

К карте

Предыдущый слайд

ML

Разработчик: Робин Миллер, 1976.

Прежде чем создать ML, Милнер работал над LCF Prover — одним из первых помощников для доказательства теорем. LCF искал ошибки в доказательстве и проверял, правильно ли оно оформлено. Программист создал для него метаязык, основанный на надежных математических формализмах — строгих статических типах и функциях высшего порядка. Этот язык позже превратился в ML и был стандартизирован как SML.

Вклад: В ML была реализована одна очень важная идея: вывод типов. Это первый язык со статической типизацией, в котором не нужно определять типы — компилятор делал это автоматически. Эта идея заложила основу для типизированного функционального программирования.

ML оказал большое влияние на современные средства доказательства теорем: «программные» языки для Isabelle, CVC3 и Coq основаны на ML. Кроме того, на языке было создано множество теорий типов, хотя позже Haskell приобрел большую популярность среди математиков.

Причина смерти: У ML было много интересных функций, но он был языком специального назначения для доказательства теорем. SML вышел в том же году, что и Haskell, который оказался более «чистым» примером языка типизированного функционального программирования.

Следующий слайд

К карте

Предыдущый слайд

Вывод

Предыдущий слайд

Большинство влиятельных языков никогда не были популярными, но их ДНК проявляется спустя десятилетия после того, как они были забыты. Есть бесчисленное множество языков, идеи которых не были оценены, например, «Энциклопедия языков программирования» состоит из более чем 8 тыс. языков.

Спасибо за внимание!

---