Forwarded from Alexander Chichigin
В очередной раз порекомендую прекрасную https://mirrors.edge.kernel.org/pub/linux/kernel/people/paulmck/perfbook/perfbook.html 😊
Forwarded from 𝙽𝚒𝚌𝚔 𝙻𝚒𝚗𝚔𝚎𝚛
Началось всё с проблемы четырёх красок. Это довольно трудная задача, об которую сломали головы не одна сотня исследователей, она формулируется очень просто, впервые озвучена в 1852-м, но доказать её потребовалось довольно много десятков лет (не так, как для теоремы Ферма, но тоже хадкорно). Вот она:
Верно ли, что любую карту на плоскости или сфере можно раскрасить с помощью только 4х красок так, что если области имеют общую границу, то они разного цвета
И вот в 1976 году было предоставлено доказательство, которое выглядело так, что любая карта (а точнее граф) сводилась к одному из примерно 1936 случаев, а затем каждый из случаев был доказан с помощью компьютерной программы.
Это породило нешуточный срач, многие математики не приняли эту новаторскую идею, потому что
1. А вдруг алгоритм содержит ошибку, а вручную проверить все 1936 случаев руками этот алгоритм почти невозможно
2. А вдруг реализация алгоритма содержит ошибку?
3. А вдруг сам процессор содержит ошибку?
Финальную точку и поставило появление Coq, в отличие от других программ он содержал доказательство самого себя и кроме этого ещё и достаточно скрупулёзно исследован. Было сделано доказательство для проблемы 4х красок и теперь возможность для ошибки стала ничтожной, во всяком случае не существует техники доказательств, которая бы обеспечивала меньшую возможность для ошибок.
Верно ли, что любую карту на плоскости или сфере можно раскрасить с помощью только 4х красок так, что если области имеют общую границу, то они разного цвета
И вот в 1976 году было предоставлено доказательство, которое выглядело так, что любая карта (а точнее граф) сводилась к одному из примерно 1936 случаев, а затем каждый из случаев был доказан с помощью компьютерной программы.
Это породило нешуточный срач, многие математики не приняли эту новаторскую идею, потому что
1. А вдруг алгоритм содержит ошибку, а вручную проверить все 1936 случаев руками этот алгоритм почти невозможно
2. А вдруг реализация алгоритма содержит ошибку?
3. А вдруг сам процессор содержит ошибку?
Финальную точку и поставило появление Coq, в отличие от других программ он содержал доказательство самого себя и кроме этого ещё и достаточно скрупулёзно исследован. Было сделано доказательство для проблемы 4х красок и теперь возможность для ошибки стала ничтожной, во всяком случае не существует техники доказательств, которая бы обеспечивала меньшую возможность для ошибок.
Дыры в системах типов Java и Scala. Когда практики берутся за статическую типизацию без хорошо проработанной теории, выходит такое (Scala, по-видимому, вынуждена была включить джавовские типы для интеропа).
Forwarded from Doctor Foland
А можно пример такой парадоксальной системы типов?
Forwarded from The Wacky Yellow Dog
кучу ранних систем типов от конструктивистов (system U, которая): https://en.wikipedia.org/wiki/System_U
Java, Scala и им. подобные с wildcard'ами: https://io.livecode.ch/learn/namin/unsound?img=#c38688f047a9dd46bd79f4d8262e53a2
Scala + type projection: https://lptk.github.io/programming/2019/09/13/type-projection.html
Java, Scala и им. подобные с wildcard'ами: https://io.livecode.ch/learn/namin/unsound?img=#c38688f047a9dd46bd79f4d8262e53a2
Scala + type projection: https://lptk.github.io/programming/2019/09/13/type-projection.html
Wikipedia
System U
special forms of a typed lambda calculus
@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://t.iss.one/rust_offtopic/307844
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://t.iss.one/rust_offtopic/307844
Gist
macro-error
GitHub Gist: instantly share code, notes, and snippets.