сунул в unwrap руку unwrap

unwrap за руку unwrap unwrap

Явный кликбейт, но возможно стóит просмотра.

Там, где одни видят проблемы, другие находят возможности!

Однажды Де Морган столкнулся с такой задачкой...

Началось всё с проблемы четырёх красок. Это довольно трудная задача, об которую сломали головы не одна сотня исследователей, она формулируется очень просто, впервые озвучена в 1852-м, но доказать её потребовалось довольно много десятков лет (не так, как для теоремы Ферма, но тоже хадкорно). Вот она:

Верно ли, что любую карту на плоскости или сфере можно раскрасить с помощью только 4х красок так, что если области имеют общую границу, то они разного цвета

И вот в 1976 году было предоставлено доказательство, которое выглядело так, что любая карта (а точнее граф) сводилась к одному из примерно 1936 случаев, а затем каждый из случаев был доказан с помощью компьютерной программы.
Это породило нешуточный срач, многие математики не приняли эту новаторскую идею, потому что
1. А вдруг алгоритм содержит ошибку, а вручную проверить все 1936 случаев руками этот алгоритм почти невозможно
2. А вдруг реализация алгоритма содержит ошибку?
3. А вдруг сам процессор содержит ошибку?

Финальную точку и поставило появление Coq, в отличие от других программ он содержал доказательство самого себя и кроме этого ещё и достаточно скрупулёзно исследован. Было сделано доказательство для проблемы 4х красок и теперь возможность для ошибки стала ничтожной, во всяком случае не существует техники доказательств, которая бы обеспечивала меньшую возможность для ошибок.

Например для РФ

Дыры в системах типов Java и Scala. Когда практики берутся за статическую типизацию без хорошо проработанной теории, выходит такое (Scala, по-видимому, вынуждена была включить джавовские типы для интеропа).

А можно пример такой парадоксальной системы типов?

@hirrolot устраивает ужас среди ничего не подозревающих растишек

Hirrolot, [06.07.20 18:06]
можно о лайфтаймах не заботиться

Hirrolot, [06.07.20 18:07]
давай, будешь senior poica developer

Hirrolot, [06.07.20 18:11]
https://gist.github.com/Hirrolot/fe752e0e0d58c3b0786f6b8a6ee58cb8
(ошибка на 1433 строки)

✊🙏😱
===
via https://www.tg-me.com/rust_offtopic/307844

О проблемах в поиске мейнтейнеров для ядра (Линус Торвальдс сетовал в своём интервью здесь)

>>>> Снизился порог входа и стало много временных молодёжных, модных, не особо развитых. В общей массе стало меньше доля людей университетского уровня. И искать стало сложнее.

>>> А как же инклюзивность и толерантность? Неужели гендерно-, расово- и умственно-альтернативные не могут писать код?

>> Вот в том и проблема, что все инклюзивные и толерантные, а мэйнтейнер должен на говно говорить говно.

> Официант! Бутылку чаю этому анониму за то, что зрит в корень.

===
из комментов

Ой 🙄😆, Ц++ не на высоте, лул

Αλεχ Zhukovsky:
я без мув конструктора? Просто я хочу написать функцию auto vectorToString(auto vector) -> auto

fn vectorToString(v: Vec<u8>) -> String {
let result = String::from_raw_parts(v.as_mut_ptr(), v.len(), v.capacity());
mem::forget(v);
result
}

как такую функу написать в плюсах?

Roman Proskuryakov:
кажется, что нельзя

наверно можно через черную магию, но сам понимаешь))

===

Танк развёл на арифметику

Нет, неправильно.
Дело не в том, что не имеет смысла, а в том, что как бы ты ни определил значение выражения a/0, ты всегда придёшь к противоречию.

Если a != 0, то x = a/0 определяется как решение уравнения x * 0 = a, которое не имеет решения ни при каком x.

Если a == 0, то x = 0/0 теоретически можно определить как любое число, но тогда ты придёшь к противоречию, что выражение 0/0 равно одновременно двум числам.

Если ты определишь a/0 как множество чисел, то получается, что значением операции / является множество, то есть операция не замкнута на множестве R.

В комплексных числах, однако, рассматривают множество C+ - это все числа и ещё одна точка ∞, так что C+ изоморфно сфере. Там на 0 делить можно.
https://en.m.wikipedia.org/wiki/Riemann_sphere