K
Ладно, для курсовой это перебор...
Да и это Gallina, а не скала
Size: a a a
2020 September 09
AT
Да и это Gallina, а не скала
А если статью прочитать? 😉
AT
Дак и в статье код на Gallina. Имеется ввиду "портировать это на скалу"?
A
Люди довольно часто делают параллельные открытия, тут никто не застрахован от "игнорирования чужих трудов". Нельзя читать всего, и знать, что Вася Пупкин уже где-то об этом хорошо написал. Насчет "это не важно" - я бы пересмотрел доклад
я недавно был свидетелем одной похожей локальной истории, но там акцент был на том, что представители индустрии сознательно делали акцент на "это не важно" вместо того, чтобы ознакомиться со статьёй.
забегая вперёд, скажу, что для тех людей из индустрии всё плохо закончилось. они понесли убытки, а их код, на словах приносящий value, мало того, что не смогли продать, его вообще задепрекейтили.
забегая вперёд, скажу, что для тех людей из индустрии всё плохо закончилось. они понесли убытки, а их код, на словах приносящий value, мало того, что не смогли продать, его вообще задепрекейтили.
AV
Убытки плохо, но обычно в таких случаях есть прибыль и это считается успехом
AV
Твой код задепрекейтили, не надо поддерживать — а у тебя прибыль, не это ли success, о котором многие мечтают
AV
Они устроились в другие места на не менее хорошие позиции
AT
Дак и в статье код на Gallina. Имеется ввиду "портировать это на скалу"?
Аблаапс — это скала-контора, а тот код на Coq просто попытка формально доказать нужные свойства. Я как-то пару-тройку раз с автором общался.
AT
Вот оно чо
истинно говорю
АГ
конкретно ту команду распустили совсем
Уверен, что некая истина из пейпера мало бы изменила ситуацию
АГ
Это не так работает обычно
АГ
И "задепрекейтили код" - это звучит как-то ненатурально, и есть ощущение, что этим словом должно быть "код не пошел в прод, его выбросили". Повторю, это такое ощущение, потому что я не склонен думать, будто пейперы имеют ажно силу политического актора
АГ
Причем непрочитанные пейперы
АГ
У меня есть сомнения, что ты не натягиваешь сову на глобус. Люди имеют право сомневаться