ruby pearls

[sassa_nf]

2.2.0 :004 > ':xyz'.split(/:/)[0]
=> ""
2.2.0 :005 > ''.split(/:/)[0]
=> nil
2.2.0 :006 > 'xyz'.split(/:/)[0]
=> "xyz"

2.2.0 :001 > weak_key = lambda {|c| c.split(/:/, 2)[0]}
2.2.0 :002 > weak_key('xyz:1986')
NoMethodError: undefined method `weak_key' for main:Object

2.2.0 :003 > def weak_key(x

Comments

[nivanych]

> sound реализации исчислений возможны только в пруверах

Нет совести и контроля? ;-)
Ну так без инструментов такое доказывать совсем тяжело.
Хоть можно проверить правильность доказательства, это как минимум.
На практике, я уверен, что при таких разработках, сейчас любой возьмёт себе какой-то инструмент в помощь.

http://ru.wikipedia.org/wiki/Эрланг
А я и не знал ;-)

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

> industrial unsound provers :)

С вероятностью чтоб просчитывали, что ли?...
Это тестирование получается ;-)
Не совсем, но близко ;-)
Ну или чтоб prover содержал баальшой и хорошо документированный (иначе не industrial!) список исключений из правил. Ну и что, что вся теория вырождается от этих исключений, надо просто аккуратнее! ;-)

Исчисление процессов, это очень не всё, что нужно для распределёнщины.
Это только нижний уровень, база, "ассемблер".
Хотя и конечно, если он весь из себя чОткий, то это сильно упрощает дальнейшую с ним работу.

[nponeccop]

> industrial unsound provers :)

Unsound - это если доказательство, что код удовлетворяет спецификации, не означает, что код удовлетворяет спецификации.

Например, части доказательства, написанные в субботу вечером, используют технику доказательства "мамой клянусь".

[nponeccop]

> Нет совести и контроля?

Не совсем. Необходимо, чтобы в военное время синус мог достигать четырёх.