Size: a a a

2020 March 05

Т8

Т-34 85 in rust_offtopic
Gymmasssorla
вопрос остался
Потому что вряд ли получится сформулировать теорему
источник

G

Gymmasssorla in rust_offtopic
Т-34 85
Потому что вряд ли получится сформулировать теорему
почему?
источник

DF

Dollar Føølish in rust_offtopic
Танк зачем ты все это пишешь
источник

DF

Dollar Føølish in rust_offtopic
Мы ведь поняли уже что ты не знаешь ни с++ ни раста
источник

Т8

Т-34 85 in rust_offtopic
Gymmasssorla
чтобы не писать тесты, а писать теоремы (которые ты сам не доказываешь, а с помощью специального софта). тесты пишет человек, они могут быть ошибочными и почти всегда покрывают далеко не все сценарии, теоремы в этом плане выигрывают
Это слишком долго, заёбищино, не каждый потянет
источник

G

Gymmasssorla in rust_offtopic
Т-34 85
Это слишком долго, заёбищино, не каждый потянет
понял, спасибо, давно хотел услышать мнение человека, не раз писавшего верифицированное ПО и обучавшего этому новичков
источник

G

Gymmasssorla in rust_offtopic
Wikipedia
Эффект Даннинга — Крюгера
Эффект Да́ннинга — Крю́гера — метакогнитивное искажение, которое заключается в том, что люди, имеющие низкий уровень квалификации, делают ошибочные выводы, принимают неудачные решения и при этом неспособны осознавать свои ошибки в силу низкого уровня своей квалификации . Это приводит к возникновению у них завышенных представлений о собственных способностях, в то время как действительно высококвалифицированные люди, наоборот, склонны занижать оценку своих способностей и страдать от недостаточной уверенности в своих силах, считая других более компетентными. Таким образом, менее компетентные люди в целом имеют более высокое мнение о собственных способностях, чем это свойственно людям компетентным (которые к тому же склонны предполагать, что окружающие оценивают их способности так же низко, как и они сами). Также люди с высоким уровнем квалификации ошибочно полагают, что задачи, которые для них легки, так же легки и для других людей.
источник

DS

Doge Shibu in rust_offtopic
Т-34 85
Потому что вряд ли получится сформулировать теорему
Теорема формируется на таких языках в качестве типов. Доказательством служит программа данного типа.

Как раз формулировки этих теорем достаточно просты, вопрос в доказательствах, т.к. они там немного своеобразные, но привыкаешь быстро.

Так что оно сильно менее нереалистичное, чем ты себе представляешь.
источник

T

Tux in rust_offtopic
красота :)
источник

T

Tux in rust_offtopic
Переслано от Tux
источник

Т8

Т-34 85 in rust_offtopic
Gymmasssorla
почему?
Ну, лично я не представляю, как что там можно сформулировать. Впрочем, наверное, я вообще слабо себе это представляю. Было бы интересно, если вы рассказали, как, скажем, менеджер памяти написать на нём
источник

G

Gymmasssorla in rust_offtopic
Т-34 85
Ну, лично я не представляю, как что там можно сформулировать. Впрочем, наверное, я вообще слабо себе это представляю. Было бы интересно, если вы рассказали, как, скажем, менеджер памяти написать на нём
да, статей мало таких. после хотя бы одного проекта на пруфах наверное напишу об этом
источник

Т8

Т-34 85 in rust_offtopic
Gymmasssorla
понял, спасибо, давно хотел услышать мнение человека, не раз писавшего верифицированное ПО и обучавшего этому новичков
Это сказал человек, который юзает указатели, как только борров чекер не скомпилил его ссылку
источник

G

Gymmasssorla in rust_offtopic
Т-34 85
Это сказал человек, который юзает указатели, как только борров чекер не скомпилил его ссылку
как только борроу чекер не скомпилировал мою ссылку, я устраняю ошибки компиляции
источник

Т8

Т-34 85 in rust_offtopic
Doge Shibu
Теорема формируется на таких языках в качестве типов. Доказательством служит программа данного типа.

Как раз формулировки этих теорем достаточно просты, вопрос в доказательствах, т.к. они там немного своеобразные, но привыкаешь быстро.

Так что оно сильно менее нереалистичное, чем ты себе представляешь.
Хотел бы посмотреть
источник

Т8

Т-34 85 in rust_offtopic
Gymmasssorla
как только борроу чекер не скомпилировал мою ссылку, я устраняю ошибки компиляции
Путём залезания в ансейф
источник

G

Gymmasssorla in rust_offtopic
Т-34 85
Путём залезания в ансейф
видишь в телоксиде хоть один ансейф?
источник

RP

Roman Proskuryakov in rust_offtopic
Т-34 85
Это единичный проект. А может, вообще единственный
hacl-star?)
источник

Т8

Т-34 85 in rust_offtopic
Tux
Переслано от Tux
Что пишешь?
источник

Т8

Т-34 85 in rust_offtopic
Gymmasssorla
видишь в телоксиде хоть один ансейф?
Что это такое? Твой проект?
источник