s
А не эти ваши пруверы.
Size: a a a
2021 March 26
AG
я в общем к тому что формальная верификация как мне кажется должна всё таки больше налегать на софт
МБ
Большинство современных доказательств принимаются на веру, не редки случае когда выходят две статьи противоречащие друг другу в одном журнале
На веру? Это в каком таком журнале?
AG
а математики как нибудь сами подтянутся (ну или нет)
M
Не понимаю как интуиция противоречит солверам, сеньор разрабы тоже архитектуру интуитивно подбирают на основе опыта и каких то наитий
M
Короче мотивации странные, время конечно все рассудить но звучит как оправдания каболистов или с++ ранней эпохи
s
Потому, что Mathematica позволяет найти решение, когда же пруверы пригодны лишь для того, чтобы доказывать вещи вроде (a + b) + c = a + (b + c).
AG
Эх, если бы...
ну тут я думаю просто нет одной математики
AG
условные топологи конечно более настроены на такой поиск чем условные числотеоретики
s
Причём зачастую доказывать руками.
МБ
Ну, я просто к тому, что терминологию переизобретают везде. Это не только болезнь программистов. У математиков терминология тоже порой долго сходится. Пример: матрицы. Их изобретали в куче разных видов. Да и до сих пор переизобретают. Я к тому, что это нормально. Не стоит заморачиваться уж чрезмерно. Если видна взаимосвязь, покажите её, скорее всего, человек с удовольствием воспользуется.
s
Оригинальный контекст был «давайте не переводить quantified как квантифицированный, ведь разработчики испугаются слова из матлогики». Это уже не переизобретение по незнанию, а прямое вредительство.
МБ
Оригинальный контекст был «давайте не переводить quantified как квантифицированный, ведь разработчики испугаются слова из матлогики». Это уже не переизобретение по незнанию, а прямое вредительство.
А в каком предложении?
s
Переслано от Alexander Tchitchigi...
"Квантифицированные" они. Не выдумывайте, пожалуйста. 😊 Посмотрите как в книжках по логике пишут.
s
Не думаю, что подвязывать изучение языка ко книжкам по логике - хорошая идея. Если что-то можно объяснить простым языком, то лучше так и поступить. Даже если пишите книжку по логике.
s
Переслано от Александр
Логика бывает разная и подвязывать перевод к формальным языкам академично, но отнюдь не педагогично, проще говоря давая малоассоциативный перевод вы повышаете порог входа, создаёте читателю трудности, а порой и вынуждаете просто сомневатся состоятельности русского перевода, т.к. новояз для читателя ничем не лучше чем оригинал.
s
«Не педагогично», видите ли, использовать слова из логики.
s
Когда математики произносят слова вроде «предпучок», они не заботятся от «педагогичности».
s
Связи между областями важнее.
s
Но программисты — как же так, им же будет страшно от таких слов, как «квантифицированный»!