Могут ли быть программы корректными при отсутствии статической типизации?

да, разумеется.

Они могут быть корректными, но этого труденее добиться. С мнением по ссылке согласен.

Кстати, вроде в последнем Эрланге есть опциональная статическая типизация :)

могут.

по ссылке - фигня какая-то, аргументов нет вообще.

Динамическая типизация суть зло, развращающее программистов, и снижающее производительность кода.

> по ссылке - фигня какая-то, аргументов нет вообще.

Там всё нормально аргументировано.

проще искать ошибки по сообщениям компилятора, чем по багрепортам.

>Там всё нормально аргументировано.

Единственный аргумент:

>Как можно написать корректную программу, если язык позволяет допустить практически любую опечатку?

Не знаю как в Erlang, но в питоне язык не "позволяет допустить практически любую опечатку". Если имена различных объектов слабо различаются, то ССЗБ, тут и Си не поможет.

> проще искать ошибки по сообщениям компилятора, чем по багрепортам.

Угу, а потом за лесом объявлений и наследования интерфейсов пытаться разглядеть, что всего-то надо было несколько разных методов у объекта реализовать/вызвать...

Каждой задаче - свой инструмент - не забыли?

QNX-овцы доказали корректность кода на ассемблере, куда уж там...

Но вообще, динамическая типизация - не есть гут.

> Угу, а потом за лесом объявлений и наследования интерфейсов пытаться разглядеть, что всего-то надо было несколько разных методов у объекта реализовать/вызвать...

1) Проектировать не пробовали?

2) ООП должно умереть.

> Но вообще, динамическая типизация - не есть гут.

Так а что тогда? Статическая типизация тоже ведь имеет свои 
недостатки. Haskell? Нет нормальной реализации, на которой можно 
разрабатывать программы для продакшна. Ocaml если только, но синтаксис 
у него не самый простой...

> Haskell? Нет нормальной реализации, на которой можно разрабатывать программы для продакшна.

me удивился, чем это он зарабатывает деньги.

Вы GHC используете? Как по-вашему мнению, он готов для того, чтобы на нем начинать проект, не расходуется ли значительная часть времени на борьбу с ним же?

Я не понял, а в чём должна заключаться борьба?

> Я не понял, а в чём должна заключаться борьба?

Ну, например, чтобы можно было писать основываясь на спецификации, а
не на глюках, багах и способе их обхода, компилятораінтерпритатора.

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

Статическая типизация может только незначительно уменьшить количество очепяток, требуя взамен трудозатрат на объявления, в которых тоже могут быть очепятки. И от ошибок типов она полностью не избавляет, как уже обсуждалось ранее. Так что без разницы, и к надёжности типизация никакого отношения не имеет.

> Ну, например, чтобы можно было писать основываясь на спецификации, а не на глюках, багах и способе их обхода, компилятораінтерпритатора.

Гм. В GHC ОЧЕНЬ мало багов, по крайней мере, в тех фичах, возраст которых более года.

> Парниша похоже никогда не слыхал про другие ашыпки, кроме очепяток.

Опечатки - ерунда.

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

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

> Статическая типизация может только незначительно уменьшить количество очепяток, требуя взамен трудозатрат на объявления, в которых тоже могут быть очепятки.

Открой для себя вывод типов, при котором 99% объявлений становятся не нужны.

> И от ошибок типов она полностью не избавляет, как уже обсуждалось ранее.

С таким-то ником - ничего не поможет.

Могут ли быть программы корректными при наличии статической типизации?

Типизация в Haskell - это действительно большой помошник в поиске ошибок. Когда я впервые решил попробовать на нем писать, я нашел какой-то сборник простеньких задачек, со списками там что-то и т.д. Я решил первые двадцать, потом забил на задачки. Так вот, с первого раза у меня хер чего скомпилировалось, что и не удивительно, но после того, как я добивался компиляции, из 20-и 19 правильно работали. Одна содержала логическую ошибку, но ее я бы в любом языке допустил.

А что касается Эрланга, да, там опечататься можно очень сурово. Проще всего - в атоме. Или переменную случайно с маленькой буквы написать, так что это атомом станет. И пока на эту ошибку не напоришься, не выловишь. Хотя, опыт у меня скудноват.

> С таким-то ником - ничего не поможет.

а должно?

Просто любопытно: а где в Питере делают на Хаскеле что-то практическое? И что делают?