![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
dennisgorelikОчень откровенный (и интересный) "разбор полётов":
http://maxim.livejournal.com/484972.html
> человеку, котрый прикоснулся к созданию прувера, уже тяжело себя заставить писать обычные Web приложения на джава-скрипте
Вот такая странная мотивация у математиков.
> мы договорились, что я ему перечисляю "на еду" (как он выразился деньги) в размере 2000 грн в неделю.
Это меньше $400/месяц.
Что делает найм энтузиастов-математиков очень привлекательным.
При условии, что есть возможность достичь практический результат.
> С начала года прошла 31 неделя и было выплачено 65,149 грн. Получается 2101,5 копеек.
$2580 - чувствительно, но не много для неудавшегося бизнес-эксперимента.
> я не получил алгоритм кодировки, который был бы понятен условному Кметту. Павел говорит, что у него он в ЖЖ
Это типичная проблема с абстрактными теоретиками. Они получают удовольствие от теоретических исследований, но не любят тратить своё время на изложение своих достижений в виде, понятном простым смертным (таким, как их работодатель).
Thanks to thedeemon and juan_gandhi
http://maxim.livejournal.com/484972.html
> человеку, котрый прикоснулся к созданию прувера, уже тяжело себя заставить писать обычные Web приложения на джава-скрипте
Вот такая странная мотивация у математиков.
> мы договорились, что я ему перечисляю "на еду" (как он выразился деньги) в размере 2000 грн в неделю.
Это меньше $400/месяц.
Что делает найм энтузиастов-математиков очень привлекательным.
При условии, что есть возможность достичь практический результат.
> С начала года прошла 31 неделя и было выплачено 65,149 грн. Получается 2101,5 копеек.
$2580 - чувствительно, но не много для неудавшегося бизнес-эксперимента.
> я не получил алгоритм кодировки, который был бы понятен условному Кметту. Павел говорит, что у него он в ЖЖ
Это типичная проблема с абстрактными теоретиками. Они получают удовольствие от теоретических исследований, но не любят тратить своё время на изложение своих достижений в виде, понятном простым смертным (таким, как их работодатель).
Thanks to thedeemon and juan_gandhi
no subject
Date: 2016-09-04 02:15 am (UTC)Написание ответного комментария - совсем не обязательно то же самое, что ответ на вопрос.
> Может тебя просто ответы мои неустроили?
Верно, не устроили, потому что чрезмерно поверхностные ответы, не отражающие суть вопроса и ответа.
> Или ты из тех, кто любит на количество каментов в своем блоге любоваться?
Нет.
Я бы предпочёл, чтобы ты отвечал по существу, а не вертелся как уж на сковородке.
no subject
Date: 2016-09-04 02:19 am (UTC)Ты в ответ мне сказал что и так задал дохуя вопросов.
Я считаю что дальше разговривать нет смысла.
Так как я могу ответить только на 1 вопрос, а на 20 уже нет. Прости.
no subject
Date: 2016-09-04 02:24 am (UTC)А утверждение - было поясняющим.
> Прости.
Я прощаю тебя за твоё враньё.
no subject
Date: 2016-09-04 02:27 am (UTC)Ответ же простейший. Я читал что пишет Ганди про Харуна. И видел чем занимается Паша.
Для меня ответ очевидный, что умнее Паши я не видел человека за последние несколько лет.
Любая обезьяна которая пишет вместе с Ганди scala-лапшу в его стиле даже рядом по моим оценкам не может стоять с Павлом.
Надеюсь что помог тебе разобарться с твоим пазлом.
Пока.
no subject
Date: 2016-09-04 02:59 am (UTC)Я этот вопрос вообще не задавал.
Хотя и этот вопрос интересный.
> И видел чем занимается Паша.
Без деталей - это очень субъективно.
И совершенно неприменимо к другим работодателям, нанимающих специалистов.
Было бы интересно узнать, чем бы тебе мог быть практически полезен Паша если бы у вас всё получилось.
no subject
Date: 2016-09-04 03:14 am (UTC)вот это хороший вопрос. Задача Паши была сделать кодировку Черча (неприменимую в продакшине из-за неэффективности) для зависимой теории с построениями теормов индукции. Это невыполнимая задача, потому что в нашем ядре нет вообще ничего кроме чистой лямбды. Поэтому мы обогатили кодировку типов всеми необходимыми нам свойствами и скомпилировали терм индукции, который вычисляется как лимит тождественного функтора в категории алгберы заданного индуктивного типа. Другими словами построено равенство, модель теории категорий и на ней написали взятие лимитов, как микропрограмма для прошивки в чистой лямбде. Вот для этого и был нужен Паша.
no subject
Date: 2016-09-04 03:53 am (UTC)Что практически полезного твой бизнес бы научился делать?
no subject
Date: 2016-09-04 03:57 am (UTC)Как вообще могла возникнуть мысль, что мы пытаемся заработать на разработке языка с зависимыми типами?
Каким нужно быть долбоебом чтобы так подумать?
no subject
Date: 2016-09-04 04:09 am (UTC)Это напрямую следует из определения:
------
https://www.google.com/search?q=research+and+development
Research and development - (in industry) work directed toward the innovation, introduction, and improvement of products and processes.
------
То есть цель R&D - улучшать продукты и процессы.
А то, что тебе такая мысль даже в голову не приходила, говорит о том, что ты - псевдо-исследователь.
Исповедующий карго-культ.
Все теоретические изыскания имеют смысл только при применении их к реальности. Если нет проверки теории на практике - к научным исследованиям это отношения не имеет.
> Как вообще могла возникнуть мысль, что мы пытаемся заработать на разработке языка с зависимыми типами?
Из того, что ты, предположительно, занимался бизнесом.
Бизнес подразумевает в качестве одной из ключевых целей - извлечение прибыли.
Но теперь я понимаю, что бизнесом ты тоже не занимался.
Похоже ты просто сидел на титьке у головной конторы и развлекался псевдоисследованиями.
Но после нескольких месяцев облапошивания тобой, твои корпоративные спонсоры прозрели и прикрыли краник.
Ну и Пашу, соответственно, пришлось уволить.
no subject
Date: 2016-09-04 04:16 am (UTC)Ну какая-то часть правды в этом есть. Впринципе со стороны такой взгляд ок.
Назови мне хоть одну компанию которая заработала на продаже языков.
Конечно у создании языка есть цель, в данном случае — это повышение качества.
Бизнесу повезет если перепишем KVS на любой язык с типами.
А если докажем хоть одну теорему с экстрактом в Эрланг — то это вообще песня будет.
Если будет эффективно — это еще сутпенька.
Но EXE и то чем занимался Паша выходит за рамки этого. Далеко-далеко.
no subject
Date: 2016-09-04 05:51 am (UTC)Microsoft.
Только продают они языки не напрямую, а как часть платформы Windows.
Или T-SQL как часть SQL Server.
> Бизнесу повезет если перепишем KVS на любой язык с типами.
В каких практических достижениях будет выражаться это "перепишем KVS на любой язык с типами"?
> докажем хоть одну теорему с экстрактом в Эрланг — то это вообще песня будет
Какая практическая польза будет от такой "песни"?
> Но EXE и то чем занимался Паша выходит за рамки этого
У этого "выхода за рамки" - есть какая-то практическая цель?
no subject
Date: 2016-09-04 01:45 pm (UTC)Хотя SQL сервер — это продукт, и ты можешь его использовать без T-SQL а используя скажем Linq.
T-SQL отедльно не продается, как и не продается F*, F#, C#, WMI Script, Jet (база реестра) и NTFS язык запросов.
Haskell — это тоже продукт Microsoft и на нем она тоже не зарабатывает.
Microsoft начиналась как компания которая собирается продавать BASIC, но сейчас ни одна компания не зарабатывает деньги на языках — это просто невозможно.
Зарабатывать можно только на продуктах. Практические цели? Отсувствуе ошибок. Тот кому надо 100% гарантия отсутвтвия ошибок в коде, тому этот проект может быть инетерсен. Вот и все практические достижение.
no subject
Date: 2016-09-04 05:27 pm (UTC)Как использовать SQL Server без T-SQL?
Данные же нужно как-то из базы данных извлечь.
Linq применяется уже на стороне клиента.
> T-SQL отедльно не продается
Это же не значит, что T-SQL вообще не продаётся.
> Отсувствуе ошибок. Тот кому надо 100% гарантия отсутвтвия ошибок в коде
Это 100%-е "Отсувствуе" ошибок с двумя грамматическими ошибками в одном слове звучит довольно забавно.
Ну и "100%-я гарантия отсутствия ошибок в коде" - это же как обещание построить вечный двигатель второго рода. Теоретически возможно, но практически невероятно для любой достаточно сложной программы.
no subject
Date: 2016-09-04 06:32 pm (UTC)no subject
Date: 2016-09-04 07:42 pm (UTC)Хотелось бы более детального комментария.