dennisgorelik: (2009)
Dennis Gorelik ([personal profile] dennisgorelik) wrote2016-08-21 03:47 pm
Entry tags:

Найм математика в софтверный бизнес - преимущества и недостатки

Очень откровенный (и интересный) "разбор полётов":
http://maxim.livejournal.com/484972.html

> человеку, котрый прикоснулся к созданию прувера, уже тяжело себя заставить писать обычные Web приложения на джава-скрипте

Вот такая странная мотивация у математиков.

> мы договорились, что я ему перечисляю "на еду" (как он выразился деньги) в размере 2000 грн в неделю.

Это меньше $400/месяц.
Что делает найм энтузиастов-математиков очень привлекательным.
При условии, что есть возможность достичь практический результат.

> С начала года прошла 31 неделя и было выплачено 65,149 грн. Получается 2101,5 копеек.

$2580 - чувствительно, но не много для неудавшегося бизнес-эксперимента.

> я не получил алгоритм кодировки, который был бы понятен условному Кметту. Павел говорит, что у него он в ЖЖ

Это типичная проблема с абстрактными теоретиками. Они получают удовольствие от теоретических исследований, но не любят тратить своё время на изложение своих достижений в виде, понятном простым смертным (таким, как их работодатель).


Thanks to thedeemon and juan_gandhi

[identity profile] maxim.livejournal.com 2016-08-21 10:58 pm (UTC)(link)
Я не понимаю, в чем идея камента Хуана Ганди, но суть вроде такая, что запретительная статья дла λP2, а λPω такая статья не запрещает, а у нас не просто λPω=CoC (с двумя вселенными), а с бесконечным их количеством. Если Хуан Ганди считает мое мнение аргументации (я не говорю о мотивации постановки задачи), пусть потрудится указать на ошибку в моих логических рассуждениях о возможной поставке проблематики (я не говорю что у меня есть готовое решение). Но запретительной статьи именно на невозможность построение терма индукции (или Sigma типа выраженного только на Pi) в CoC + predicative hierarchy of universes, насколько я знаю не существует. Или, если он возьмется за $100/час на 4 часа ее расписать (показать что не существует во всех кодировках (в статье только за Черч Нумералы идет речь, т.е. кодировка без конгруэнтности например), чтобы это не была белетристика или Дилберт в картинках), я с радостью заплачу назамедительно сумму (за 4 часа) и признаю что я нижайший пидоро-червь на планете :-)

Вот линк статьи:
http://www.cs.ru.nl/~herman/PUBS/IndNonder.ps.gz

http://maxim.livejournal.com/485410.html
Edited 2016-08-22 00:16 (UTC)

[identity profile] juan-gandhi.livejournal.com 2016-08-22 12:21 am (UTC)(link)
Я уже сообщал, что я не специалист в этой области, и могу только делиться подозрениями да удивляться смелости подхода. Делайте на здоровье; я точно не планирую лезть с советами в этой области. Мое мнение в этой области совершенно нерелевантно.

P.S. 100 в час - это какой-то странный рейт. Столько получают младшие джава-программисты, мне кажется.

[identity profile] maxim.livejournal.com 2016-08-22 12:24 am (UTC)(link)
Не я озувил этот рейт, а Денис. Но в прочем меня любой рейт устроит если будет какая-то ставка на рейт.
Главное чтобы натуральная, а не трансфинитные числа.

[identity profile] gineer.livejournal.com 2016-08-22 01:50 pm (UTC)(link)
Не настоящий сварщик, но глянул. %)

Я так понимаю что они там используют тот же механизм "представить все возможные теоремы в виде натуральных чисел, и доказать недоказуемое исходя из их свойств" что и у Геделя. ;)

Ну как бы ХЗ.

С т.з. математики это давно уже притча во езыцех... вон и Ганди потому завелся, почуял кровушку, математик. %)

А программистам подобным вообще как-то не пристало заморачиватся.

ЗЫ Как бы... не понятно чего они там хотят добится -- явный же висяк метатся, то есть мертвец висящик, висяк мертвецкий...
а они проуют как-то на кривой козе пропетлять. %)

Что напоминает мне, из моего аутсорсного опыта, то как чудаки неместные, заказывают мастарам молотка и зубила местным... зафигачить им свою версию Фэйсбука, на РНРхе %)))