ТЕХНОЛОГИИ УСПЕШНЫХ ПРОГРАММИСТОВ

Рекомендации
Тру:

Binary Protocols and Protocol Stacks (CORBA and SOAP Replacement)

— WebSocket
— SVG
— MQTT
— N2O
— ASN.1

Storage Systems (CODASYL and MUMPS Replacement)

— Aerospike (SSD)
— BlazingDB (GPU)
— PumpkinDB (FORTH, AVX) — лучший хакатон стартап на расте, авансом

Array Processing Languages (Fortran replacement)

— Futhark (GPU)
— Julia (AVX)
— AutumnAI (ML)

Concurrency Runtime and Languages (Ada Replacement):

— Pony (Runtime+Language, Erlang replacement, Zero Copy, CAS)
— Erlang, LING (Runtime+Language, Poor man)
— Rust (Language, Zero Copy)

R&D Languages (AUTOMATH replacement):

— Coq
— Z3
— Lean

Target Languages (Pascal Replacement):

— OCaml
— LLVM/MIR
— Rust
— D

New Markets (Inexistant satisfaction) — озеро, где живут Черные Лебеди:

— VHDL FPGA toolchain replacement
— SIP/VoIP replacement
— RTP replacement
— Xen, Hyper-V, EXSI replacement
— Wolfram Mathematica replacement
— Lisp Machine replacement

Для петухов:

— JSON, XML, MessagePack, Text Protocols, ...
— HTML, Virtual DOM, React, Angular, Any JavaScript Framework ...
— HTTP 1, 2, 3, 4, ...
— C-Style Languages: Go, C, C++, JavaScript, TypeScript, ES6, ASM.JS, ...
— All LISPs: Clojure, Common Lisp, Smalltalk, ...
— Big VMs: JVM, CLR, ...
— Просто унылое говно: C#, Java, PHP, Scala, Python, PHP, Ruby, Elixir, Perl, node.js ...
— All RDBMS: SQL, MySQL, PostgreSQL, Oracle, ...
— British Languages: Haskell, Agda, Idris, ...
— APL Languages: K, J, Q, APL, ...
— Almost all DHT: Riak, Cassandra, Spark, Hadoop, RethinkDB, CouchDB, Memcache, BDB, Tokio, MongoDB, Redis, ArangoDB, Neo4j, AllegroGraph, OrientDB, OrientDB
— Almost all serializers: gRPC, Protobuf, Thrift, ...
— Modern way of devops: Kubernetes, Docker, ...
— Any product built by Google: TensorFlow, Android, Blockly, Dart, Polymer,
— Big Operaing Systems: Linux, Windows, Mac

Список Обновляется. Коментарии Пендинг. Дискас.

>>972961 (OP)
Успех определяется уровнем жизни. С твоими тру технологиями можно разве что гнить в НИИ.

>>972961 (OP)
Репортов накидайте, это уже перебор

>>972961 (OP)
Все, что должен знать программист, чтобы его после 40 лет не выбросили на Помойку, Где Бомжи:
• C++, стандарт, Comeau, 1TBS, Страустрап/D&E/Джосаттис/Вандервуд, Дьюхэрст/Мейерс/Саттер, RAII/copy-and-swap/exception-safety, правило пяти, Александреску/Абрахамс-Гуртовой, type erasure, CRTP, NVI, SFINAE, Koenig lookup, Duff's device, Boost, Сик-Ламсдейн/Карлссон, TR on C++ performance, тест Степанова, forwarding problem/move semantics, SPECS, GotW, Meyer's singleton, cppgm
• Компиляторы С++, особенности реализации стандарта, ограничения реализации, интринсики, отличия стандартных библиотек (контейнеры, rand), ABI, реализация виртуальных функций, виртуального наследования, исключений, RTTI, switch, указателей на функции и методы; оптимизации, copy elision (RVO, NRVO), sizeof на различных платформах, дефайны компилятора и среды, __declspec, ключи компилятора, empty-base optimization, статическая и динамическая линковка, манглинг, распределенная компиляция, precompiled header, single compilation unit, (strict) aliasing/restrict, inline/_forceinline, volatile, быстрое вычисление математических функций через битхаки, linkers & loaders by Levine
• Мультитредность, обедающие философы, deadlock/livelock/race condition/starvation, атомарность, lock инструкции процессора, memory model/barrier/ordering, CAS или LL/SC, wait/lock/obstruction-free, ABA problem, написание lock-free контейнеров, spin-lock, TLS/per-thread data, закон Амдала, OpenMP, MPI, map-reduce, critical section/mutex/semaphore/condition variable, WaitForSingleObject/WaitForMultipleObjects, green thread/coroutine, pthreads, future/deferred/promise, модель акторов, parameter server, RDD (as seen in sparks), downpour SGD, wait-free, stackful vs stackless
• Язык ассемблера, Зубков/Хайд/Дреппер/Касперски/Фог/Абраш, x86, FPU/MMX/SSEn/AVX, AT&T и Intel-синтаксис, masm32, макросы, стек, куча/менеджеры кучи, соглашения вызова, hex-коды, машинное представление данных, IEEE754, little/big endian, SIMD, аппаратные исключения, прерывания, виртуальная память, реверсинг, срыв стека и кучи, return oriented programming, alphanumeric shellcode, L1/L2/RAM/page fault и их тайминг, язык ассемблера ARM
• Аппаратное обеспечение, Хоровиц-Хилл/Титце-Шенк/От физики к Си от panchul, полупроводниковая электроника/спинтроника/фотоника, транзистор, триггер, схемотехника, микрокод, технология создания процессоров, logic synthesis, static timing analysis, FPGA, Verilog/VHDL/SystemC, SISAL, Arduino, устройства памяти (ROM → EEPROM, RAM, SSD, HDD, DVD), RISC/CISC, Flynn's taxonomy ([SM]I[SM]D), принстонский и гарвардский подход, архитектуры процессоров, архитектуры x86, VID/PID
• Процессоры, конвейеризация, hyper-threading, алгоритм томасуло, спекулятивное исполнение, static/dynamic branch prediction, префетчинг, множественный ассоциативный кэш, кэш-линия/кэш-промах, такты, кольца защиты, память в мультипроцессорных системах (SMP/NUMA), тайминг памяти, intel optimization manuals, performance counters
• Дискретная математика, K2, теорема Поста, схемы, конечные автоматы (ДКА и НДКА), автомат Калашникова, клеточные автоматы
• Вычислимость, машина Тьюринга, нормальные алгоритмы Маркова, машина Поста, диофантовы уравнения Матиясевича, лямбда-функции Черча, частично рекурсивные функции Клини, комбинаторное программирование Шейнфинкеля, Brainfuck, эквивалентность тьюринговых трясин, проблема останова и самоприменимости, счетность множества вычислимых функций, RAM-машина, алгоритм Тарского, SAT/SMT-солверы, теория формальных систем, interactive proofs, теорема Левина-Кука, 3SAT, PSPACE = NPSPACE, #P
• Языки программирования, грамматики, иерархия Хомского, теорема Майхилла-Нероуда, лемма о накачке и лемма Огдена, алгебра Клини, НДКА → ДКА, алгоритмически неразрешимые задачи в формальных языках, Драгонбук, Фридл, регекспы и их сложность, PCRE, БНФ, Boost.Spirit + Karma + Qi/Ragel, LL, LR/SLR/LALR/GLR, PEG/packrat, yacc/bison/flex/antlr, статический анализ кода, компиляция/декомпиляция/обфускация/деобфускация, Clang/LLVM/XMLVM/Emscripten, GCCXML, OpenC++, построение виртуальных машин, JiT/AoT/GC, DSL/DSEL, on-stack replacement, type checking/type inference алгоритмы, CYK parser, advanced compiler design and implementation by Muchnick
• Алгоритмы и комбинаторная оптимизация, Кормен/Скиена/Седжвик/Кнут/Ахо-Хопкрофт-Ульман/Пападимитриу/Шрайвер-Голдберг/Препарата-Шеймос/e-maxx.ru, структуры данных, алгоритмы, сложность, символика Ландау, теорема Акра-Баззи, time-space tradeoff, классы сложности, NP-полные задачи, КМП, графы и деревья, потоки в сетях, матрица Кирхгофа, деревья поиска (особенно RB-дерево и B-дерево), occlusion detection, куча, хэш-таблицы и идеальный хэш, сети Петри, алгоритм русского крестьянина, метод Карацубы и матричное умножение Винограда-Штрассена, сортировки, жадные алгоритмы и матроиды, динамическое программирование, линейное программирование, diff-алгоритмы, рандомизированные алгоритмы и алгоритмы нечеткого поиска, псевдослучайные числа, нечеткая логика, gusfield (suffix tree, string alignment), motif search, scanning line, cache oblivious, funnel sorting, VEB-layout, корневая оптимизация, алгоритмы для динамических графов,
модели вычисления (RAM-machine/pointer machine/decision trees и т.д.), алгоритмы в иерархиях памяти/стриминговые алгоритмы, time forward processing, range & rank, LSM-trees, buffered a-b-trees, toku trees, персистентные структуры, succint-структуры, lossy-струтуры (bloom/bloomier filter, hash-tables with false positives), locality sensitive hashing, space-time tradeoff в хэш-таблицах, scheduling strategies
• Численные методы, дихотомия/метод Ньютона, интер- и экстраполяция, сплайны, метод Гаусса/Якоби/Зейделя, QR и LU-декомпозиция, SVD, МНК, методы Рунге-Кутты, метод Адамса, формулы Ньютона-Котеса, метод Ритца, метод Бубнова-Галеркина, метод конечных разностей/элементов, FFT/STFT, сходимость и устойчивость, l-bfgs и другие квазиньютоновские методы, adagrad, PARAFAC, cassowary, interior point methods, вариационные методы для байесовского вывода, nesterov, автоматическое дифференцирование, alternating least squares, what every computer scientist should know about floating point arithmetics by Goldberg, Nocedal & Wright/Boyd & Vandenberghe
• Машинное обучение, Тибширани/Bishop, подходы к моделированию AI, переобучение/кроссвалидация, байесовские сети, нейросети, сети Кохонена, Restricted Boltzmann machine, градиентный спуск/hill climbing, стохастическая оптимизация (метод Монте-Карло, метод отжига, генетические алгоритмы, муравьиные алгоритмы), SVM, gradient boosting, кластерный анализ, метод главных компонент, LSH, обучение с подкреплением, MDP, information retrieval/data mining/natural language processing, машинное зрение, Szeliski, OpenCV, image processing, OCR, фильтры Собеля, каскад Хаара, Viola-Jones framework, SURF, введение в психофизиологию зрения, IPython/pandas/scikit-learn, (ME)HMM, CRF, label bias problem, stacked NN, LeToR, factorization machines, autoencoders, RNN/CNN, вместо NLP лучше отдельные задачи (language modelling, co-reference detection, text chunking, POS-tagging, probabilistic parsing, statistical machine translation, misspell correction, question answering, NER, collocation detection, text summarization, speech recognition, fact extraction, sentiment analysis), эффективное вычисление softmax, feature engineering/selection, quality estimation, Manning/Jurafsky/McCallum/Koehn, latent topics (LDA, chineese restaurant, pLSI), parallel coordinates, vowpal wabbit, NLTK, structured learning, EM-алгоритм, contrastive divergence, optimal brain surgery, belief propagation, semi-supervised learning, inductive vs transductive learning, kernel trick, discriminative/generative pairs (as seen by Ng & Jordan), sequence to sequence learning, bagging, анализ социальных графов, рекомендательные системы/collaborative filtering, multimodal learning
• Теория информации, сжатие, Хаффман, RLE, BWT, LZ, коды коррекции ошибок, сжатие с потерями (изображения, аудио, видео), информационная энтропия, формула Шеннона, сложность Колмогорова, maximum entropy problem, kullback-leibler divergence, elias/shannon-elias encoding
• Криптография, Шнайер/Ященко, Принцип Керкгоффса, симметричная (DES, AES), асимметричная (RSA), качество ГПСЧ, алгоритм Диффи-Хеллмана, эллиптические кривые, хэширование (MD5, SHA, CRCn), DHT, криптостойкость, криптоатаки (атака гроссмейстера), WEP/WPA/WPA2 и атаки на них, цифровая подпись и сертификаты, PKI, HTTPS/SSL, доказательство с нулевым разглашением, пороговая схема, murmurhash/cityhash, DKIM
• Математика, Кнут-Грэхем-Паташник/Зорич/Винберг, Spivak/Dummit-Foote, матан, линал, комплан, функан, диффгем, теория чисел, дифуры/интуры/урчпы/вариационное исчисление/оптимальное управление, производящие функции, ряды, комбинаторика, теорвер/матстат/слупы/теория массового обслуживания, цепи Маркова, интегральные преобразования (Фурье, Лаплас, вейвлет), NZQRCHOS, матпакеты (Mathematica, Maple), теория категорий
• Физика, правила Кирхгофа, закон Джоуля-Ленца, комплексное сопротивление, скорость и частота света, уравнения Максвелла, лагранжиан и гамильтониан,
quantum tunnelling/hot electron injection :)
• Химия, стехиометрия, химия кремния :)

• Архитектура и стиль кода, Макконнелл/Фаулер/Лебланк/Гамма/Александреску-Саттер/Буч, защитное программирование, паттерны, SOLID/GRASP/KISS DRY SPOT/YAGNI, UML, OOP (Smalltalk), OOD/OOA, метрики кода, uncle Bob
• Методологии разработки, Waterfall/RUP/Agile/Scrum/Kanban/XP, TDD/BDD, CASE
• Тестирование, юнит-тесты, функциональное, нагрузочное, интеграционное тестирование, тестирование UI, mocks/stubs/spies, fixture, запахи и паттерны тестов (Osherove/Meszaros)
• Инструментальные средства разработки, IDE, IntelliSense, отладчики (VS/Olly/WinDbg/kdb/gdb) и трейсеры (strace/ltrace), DWARF debug information format, дизассемблеры и декомпиляторы (IDA/HexRays/Reflector), системы контроля версий (SVN, GIT), merge/branch/trunk, системы именования файлов и бранчей, continuous integration, ant, code coverage, статический анализ (lint, cppcheck), динамический анализ (valgrind, фаззинг), верификация и валидация ПО (Frama-C, RAISE (RSL), Coq), профайлинг, багтрекеры, документирование кода, системы сборки (CMake), пакетные менеджеры (NuGet)
• Фреймворки, Qt, moc и метаинформация, концепция слот-сигнал, Саммерфилд-Бланшет/Шлее, PoCo, промышленные библиотеки: GMP, i18n, lapack, fftw, pcre
• Операционные системы, Silberschatz/Рихтер/Соломон-Руссинович/Робачевский/Вахалия/Стивенс/Таненбаум/Love/Linux Kernel Internals, менеджер памяти, менеджер кучи и ее устройство (LAL/LFH/slab), менеджер устройств, менеджер процессов, context switch, реальный и защищенный режим, исполнимые файлы (PE/ELF/Mach), объекты ядра, отладочные механизмы (strace/ptrace/dtrace/pydbg, Debug API) и минидампы, bash, сетевой стек и высокопроизводительные сервера, netgraph, CR0, IPC, оконная подсистема, система безопасности: ACE/ACL и права доступа, технологии виртуализации, RTOS (QNX), программирование драйверов, IRQL, IRP, файловые системы, BigTable, NDIS/miniport/FS drivers/filter driver, Mm-, Io-, Ldr-функции, DKOM и руткиты, GDT/IDT/SDT, ядра Windows/Linux/BSD, POSIX, TRIM
• Компонентно-ориентированные модели, Роджерсон/Таварес, COM/OLE/ActiveX/COM+/DCOM RPC, ATL, апартменты, моникеры, MIDL, XPCOM, CORBA, TAO, D-Bus
• Сеть, Стивенс, OSI model/Internet model, Ethernet, TCP/IP, TCP window, алгоритм Нейгла, сокеты, Protocol buffers/Thrift/Avro/ASN.1, AMQP, ICMP, роутинг/BGP/OSPF, ARP, атака Митника, syn flood, HTTP/FTP, P2P/DHT, DHCP, SMB/NBNS, IRC/XMPP, POP3/SMTP/ESMTP/IMAP, DNS, WiFi/WiMax/GSM/CDMA/EDGE/Bluetooth/GPS, ACE, Wireshark
• Графика и GPGPU, алгоритм Брезенхема, цветовые модели, трассировка лучей vs полигональная графика, OpenGL/GLSL/Open Inventor, DirectX/DirectShow/DirectAudio/HLSL, stencil/depth/alpha-test, графический конвейер в DirectX 11, шейдеры, модели освещения (Фонг), пропускная способность, fillrate, OpenCL/CUDA/AMP, ландшафты, лоды, тени, deferred shading, текстурирование и фильтрация, антиалиасинг, HDR, tone mapping, virtual/augmented reality
• Форматы, XML/XSLT/XPath/XMLStarlet/DOM/SAX, RTF/ODF, JSON/BSON/bencode, YAML, JPEG/PNG/WebP, AVI/MPEG/RIFF/WAV/MP3/OGG/WebM, SVG, Unicode, кодировки однобайтные/UTF-8/UTF-16/UCS-2/UTF-32, проблемы длины и сравнения Unicode-строк, base64, markdown
• Базы данных/Распределенные системы, Грубер/Дейт, ANSI SQL, T-SQL, ODBC, MySQL/PostgreSQL/MS SQL/BDB/SQLite/Sphinx, хранимые процедуры, триггеры, алгебра Кодда/А, Tutorial D, нормальные формы, оптимизация и выполнение запросов, структуры данных индексов, транзакции и ACID, CAP-теорема Брюера, graph DB, document store, wide column store, key-value storage, теория распределенных систем, CRDT, net split проблема, протоколы консенсуса, теория шардинга/репликации, ORM (C++ ODB), ERD, OLAP, семантическая сеть, triplestore, RDF/Turtle, SPARQL, OWL, Semanticscience Integrated Ontology, reasoner, DBpedia, big table/hbase vs. dynamodb/cassandra/riak, 2/3PC, chubby/zoo keeper, leader election (paxos/raft), hdfs/gfs/glusterfs, deduplication problem, causality detection (vector clock/stamps), R/W quorum, load balancing, устройство индексов поисковых систем, event sourcing, CRDT, дизайн протоколов и принципы коммуникации, с точки зрения эволюции, расширяемости, надежности, дизайн программных интерфейсов (API)
• Прикладное программирование, C#/F#, Шилдт/Троелсен/Рихтер, генерики, yield, linq/plinq, рефлексия, AST, WCF, WinForms/WPF/Silverlight, AOP, фреймворки логгирования, .NET assembly, Scala, Хорстманн/Одерски, pattern matching, макросы/квазицитаты
• Квантовые вычисления, алгоритм Шора, квантовая криптография
• Функциональное программирование, Haskell/Ocaml/Scheme/Alice или Oz, SICP/TaPL/YAHT/Purely Functional Data Structures/Харрисон-Филд, HOF (map/fold/filter), система типов Хиндли-Милнера, монады, тайпклассы, АТД, dependent types, ленивость/энергичность, логическое программирование (Prolog или Mercury), конкурентное программирование (Erlang или Oz)
• Веб-программирование и скриптовые языки, Фланаган/Zend PHP5 Certification Course + Study Guide, Apache/nginx, CGI/FastCGI, PHP/Zend Framework/ReactPHP/Zend Engine/Doctrine или Propel/CodeIgniter или Symphony или Yii, Python/Django/Twisted, Ruby/RoR, ASP.NET MV*, JavaScript/jQuery/React/Google Closure/ExtJS/node.js, ООП в JavaScript, HTML5, CSS3/табличная и блочная верстка, RSS, canvas/WebGL, Ajax/WebSockets, вопросы безопасности (XSS, SQL injection, CSRF), highload, C10k problem, SWIG, CDN, shadow DOM, квирки браузеров, real time bidding/trading, anomaly detection, архитектура single page apps, устройство веб-краулеров, web/social graph random walk, asm.js и компиляция в js, v8/spidermonkey internals, PaaS/IaaS, SPDY
• Проектирование GUI и представление информации, Раскин/Тафти, юзабилити, основы дизайна и типографики, закон Фиттса, основы верстки, LaTeX, алгоритмы визуализации данных (as seen in d3), subpixel rendering

>>972976
>>972977

Все это знаю, но по прежнему хлебаю мамкины борщи.
А вот если бы осваивал технологии оп-поста то сейчас бы вяло попивал смузи с маффинами на сейшелах.

"Application Files"

Introduction

If you develop SWT applications, you know that SWT uses the native operating system controls and cannot easily be configured to use advanced GUI features, such as animation. You can quickly add sparkle to an SWT application by integrating JavaFX with SWT. All you need is the FXCanvas class from the javafx.embed.swt package. The javafx.embed.swt package can be found in jfxswt.jar, which is located in the JDK_Home/jre/lib/ directory. FXCanvas is a regular SWT canvas that can be used anywhere that an SWT canvas can appear. It's that simple.

In this article, you will see how to create an interactive SWT button and JavaFX button, shown in Figure 8-1.

Figure 8-1 SWT Button on Left, JavaFX Button on Right

Screenshot of the SWT and JavaFX buttons
When the user clicks either button, the text is changed in the other button, as shown in Figure 8-2 and Figure 8-3. This example shows how the SWT code and JavaFX code can interoperate.

Figure 8-2 Clicking the SWT Button Changes the JavaFX Button Label

Description of Figure 8-2 follows
Description of "Figure 8-2 Clicking the SWT Button Changes the JavaFX Button Label"

Figure 8-3 Clicking the JavaFX Button Changes the SWT Button Label

Description of Figure 8-3 follows
Description of "Figure 8-3 Clicking the JavaFX Button Changes the SWT Button Label"

Adding JavaFX Content to an SWT Component

In JavaFX, the Java code that creates and manipulates JavaFX classes runs in the JavaFX User thread. In SWT, code that creates and manipulates SWT widgets runs in the event loop thread. When JavaFX is embedded in SWT, these two threads are the same. This means that there are no restrictions when calling methods defined in one toolkit from the other.

Example 8-1 shows the code to create the SWT button and JavaFX button shown in Figure 8-1. As shown in the code, you set JavaFX content into an FXCanvas with the setScene() method in the FXCanvas class. To force SWT to lay out the canvas based on the new JavaFX content, resize the JavaFX content first. To do this, get the JavaFX Window that contains the JavaFX content and call sizeToScene(). When JavaFX is embedded in SWT, a new preferred size is set for FXCanvas, enabling SWT to resize the embedded JFX content in the same manner as other SWT controls.

JavaFX constructs content in terms of a hierarchical scene graph, placed inside a scene. The code in Example 8-1 places the JavaFX button into a scene with the scene graph shown in Figure 8-4 and described in comments in the code example.

Figure 8-4 JavaFX Scene Graph in SWT Application

Description of Figure 8-4 follows
Description of "Figure 8-4 JavaFX Scene Graph in SWT Application"

Example 8-1 Java Code for Plain SWT and JavaFX Buttons

import javafx.embed.swt.FXCanvas;
import javafx.event.ActionEvent;
import javafx.event.EventHandler;
import javafx.scene.Group;
import javafx.scene.Scene;
import javafx.scene.control.Button;
import javafx.scene.paint.Color;

import org.eclipse.swt.SWT;
import org.eclipse.swt.graphics.Point;
import org.eclipse.swt.layout.RowLayout;
import org.eclipse.swt.widgets.Display;
import org.eclipse.swt.widgets.Event;
import org.eclipse.swt.widgets.Listener;
import org.eclipse.swt.widgets.Shell;

public class TwoButtons {

public static void main(String[] args) {
final Display display = new Display();
final Shell shell = new Shell(display);
final RowLayout layout = new RowLayout();
shell.setLayout(layout);

/ Create the SWT button /
final org.eclipse.swt.widgets.Button swtButton =
new org.eclipse.swt.widgets.Button(shell, SWT.PUSH);
swtButton.setText("SWT Button");

/ Create an FXCanvas /
final FXCanvas fxCanvas = new FXCanvas(shell, SWT.NONE) {

@Override
public Point computeSize(int wHint, int hHint, boolean changed) {
getScene().getWindow().sizeToScene();
int width = (int) getScene().getWidth();
int height = (int) getScene().getHeight();
return new Point(width, height);
}
};
/ Create a JavaFX Group node /
Group group = new Group();
/ Create a JavaFX button /
final Button jfxButton = new Button("JFX Button");
/ Assign the CSS ID ipad-dark-grey /
jfxButton.setId("ipad-dark-grey");
/ Add the button as a child of the Group node /
group.getChildren().add(jfxButton);
/ Create the Scene instance and set the group node as root /
Scene scene = new Scene(group, Color.rgb(
shell.getBackground().getRed(),
shell.getBackground().getGreen(),
shell.getBackground().getBlue()));
/ Attach an external stylesheet /
scene.getStylesheets().add("twobuttons/Buttons.css");
fxCanvas.setScene(scene);

/ Add Listeners /
swtButton.addListener(SWT.Selection, new Listener() {

@Override
public void handleEvent(Event event) {
jfxButton.setText("JFX Button: Hello from SWT");
shell.layout();
}
});
jfxButton.setOnAction(new EventHandler<ActionEvent>() {

@Override
public void handle(ActionEvent event) {
swtButton.setText("SWT Button: Hello from JFX");
shell.layout();
}
});

shell.open();
while (!shell.isDisposed()) {
if (!display.readAndDispatch()) {
display.sleep();
}
}
display.dispose();
}
}

Clipping the Drawing Region

Any Shape object can be used as a clipping path that restricts the portion of the drawing area that will be rendered. The clipping path is part of the Graphics2D context; to set the clip attribute, you call Graphics2D.setClip and pass in the Shape that defines the clipping path you want to use. You can shrink the clipping path by calling the clip method and passing in another Shape; the clip is set to the intersection of the current clip and the specified Shape.

Example: ClipImage

This example animates a clipping path to reveal different portions of an image.


Note: If you don't see the applet running, you need to install at least the Java SE Development Kit (JDK) 7 release.
ClipImage.java contains the complete code for this applet. The applet requires the clouds.jpg image file.

The clipping path is defined by the intersection of an ellipse and a rectangle whose dimensions are set randomly. The ellipse is passed to the setClip method, and then clip is called to set the clipping path to the intersection of the ellipse and the rectangle.

private Ellipse2D ellipse = new Ellipse2D.Float();
private Rectangle2D rect = new Rectangle2D.Float();
...
ellipse.setFrame(x, y, ew, eh);
g2.setClip(ellipse);
rect.setRect(x+5, y+5, ew-10, eh-10);
g2.clip(rect);
Example: Starry

A clipping area can also be created from a text string. The following example creates a TextLayout with the string The Starry Night. Then, it gets the outline of the TextLayout. The TextLayout.getOutline method returns a Shape object and a Rectangle is created from the bounds of this Shape object. The bounds contain all the pixels the layout can draw. The color in the graphics context is set to blue and the outline shape is drawn, as illustrated by the following image and code snippet.

The Starry Night text (outline)
FontRenderContext frc = g2.getFontRenderContext();
Font f = new Font("Helvetica", 1, w/10);
String s = new String("The Starry Night");
TextLayout textTl = new TextLayout(s, f, frc);
AffineTransform transform = new AffineTransform();
Shape outline = textTl.getOutline(null);
Rectangle r = outline.getBounds();
transform = g2.getTransform();
transform.translate(w/2-(r.width/2), h/2+(r.height/2));
g2.transform(transform);
g2.setColor(Color.blue);
g2.draw(outline);
Next, a clipping area is set on the graphics context using the Shape object created from getOutline. The starry.gif image, which is Van Gogh's famous painting, The Starry Night, is drawn into this clipping area starting at the lower left corner of the Rectangle object.

g2.setClip(outline);
g2.drawImage(img, r.x, r.y, r.width, r.height, this);

Note: If you don't see the applet running, you need to install at least the Java SE Development Kit (JDK) 7 release.
Starry.java contains the complete code for this program. This applet requires the Starry.gif image file.

>>972961 (OP)
Шизофреник Максимка, залогинься.

Двачую, программирую на Pony, я на дваче самый успешный, это лучший язык т.к. имеет схожее название с моим любимым мультфильмом, надеюсь ОП выбрал его по этой-же причине.

>>972998
Надеюсь общаешься на toki-pona?

>>972962
Этот тред для успешных творческих людей, а не для обычных.
Обычный человек способен только заучить как лапшу на яве варить и генерировать её тоннами в надежде что его зарплата будет расти. Но расти она будет только до дочки психических расстройств/хронических болезней. А потом он обосрётся, так как жизнь прошла как на руднике - ебашишь изо дня в день, а плутоний всё не кончается.

>>973002
А когда творческие успехи стали определяться инструментами?

>>973005
Когда инструмент стимулирует творческие успехи, а не подавляет

>>973005
Ну так за некоторые «инструменты», например, расплата — хроническая бессонница, например.
Я вот, например, зелёный чай пью, например.

>>973006
>>973008
Ты же понимаешь, что это настолько субъективно насколько возможно?

>>972961 (OP)

>>973009
Продолжай дальше чистить говно вилкой, мне все равно

>>973017
>>972965
Мартыханы, плиз

Мимо оп

>>973019
А ты сам-то чем на хлеб зарабатываешь, успешный?

>>973021
Разумеется не ява-макакингом за буханку хлеба

>>973029

>>973030
Elixir и эрлангостек

>>973031
И это делает тебя илитой, вопросов нет.

И такой-то selfowned

>Просто унылое говно: C#, Java, PHP, Scala, Python, PHP, Ruby, Elixir, Perl, node.js ...

>Elixir

>>973034
Это список от поехавшего ублюдка - максимки, но в списке почти все годнота.

>>973044
В котором именно непонятно же

>>973118
Все кроме последнего, ясное дело. Ту парашу, если вкатываешь, стоит только учить на уровне джуна чтобы тебя взяли хоть куда и набрать год официального, подтверждаемого опыта и уволиться. Заодно научиться всей этой корпоративно-офисной поеботе, чтобы рандомный сыч с двачей не сильно выделялся своим чуханством. Все, с этого момента уже начинается нормальная работа и начало карьеры.

>>973136
А после идти на Coq писать?

>>973152
На coq только петухи идут писать, впрочем тебе можно

>>973199
Нет уж тогда, я лучше на js продолжу писат

>>973199
Нет уж тогда, я лучше на js продолжу писат

>>973204
писать fix

>>973203
>2017
>писать на js
Может ты еще и бекенд пишешь?

>>972961 (OP)
лол, мараз, как будто даун уровня maxim напейсал

>>972961 (OP)
>Binary Protocols and Protocol Stacks
>Storage Systems (CODASYL and MUMPS Replacement)
>Array Processing Languages (Fortran replacement)
>Concurrency Runtime and Languages (Ada Replacement)
>R&D Languages (AUTOMATH replacement)
>Target Languages (Pascal Replacement)
>New Markets (Inexistant satisfaction)

Понты, понты. Почему в таком же стиле не продолжил?
Dlya petuhov
Prosto unyloe govno

>>973211
>даун уровня maxim
Лол, ты не поверишь...

>>973209
Для себя на flask трогал

>>973216
Очень легко по кейвордам распознаётся:
>N2O
>ASN.1
>Erlang
>Rust
>Coq
На
>Z3 Lean
вообще сейчас тренд у тамошних фепешных жж-шизиков

>>973261
тьфу Короче на питоне немного писал.

Олсо, забавно что Erlang типа норм Concurrency все дела, а Elixir, который может всё то же самое + много чего ещё, и за поледний год пророс больше, чем ершланг за 10 лет, ну и блевать с него не так тянет - так это Просто унылое говно же, нужно выебнуться типа фу лахи хипсторы я не такой я хардкордный задрощер.
Махимка, какой же ты нелепый.
Олсо
>Pony - Erlang replacement
Как эта статическая параша уровня гоу его заменит-то? Проиграл с кукареков на оф сайте про супир-пупир сейфети, это с такой-то системой типов, лоооол. Лучше уже без типов вовсе, но с нормальными dataflow примитивами, чем вот это гавно с претензями на корректнес, у первого хотя бы in real world задачи есть.

>>972961 (OP)
Объясните, кто в теме, что не так с этим человеком? Почему он всех называется ебанатами? Есть ли практическая польза от его пруверов и того матана, которым он постоянно выебывается в своем ЖЖ. Насколько я понимаю по состоянию на сегодняшний день он безработный. Он хуй с горы или норм чувак, который дохуя всего знает и сильно умнее среднего программиста?

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

>>973888
чо за васян с пропуском в трусики?

>>973888
>Есть ли практическая польза от его пруверов и того матана, которым он постоянно выебывается в своем ЖЖ.
Этот "матан" - будущее всей математики, если что. Потому что классический подход умер в начале 20 века от кризиса оснований. И вот как-то так получилось, что пан ебаный хохол в этот "матан" будущего может, причем на уровне аж запиливания своих пруверов и языков с зависимыми типами, а в великой расеюшке во все это не может вообще никто. Последним был Воеводский, который съебал отсюда в ужасе и сейчас профессор в Принстоне и лауреат филдса. Так и живем, сладкий хлеб жуем. Ебанаты и есть, самые настоящие.

>>973938
>профессор в Принстоне и лауреат филдса.
ясно, ноунейм грантохуй

осторожно конструктивный петух протёк в пр

>>973938
Зависимые типы - это новый хайп, по типу фп, когда все начали лямбды пихать в старые языки? В чем профит от них?

>>973938
А что, в вашей математике для альтернативно одарённых утверждение теоремы Гудстейна действительно является ложным?
Кстати, как относишься к Пенроузу, сильно пукан от него болит?

>>973958
>Зависимые типы - это новый хайп
Этому хайпу уже 40 лет.
>В чем профит от них?
Благодаря изоморфизму Карри-Говарда, с точки зрения программирования - абсолютно корректные программы, работающие так как положено, а не как Аллах на душу положит, а с точки зрения математики - конструктивные, вычислимые основания и как итог - математика без кризисов и парадоксов, автоматизированное доказательство теорем, а в перспективе вообще полная автоматизация математики.
>>973959
>в вашей математике для альтернативно одарённых утверждение теоремы Гудстейна действительно является ложным?
Конструктивные утверждения = построения. Нет построения, соответствующего утверждению - нет и утверждения, а есть треп бабок с семками на лавочке, никакого отношения к математике не имеющий.
>как относишься к Пенроузу
Распиаренный хуй с горы.

>>973888
Ч У Х А Н
У
Х
А
Н

>>973973
>ерспективе вообще полная автоматизация математики.
Разве теорема Геделя не говорит что ты сосешь хуи?

>Replacement
зачем

>>973973
>Этому хайпу уже 40 лет.

Я имею в виду в среде программирования, идрис вообще себя позиционирует, как язык общего назначения, а не для науки.

>>973984
Нет, не говорит. В конструктивной математике выводимо и доказуемо все, что в ней может быть выражено. Поэтому, например, MLTT не только теория касающаяся конструктивных объектов, но и сама по себе конструктивный объект, правила вывода в которой так же конструктивные объекты, проверяемые на корректность средствами самой теории. Это возможно из-за конструктивной интерпретации логических констант (BHK), а не просто трактовки их как оторванных от построений знаков, смысл которых можно вообще не рассматривать (как у Бурбаков).
>>973987
Идрис делается с упором на программирование общего назначения, да. Но это не значит, что для этой цели не подходит тот же кок, просто там были бы нужны костыли, которые в идрисе уже запилены, н-р тип IO.

>>973973
>вообще полная автоматизация математики

Лол, тогда все творчество из математики пропадет, в чем кайф автоматически получать доказательства или я не правильно понял и это просто ускорит вывод нужных теорем или сразу скажет, что что-то невозможно?

>>973989
И то и другое. Если есть надежные непротиворечивые основания математики, то все возможные следствия из них (всю математику, считай, ну с учетом времени, требующегося на это) можно получить автоматически. С другой стороны, вот есть например мочидзукина теория IUTeich. Мочидзука утверждает, что в ней доказуема АВС-гипотеза. Проблема в том, что кроме него самого доказательства никто не понимает, потому что никто не въезжает в его аутизм. А взяв IUTeich за основу, можно было бы автоматически проверить, доказуема ли в ней АВС-гипотеза или там теорема Ферма, или таки Мочидзука пиздит / заблуждается.

>>973991
А в чем тут аутизм, все понятно же?

>>973994
Ну если тебе мочидзукины доказательства понятны, поздравляю. Выгода автоматизации в данном случае была бы в том, чтобы не тратить годы на штудирование мочидзуки, т.к. он слишком широко использует формализмы собственного изобретения, которые кроме его работ нигде не встречаются.

>>973996
т.е. он нинужен

>>973999
Почему не нужен? Он поехавший гений, понимающий математику настолько, чтобы самостоятельно пилить все нужное для своих доказательств. Проблема в том, что остальным требуется во все это въезжать. При автоматизации этого бы не потребовалось.

>>973973
лол, свидетель тезиса Чёрча-Тьюринга бля настолько огорчён тем, что противные математики умудряются решать невычислимые задачи, что ушёл в конструктивный манямир, где даже легко формализуемая простая теоремка, истинность утверждения которая понятна любому ребёнку - это серьёзный вопрос

возвращайся лучше в math/, маня, дальше народ смешить, там тебя заждались уже

>>973996
С чего начинать штудировать современный матан? Знаю только университетский курс прямиком из 19 века на уровне зубрежки формул. Однако желалание причастится к таинству этой науки никогда не пропадало.

>>974003
>противные математики умудряются решать невычислимые задачи,
Вера в решение != решение. О каком решении без соответствующего ему построения вообще можно говорить? Вот такие умники и привели математику к кризису оснований, из которого нет выхода кроме полного конструктивного переосмысления.

>>974005
понятно, у альтернативно одарённых Теорема Гудстейна неформализуема

суть в том что МТ - это весьма ограниченный кусок говна, разум на которой построить невозможно из-за отсутсвия мат. индукции, абдукции и интуиции.
хайп на твою пруверопарашу спадёт через десяток лет, а какой нибудь модус понес будет жить вечено

>>974007
>суть в том что МТ - это весьма ограниченный кусок говна, разум на которой построить невозможно из-за отсутсвия мат. индукции, абдукции и интуиции.
Ну раз так школьник на мейлру сказал, то ладно. Даже не буду спрашивать определение разума и интуиции, случай и так предельно ясный.

>>974004
Курант "Что такое математика"

>>974051
Хорошая книга, но она скорее для старшего школьного возраста.
Впрочем, если кто-то не знает того что там написано, то дальше двигаться смысла нет.

>>972961 (OP)
Там сайтик с объяснениями подъехал:
http://semantic.vision/

>>974965
Все теперь я перестану быть быдлом и буду писать бэк на Pony с BlazingDB и напишу транслятор из Coq в js, чтобы писать фронт по человечески с автоматический доказательством корректности аякс запросов и анимирования каруселей!

>>974986
автоматическим конечно же

Почитал блог этого максимки и что самое страшное, в комментах под его бредом мало несогласных, они серьезно там все поехавшие в жж?

>>974994
Но ведь он прав.

>>975002
В чем прав лол? В мире существует сотни и тысячи "интересных" технологий, у которых нет будущего, зачем призывать их учить лол? У каждого я думаю такой список наберется на который он дрочит, но который кроме него никому не нужен.

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

>>975009
Знаешь, после жж, у меня сильно поднялось мнение о кодаче.

О будущем в ближайшем будущем, очевидно, что будущее за теми технологиями, за которыми стоят google, microsoft, ibm, oracle...

Сколько бы не хейтили go, но вот за ним реально будущее.

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

>>975020

>>975032
>эти боевые картиночки
-> /b

>>974994
на тематическом гей-форуме тоже будет мало несогласных с концепцией ебли в жопу..

>>974004
определись, есть ли у тебя доступные ресурсы
например, мамка с борщем

>>975118
И то верно

>>975011
>мнение о кодаче.
Кодач пал, центурион.

Надо быть шизойдом дабы понять это?

>>975405
просто это путь жжшного илитклоуна
первая волна илитблядства: хаскiль, дрочка на мощные системы типов и кокотегориальность, утверждение о прикладной пользе всего этого в повседневном программировании
вторая волна илитблядства: дрочка на завтипы, пруверы, начало интуиционистского маразма
третья волна илиблядства, предтерминальная: отход в кококонструкивистский манямир с кукарекам про полную автоматизацию математики, постоянная фокусировка на основаниях
по всей видимости, четвёртая финальная стадия: полная деградация до ультрафинитизма и понимания математики на уровне древних греков

тут можно провести аналогию с фемками
первая волна - задачи чисто прикладные, движение по законодательно-правовому направлению
вторая волна - направление тоже вроде прикладное, хотя задачи весьма расплывчатые, уже появляются какие-то обощения и теор. обоснования, вроде теории пересечений
третья волна - полнейший пиздец с gender science и privilege theory, и прочими фундаментальными открытиями, которые должны изменить мир

в обоих случаях имеем типичный криптомарксизм: всё плохо, потому что всё с самого основания ниправильна, нужно всё изменить, мы знаем как это сделать, ко-ко-ко ривалюция нужно привозмогать и высрать нового человека, и новое общество, без классов, полового диморфизма и модус понес, аминь
ну и конечно же бесконечный самоподдув, заключающийся в ощущении себя неибаца прогрессивным

>>975405
Нет, достаточно иметь каплю критического мышления чтобы понять, что перед нами шизик.

>>975497
Не понимаю я твоей попаболи по поводу конструктивной математики. Из твоих постов на эту тему можно понять, что ты считаешь интуиционизм чем-то плохим.
>полная деградация до ультрафинитизма и понимания математики на уровне древних греков
Кризис оснований как раз и показал, что на самом деле от греков почти и не ушли никуда. Вроде чего-то там усиленно развивали, доказывали, а как до дела дошло, оказалось, что формально-аксиоматически невозможно доказать даже непротиворечивость арифметики, с геометрией еще худо-бедно вышло. У меня так программа Гильберта проебалась. Проблема-то оказалась всего лишь в вере во всякие невычислимые античные странности типа закона исключенного третьего и актуальной бесконечности, откуда и растут ноги у всяких парадоксов. Про культурмарксизм и феминизм вообще хуйню несешь какую-то, сжв тут вообще не при чем, параллелей никаких.

>>975535

>>975535
>Кризис оснований как раз и показал, что на самом деле от греков почти и не ушли никуда.
Конечно, никуда не ушли. Ракеты только в космос запускаем и ядерные реакторы строим.

>>975565
>Ракеты только в космос запускаем и ядерные реакторы строим.
Вся математика, нужная для этого, вычислима. Конструктивна, то есть.

>>975567
Пруф, пожалуйста.

>>975535
петушок, просто съеби обратно в math/

>>975497
Анон, я правильно понял, что конструктивисты в мире математики - это как хаскелисты в мире программирования? То есть обиженные петухи, которых успешные господа обходят стороной.

>>975497
Их обходят ибо бояться. У них есть шаманское Знание.

>>975603
* боятся

Впрочем, даже от мира функционального программирования появились хорошие вещи типа map и прочих функций принимающих функции.

>>975606
А тебя не смущает, что само программирование в нынешнем виде появилось как одно из практических применений конструктивной математики? Тьюринг, Пост, Черч, Колмогоров, Марков - слыхал про таких крнструктивистов, не?

>>975653
Я так понял, для того чтобы объект был конструктивным, достаточно иметь правило его построения?
Если да, то бесконечная снежинка Коха - это конструктивный объект, верно?

>>975689
>для того чтобы объект был конструктивным, достаточно иметь правило его построения? бесконечная снежинка Коха - это конструктивный объект, верно?
Это пример потенциальной бесконечности по Маркову. Разница с актуальной бесконечностью в том, что в данном случае бесконечность не оторвана от конкретного объекта, правила построения которого у нас есть.

>>975697
Но ведь у нас нет алгоритма определения является ли х потенциальной бесконечностью или актуальной, так ведь?

>>975707
Потенциальная бесконечность - это бесконечность, связанная с правилами построения объекта. Актуальная бесконечность - это бесконечность в общем виде "сама по себе", не связанная с конкретными правилами построения. В нее можно только веровать.

>>975708
Допустим у нас есть тьюринг-полный язык, у нас на нём есть программа, которая принимает на вход некое (синтаксически корректное) выражение, описывающее некий объект. Если объект конструктивный - возвращает true, если неконструктивный - false. Возможно ли построить такую программу?

>>975711
Деньги вперед.

>>975119
>мамка с борщами
Есть конечно, поэтому и спрашиваю. Куранта читал, куда двигаться дальше?

>>975775
>куда двигаться дальше?
-> /a

>>975782
Затралел, возьми с полки говна пирожок, дружок.

>>975790
Ня :3

>>975567
А как же всякие теории, основанные на бесконечностях, типа интергралов, диффуров?
Я тему не секу, но вроде как они не попадают под "абстракцию потенциальной осуществимоси", или че?

>>975822
все это ненужно

>>975822
Суть в том, что они оперируют бесконечностями как в ленивых языках или бесконечными стримами в неленивых. Т.е. ты можешь передовать бесконечность как объект, но делать вычисления с ней можешь только до конечной величины, иначе пиздец. Т.е., например, число pi - бесконечное, но для того чтобы посчитать площадь реального круга, тебе же не нужна бесконечность, ты используешь его до определённой степени точности вооот.

>>975864
Что можно почитать для вката в эту вашу секту конструктивисткую математику?
Почему аноны считают тебя ебанутым? Вроде бы вполне адекватная вещь

>>975873
Я не он. Можешь просто архив math/ почитать на эту тему для большего погружения в забавность срача и там же и спросить лит-ру.

>>975711
Сделаю за 5К на JS, HTML и CSS. Деньги вперёд.
[email protected]

>>975888
Надо будет поискать ибо начал читать первую попавшуюся книгу а там:
Образное мышление обрабатывает в основном
объективные данные, поступающие из внешнего мира конструктивными методами, т.е. через
представления. Левое полушарие оперирует преимущественно субъективными и качественными категориями; оно имеет дело с
речью, логикой и счетом в
уме(арифметические действия производятся помимо каких-либо пространственных моделей). Языковое мышление называют еще вербальным; в противоположность образному мышлению, его можно назвать дифференциальным или
микрооперационным.Биполярность психической деятельности имеет доминантный и рецессивный
полюса, в зависимости от того, какое из полушарий левое или правое является ведущим, а какое–ведомым. Слева находятся «мистические» центры, справа – «эмоциональные», отсюда
левополушарные люди менее эмоцион
альны, но более религиозны, и наоборот.

Продолжаю читать и жду пока торсионы с эфиром на эпициклах вылезут избавлять мой мозг левши от шлаков и болезнетворных миазмов.

>>976008
Лол.

Очевидно, что прикладной пользы со всей этой клоунады с теориями типов нет никакой. Даже Haskell с мандадками не взлетел и так и остался уделом определённого сорта извращенцев. Кукареки про ко-ко-корректность не оправдались, писать программу и в этом же месте доказывать её - долго, сложно и дорого, и писать интеграционные тесты всё равно нужно. Требования к прикладной программе, её разработке и поддержке мало пересекаются с формальными изъёбами. При этом, какую-нибудь более строгую систему, вроде базирующейся на субструктурной логике не могут осилить даже немногочисленные любители мандадок.
Касательно пруверов - это отдельный лулз. Они ненужны даже самим построителям теорем, посколько заставляют делать слишком много рутинной работы даже в Coq, да и знает о их существовании ничтожный процент математиков. Складывается впечатление, что ими пользуются только вчерашние хаскелисты, решившие поднять планку илитблядства, либо сами создатели этих пруверов.
Касательно конструктивной матеши - опять же, всё просто - всем похуй. Вот и остаётся кукарекать про "ривалюция! человеки не нужны! слава роботам! скоро, очень скоро!" То есть остаётся быть кем-то на уровне машин лёрнинг дебича. Но если второе имеет хотя бы прикладное применение на некоторых задачах и может принести гешефт, то быть ТТ-дебичем - чуханство забесплатно.

>>976008
По данному вопросу лучше смотри Борис Сергеев,
«Ум хорошо, а два лучше».

>>976056
А как же теорема 4 красок?

>>976079
А что с ней?

Нужен прогер, для разработки и дальнейшей работы над мобильным приложением.
Опыт работы обязателен.
Мои контакты [email protected]
Зарплата от 500зеленых в месяц. В перспективе рост зп
В письме рассказать немного о себе, о своих проектах и т.п., возраст.

>>976124
Ты бы хоть в википедию заглянул.
Задача 4 красок - сложная задача, долгое время остававшаяся нерешённой. Доказательство было получено с помощью компьютера, используя Coq.
Таким образом, тезис о том, что пруф ассистенты не нужны самим математикам, опровергнут.

>>976056
Весь твой высер можно заменить одной фразой - "быдлопроблемы неосиляторов". Сложна вам все, как той Карине. Ты хотя бы пойми тот факт, что неосиляторство рандомного васяна из северной нигерии со снегом - это не проблемы конструктивной математики. То, что прувер по назначению может использовать только его автор и 3,5 калеки понимающих что это такое вообще и зачем, никак не свидетельствует в пользу бесполезности пруверов.

>>976210
Мать твою ебал.

>>973209
А чем принципиально плох js на бэке?

>>976210
Как раз свидетельствует, и дело не в том, что их не понимают, А НЕ ПОНИМАЮТ зачем они нужны и соответственно низкий интерес даже у самих математиков, тем более нахер это не нужно программистам.

>>976233
У машоба, нейронок нашлось применение, поэтому ими заинтересовался бизнес, программисты стали смотреть в эту сторону, потому что есть профит, есть новые возможности, какие возможности дают пруверы, чтобы людям захотелось их изучать и внедрять в стартапы/бизнесс и тд.

>>972961 (OP)
Заказываю ОПу два чая за создание монумента эталонного снобизма /pr. Ещё бы всё это облечь в одну фразу и можно на все профильные ресурсы с этим идти.

>>976233
>НЕ ПОНИМАЮТ зачем они нужны и соответственно низкий интерес даже у самих математиков, тем более нахер это не нужно программистам.
Странный аргумент. 95% программистов - макаки, говнокодящие для дяди за хлебушек. То, что они ни во что не могут, кроме прочитанного про свои параши, это вообще норма. Насчет ненужности математикам, тут смотря что за математика. Гомотопическую теорию типов изначально в пруверах писали, там без этого вообще никуда.

>>972961 (OP)
Почитал про технологии из твоего списка, все действительно очень годно. Особенно заинтересовали бдшки. Aerospike как замена редиске, и blazing как замена нормальной бд. Есть только одно но, аэроспайк только под шлинукс и нихуя не попенсурс, а блазинг так вообще полностью проприетарный стоит 5к бачей. Есть что-нибудь аналогичное но попенсорс?
Алсо
>— Big Operaing Systems: Linux, Windows, Mac
Ну и что тогда использовать?

>>976243
>Ну и что тогда использовать?

dos

>>976247
Но на нем ни одна из выше перечисленных технологий не встанет.

>>976243
>Ну и что тогда использовать?
Спроси у Максимки.

>>976243
Nix, Barrelfish, Arrakis

>>976272
Так под них же софта нет. Все эти крутые штуки не работают на этих зачаточных ос. Я так понял даже на фряху портов у половины нет.

>>976272
>Nix
http://www.nix.ru/

Зарепортил маркетолога

>>972961 (OP)
Есть дин чувак, вроде американец, постоянно тусит с кучей голых баб на своих яхтах. Или на стрельбищах тусуется стреляя из всего чего можно.

Вот это успех!
Уверен он к нему пришёл без использования всей этой хуеты.

>>976288
Ебануты чтоле?
https://nixos.org/

>>976272
Последние два это экзоядра все?

>>976210
Типичный подход криптомарксиста. Talk is cheap.

Сложность и её нарастание - это вообще-то существенный аргумент учитываемый в любом бизнесе. Например, программный код, написанный сложно и требующий дохуя интелектуальных затрат и звёздных специалистов - нужен только в случае отсутсвия альтернатив. Ненужность хаскиля для бизнеса легко из этого выводится.
>То, что прувер по назначению может использоват
Его не не могут использовать, его использование в 99% случаев просто нахуй не нужно и не интересно, потому как подавляющее большинство математиков не интересуется конструктивизмом, а просто юзают математику на классической логике и не ебут мозг себе и остальным. Основания математики вообще не относятся к математике, а лежат где-то в промежутке между философией и метафизикой.

>>976241
>95% программистов - макаки
Плохой криптомарксист, негодный. Вместо того чтобы пытаться популяризовать свою парашу, устраивает из неё илитблядский культ и маргинизуруется в гетто для альтернативно одарённых.
Хотя популяризация позже была, да провалилась, ведь программисты скорее выберут язык за его UX, чем за превозмогания и кукареки про ко-ко-коректность.

А есть пример какой-то где можно применить эти все зависимые типы и прочая на чем-то прикладном типа веб-сервера? Или хотя бы это докажет корректность операционной системы? Оно только для корректности, роста производительности и не должно быть?

>>976243
Максимушка наверняка имел в виду это:
http://erlangonxen.org/

>>976308
>существенный аргумент учитываемый в любом бизнесе.
>Ненужность хаскиля для бизнеса
Бизнис, разумеется, высшая цель человечества. Но так-то да, Гиви арбузами торгует без всяких хаскелей и даже таблицы умножения не знает.
>Основания математики вообще не относятся к математике,
К неконструктивной не относятся. Отсюда и парадоксы и кризис оснований. До Брауэра никому и в голову не приходило, что основания - это то, с чего вообще начинается математика, и без понимания сути (любой) науки невозможно эту науку развивать, пик >>975535 релейтед.
>Плохой криптомарксист, негодный.
Все проще - не криптомарксист.
>Вместо того чтобы пытаться популяризовать свою парашу,
А зачем? Это не секта, для которой важно нагнать побольше баранов. Кто не осилил, тому и не место в теме, порог вхождения - это хорошо же, отсеиваются всякие школьники, васяны и тети сраки.

>>976331
Ну так и говори, что чисто теоретический узконаправленный материал и ничего общего с реальным применением не имеет, а программирование - это в первую очередь решение конкретных задач, а не теоретические излияния.

>>976338
update, вот когда придумаете приложения к каким-то задачам, тогда и приходите в /pr, а пока изволите пиздовать в /math

>>972961 (OP)
>New Markets (Inexistant satisfaction) — озеро, где живут Черные Лебеди:
>Lisp Machine replacement
>Для петухов:
>All LISPs: Clojure, Common Lisp, Smalltalk, ...

Это как?

>>976300
Пгошу ответить.

>>976398
Лис-машина — просто название для процессоров, интерпретирующих динамикопарашу напрямую. Откуда там эрланг сам подумой.

>>976501
Зайди да посмотри, идиот.

>>976278
>Так под них же софта нет.
Да и хуй на него.
Плюсы есть - все что надо сам напишу.

>>976558
Плюсы для была же, только С и Ассемблер.

>>976643
быдла*

>>976643
>только С и Ассемблер.
Эхм.
Ну так ты прав, да - структур с генериками вполне достаточно.

>>975497
Поясни за Мартин-Лёфа, куда его присунуть?

>>976547
Лисп-машины ничего не интерпретировали напрямую, так что это странное название.

>>972961 (OP)
Максим, ты опять выходишь на связь? Как там твои стартапы стоимостью десятки миллионов долларов? Уже продал?

Почему у меня ощущение что оп аутист.

Зато Махiмка даёт лекции
з категорної семантицi індуктивних типів
а вы тут все школники и хэйторы с сосача.
Так то.
https://www.youtube.com/watch?v=UjjuCRlS-bA

>>977032
Будто не так.

>>972961 (OP)
>Erlang
>Rust
>OCaml
>Lisp

максимальный долбоеб

>>977058
Макаку забыли спросить

>>977066
ВСЕ ПИТОНИСТЫ ГОРДЫЙ НАРОД
ЭРЛАНГОВЦЕВ ВСЯКИХ ЕБАЛИ МЫ РОТ

НА ГАЛЕРЕ РАНЬШЕ ЕБАЛИ БАРАН
ЛИСПОВЦЕВ МАМКИ ТЕПЕРЬ ДАЮТ НАМ

>>973044
>PHP, Ruby, Elixir, Perl
>годнота
Лловите говноеда!

>>977371
Самехом по губам - шмяк!

>>977375
Паааш, там надо на вордпресс тему натянуть срочно! Дуй на работу, плевать что выходной!

>>977032
Начал смотреть эту лекцию, все понятно даже без знания цыганского и чет проиграл с объяснений что есть тип П(А,В) и вопросов из зала уровня "якщо це таке В(х)". Сразу нарисовал бы что-то а-ля пик2 и все.

>>977400
моар/соус тян на первом пике?

>>977425
>тян
Максимка ежжи :3

Признавайтесь, бугуртсмены, кому с максимкиной лекции подгорело?

>>977454
У меня.

>>976059
Аноны, поясните это не троллинг? Я потом не стану креационистом?

>>977551
Нет, не троллинг, это книга о работе моска, написанная врачом, реабилитировавшим солдат после войны. Одного заново научили считать, потом он работал бухгалтером.
Асимметрия полушарий больше нигде не объяснена, даже у Докинза.

>>977560
Тогда пошел наворачивать.

А теперь как будет всё на самом деле.

Начнём с фундаментально-принципиального.
Категориально-петушанский хайп-пузырь уже почти полностью сдулся (а вместе с ним хаскель и прочее говно, якобы базирующееся на теоркате) и околомаетатические хипстерские выблядки мигрируют на новый, ещё более улюдошный хайп-пузырь - HoTT. То что с ним через 5-10 лет произойдёт то же самое, что и с предшественником вполне очевидно - это одна и та же петушиная культура для мамкиных модников. В этом смысле хотт-петушок ближе к жс-хипстерам, меняющих фреймворк каждые два месяца, чем к логике или математике. CS - это вообще отрасль состоящая целиком из анальной клоунады и натужного пердежа в лужу 24/7; за последние 40 лет все вещи, которые применялись в промышленном программировании созданы инженерами-прикладниками, а не компуктер сцайнс мочёными.

Далее, переходим уже конкретно к IT. Хайп-пузыри Big Data и Data Science продолжают активно сдуваться. Выяснилось, что это псевдо-отрасли, к которым применяются обычные, общие для программирования методы, и выделение их как отдельных было выгодно только для маркетолухов, разжигающих хайп в 2016 и 2015 годах соответсвенно. Так же было выяснено, что проблемы из этих псевдо-отраслей надуманные и для 99,9% бизнеса вообще чуждые.
Илитарным хайп-петухам сегодня приходиться держаться мёртвой хваткой за машмоб, для которых это святая святых. Вообще можно провести паралель хотт - машмоб - жс-хипстерство со смузи в старбаксах. Это всё один вид петухов, занимающихся не разработкой, а свечением своими ебальниками на конференциях и участия в наебательских стартапах.
Серьёзных предпосылок к сдуванию машмоб-пузыря ближайшие 10 лет пока нет. Дело в том, что IT-рынок - это несовршенный корпоративистский пиздец, который driven by группой жырных пузырчатых говноконтор, чей пердёж настолько громкий, что тотально засырает всё инфопространство и как шторм сносит более мелкие конторы в нужном первым направлении. Но всё же сдувание произойдёт, потому как кризис этого говна - вообще переодическое явление, вызываемое тем, что возложенные на него ожидания не оправдываются, потом его откладывают в долгий ящик на лет 20, потом кто-то придумывает новый фундаментальный костыль и начинается очередная волна хайпа.

Касательно языков. Мейнстримовые говна дают всем пасасать и уверенно показывают, что никуда уходить они не собираются и терять своих рабов тем более. Они стали модернизироваться куда чаще, добавляя множество фитч, которые в своё время "прозевали", существенно сокращая разрыв с немейнстримом высокими темпами. Достаточно грамотно в этом плане поступают мелкомягкие, постоянно вводя паралельно несколько веток экспериментальных языков и сливая более менее полезные вещи из них в сисярп. Главное тут, чтобы полезность "вещей" оценивалась самими разработчиками, а не коммитетскими пидорами, а то язык вскоре обрастёт тонной ненужных говен.
Однако, гугель продемонстрировал всем в очередной раз, что со времён девяностых ничего особо не изменилось, и можно пропихнуть любое жалкое поделие с нуля достаточно глубоко, просто пердя в уши индустрии из всех щелей.
Насчёт статика vs динамика. Очевидно, что преобладает и будет преобладать первая, так как мейнстрим весь статический. Правда в вебе статика традиционно просасывает, хоть и пытается просочится туда. Как бы там ни было, маняфантазии уебанов из первого параграфа, про покрытие мощными системами типов и ко-ко-коректностью всего и вся, ничего общего с реальностью не имеют, потому как статика уровня джявы большинство народа вполне устраивает. Смачный отсос хаскеля по всем фронтам только это доказывает. Думать, что если не взлетела полимфорная типизация 2го порядка, то взлетят завтипы - это полный ебанатизм. Это как думать, что если не взлетел пролог, то взлетит что-то на логике высших порядков которая, кстати говоря, выразительнее, чем ебёнаные завтипы лооол.
Касательно динамики - участь её печальна. Но не совсем. Дело в том, что существует неформальное движение статикоскептиков, численость которых возрастает тем больше, чем больше статикобляди форсят свой статикодебилизм. В отличие от динамических петушков, которые стали ими вынужденно, из-за бедности нажравшись всякого там пехепе-говнеца, первые - вполне опытные программисты, писавшие в том числе и на статике, и сделавшие свой выбор вполне осознанно. Убежище для таких всегда было и будет в виде лиспов, ершлангов, эликсиров, фортов и прочего тому подобного.

>>977680
Ок, а какие тогда действительно годные тренды есть из современных, которые не хайп и не пузырь? Что по поводу blockchain?

>>977680
аж до слез, малаца.

>>977727
Удваиваю.

>>977727
Что ты подмахиваешь, чухан? Этот высер, абсолютно неаргументируемая и бессмысленная графомания, в которой нарушается даже Modus Ponens. Единственное зерно мысли - это
> Это как думать, что если не взлетел пролог, то взлетит что-то на логике высших порядков
в остальном - пузырение лужи от самозванного "эксперта".

>>977755
модулус хуенис. расскажи нам о прорывных технологиях созданных матанопетухами? охуенной предсказательной спрсобностью бигдаты, ну или профита от нейронных сетей? фсе это хайп созданный матанопетухами для попила грантов и развода лохов.

>>977713
>blockchain
Еще больший хайп

>>977760
>профита от нейронных сетей
FaceApp, Prisma и еще та хрень, которая картинки делает психоделичными

>>977766
ну и компьютерное зрение, анализ текста

>>977766
Профит достойный мелкобуквенного, хуле.

>>977760
Поддвачну шарящего
>>977767
Куча алгоритмов обработки и конкретно компьютерного зрения, которые сейчас испольюзуются эвриве, придуманы без какой-либо кукаретико-математической базы.

>>977772
>без какой-либо кукаретико-математической базы
Там же линал сплошной.

>>977773
>линал
С точки зрения мамкиных теоркатпетушков это вовсе не математика.

>>977783
Ну если в этом смысле, то да, ничего "особенного" там не нужно.

>>977773
Линал там вспомогательный инструмент и есть далеко не везде. Это как говорить что какой-нибудь рендеринг opengl или directx придуманы мотематиками потому что там ангем.

>>977773
>Там же линал сплошной
если какая нибудь неработосбособная громоздкая хуйня, то да. а все работоспособное выглядит примерно так
http://www.imageprocessingplace.com/downloads_V3/root_downloads/tutorials/contour_tracing_Abeer_George_Ghuneim/index.html

>>977788
>если какая нибудь неработосбособная громоздкая хуйня

Я вообще http://opencv.org/ имел в виду, как стандарт на рынке.

>>977792
лол, неа. опенсв это набор алгоритмов, которые по большей части неработоспосбны.

>>977755
А с чем конкретно ты не согласен?

>>977797
>по большей части неработоспосбны
И ты тут такой такой хоть какие-то пруфы предоставляешь.

>>977801
За щекой проверь.

>>977797
Чем они неработоспособны? Тем что ты хотел йоба решение конкретно заточенное под твои нужды, а там набор дженерик функций?

>>977804
Уроки уже сделал?

>>977801
>какие-то пруфы
тебе защеку. поработай с ней поймешь. делал поиск окон на рабочем столе с захватом текстовых блоков, жидко обосрался. также нужно было найти элементы из набора на картинке, обосрался еще больше.

>>977806
хотябы перекрывающиеся элементарные фигуры вычленить.

>>977808
Н - неосилятор
Вангую что ты просто пытался сделать что-то типа import slesarflow as sf, как тут рядом товарищи из машоба делают. А вот хуй, с компьютр вижн такое не прокатывает.

>>977806
>>977807
>>977808
>>977809
>>977811
ебал твою мамашу

>>977808
>пруфы
>cубъективный опыт, причина которого скорее всего кроется в банальной некомпетентности

https://habrahabr.ru/post/208092/

https://habrahabr.ru/post/301096/

Ну вот парочка успещных примеров

>>977811
ой, иди нахуй осилятор. я с опенцв зарекся иметь дело и всегда говорю, что она говно и не надо тут мяняпроецировать.

>>977815

>Очкую подойти в тян
>ТНН!!!!!

>Не смог использовать инструмент
>ИНСТРУМЕНТ ГОВНО!!!!

>>977814
вот тебе хаартрейнинг, который длился целую неделю
http://note.sonots.com/SciSoftware/haartraining.html
с посредственным результатом, а то что швабропидоры красиво расписали это ничего не значит, детектить сову можно более простыми и эффективными методами.

>>977814
и да, можешь пободить по форуму опенцв и посмотреть как там все успешно и красиво.

>>977815
И зря, просто надо было сначала читануть\посмотреть пару курсов по computer vision в целом. Тогда бы не возникало 99% НЕ РАБОТАЕТ проблем, какие обычно вылазят если просто открываешь документацию и начинаешь хуячить код.

>>977822
все с тобой ясно, тащи сюда серьезный работоспособный проект тогда может тебя и не абасу.

>>977824
Хех, спасибо посмеялся

>>977830
абасал

>>977872
Смотри чтоб с монитора на клаву не затекло, сам знаешь что с ней бывает от влаги.

>>977764
Работаю blockchain-специалистом, брат жив, зависимость есть, батя грит малаца.

>>978075
>Работаю blockchain-специалистом
Кекус-пекус, уже даже должности такие придумали. Ну расскажи чем занимаешься? Без трололо, риали интересно

>>978075
>Работаю blockchain-специалистом

Майнишь? )

Если серьезно, посоветуешь, какие языки/технологии в этой сфере нужны?

>>977560
Интересная книга, два члена чаю за совет.
Я оказался унтермешем-амбидекстром блять

>>978205
И вот что сцукко характерно: социобляди в основном 100% правши. Даже в школе ебальных танцев они стоят справа в зале, чтобы лучше видеть зеркало и тренера. О том, что праворукость неразрывно связана с речевой деятельностью (это следствие того, что моск покривился, чтобы у волосатых четверолапых появилась речь), писали Ричард Докинз и Виктор Дольник. Ясно, что у одних будут развиты soft skillz, у других mad skillz, ну а третьи будут безуспешно пытаться вкатиться в айти.

>>978116
>Ну расскажи чем занимаешься?
Смарт-контракты для b2b-инвестирования и прочей торговли на фондовых рынках, интеграция блокчейнов, блокчейны на блокчейнах)
>>978150
>Майнишь?
Само собой)
>какие языки/технологии в этой сфере нужны?
Общего подхода нет, скорее можно выделить какие не нужны: ассемблеры, Си, языки с динамической типизацией. Я работаю с C#. Ещё популярны C++ и Java. Вообще тут больше в предметной области нужно шарить, в моём случае - финтех.

>>978245
Понятно, спасибо за инфу сначала прочитал, что нужны ассемблер и си лол

>>978255
И еще подскажи, что почитать по финтеху для нюфагов.

>>978245
>финтех
это бля че? финансовые технологии? понапридумывали хуйни всякой

>>978272
Курс экономики неплохо бы) В особенности макроэкономики, потом про функционирование конкретной сферы(например банкинг).
>>978275
Есть такое, просто сфера немного специфичная, поэтому выделяют.

>>978309
Спасибо

>>978309
Handbook Of Financial Cryptography And Security Burton Rosenberg годная книжка, стоит навернуть?

Мимо

>>978332
>Handbook Of Financial Cryptography And Security Burton Rosenberg
Не читал, поэтому не могу ничего сказать.

>>977680
Не совсем так. Функциональщики - это в первую очередь фанатики, социоблядками-хипстерами они являются не так часто, большинство вообще не ходит на конференции. Какой-то профит в плане типобезопасности у них действительно есть и с десятилетиями нарастает, просто в практическом отношении он гораздо менее значимый, чем им кажется, а главное, увеличеная сложность программ зачастую с перевесом нивелирует эти профиты, когда дело доходит до реальной майнтабельности. Динамические петушки вроде лисперов - это такие же фанатики, только с другими ценностями, с реальностью их ценности пересекаются не лучше.

>>980440
Сам то чьих?

>>978245
>Смарт-контракты для b2b-инвестирования
Виталик в трэде, все в tao

>>980628
жрет жабо или гопарашу ступудово

>>980628
Попробовал в automation qa, получше чем кодинг, но всё равно слишком много работать надо, сейчас хочу дворником, грузчиком или официантом, барменом.
Чтобы работать надо было пару дней в неделю, либо 4-5 дней, но по пару часов, и чтобы ничего изучать не надо было, и можно было думать о своём.

>>972961 (OP)
>ТЕХНОЛОГИИ УСПЕШНЫХ ПРОГРАММИСТОВ
Это успех! Смотрите, каких высот достиг Никитка!
https://lenta.ru/news/2017/04/21/sadkov/

Хули хаскелисты обязательно фрики и ебанутые на всю голову? Я как вижу явно нездорового анона и спрашиваю, кто он по масти, так оказывается из ваших.

>>981538
Наверное haskell раздувает чсв до небывалых масштабов из-за его нишевости и чердак начинает ехать, я вот учу его для себя просто интересно фп попробовать, пока нормально вроде.

>>981538
Хз, у него на гитхабе нет хаскеля вообще, с чего ты взял, что он хаскелист?

>>981538
золотце был местный лисп-задрот и никакого отношения к хаселл-господам не имел, кроме того что работал у них дворником

>>973034
Где self-owned то? Есть Erlang, есть ненужная надстройка Elixir для ниосиляторов которым неуютно без привычного говнеца

>>976224
Тем, что есть лучшие языки. Зачем жрать баланду, когда есть нормальная еда?

>>978332
>Handbook Of Financial Cryptography And Security Burton Rosenberg
>Financial
>(((Rosenberg)))
Норм должно быть.

>>981581
Есть Assembler, есть ненужная надстройка Erlang для ниосиляторов которым неуютно без привычного говнеца

>>981562
Ты на 0-самзнаешь не сидел, что ли?

>>981584
Не уловил твоей шутеечки, он что еврей или нацист?

>>981585
Зачем ассемблер, если можно микросхему конктерно под свою задачу собрать, без какого-либо оверхеда по энергии и тепловыделению?

Там это, Максимушка у себя в жжешечке этот тредик пиарит.

Короче, дабы это понять надо быть рыжим евреем-аутистом с бородой?

>>981811
Не обязательно рыжим.

>>981800
Что за Максимка и где его жж?

>>982276
Господи, ну наконец-то.
http://maxim.livejournal.com/

Максимка чёта загрустил.

>>973938
>Потому что классический подход умер в начале 20 века от кризиса оснований.

Ебанат, зачем ты пиздишь о том, в чем нихуя не понимаешь? Ни конструктивизм, hoott и прочая хрень не разрешают этот кризис чем формальная программка Гильберта которой сто лет в обед.

>>977032

Обзмеился с ЦЕ КОК

>>982878
Поясни почему вся эта хрень не разрешает кризис.

Мимо

>>983267

Потому что все они пытаются разрешить противоречия "юридически", запретом на проведение рассуждений или конструкции всяких "множеств всем множеств". У конструктивистов вроде даже логика ограничена, без закона исключенного третьего. Формальные системы Гильберта точно так же работают, в этом плане ничего нового.

це кок

>>973938
>Этот "матан" - будущее всей математики, если что. Потому что классический подход умер в начале 20 века от кризиса оснований.

>>983321
Вроде, блядь, мавроди. Ум у тебя огранисен, а не логика у конструктивистов. Хоть бы педивикию почитал прежде чем сюда лезть со своим школьным мнением.

>>983498

Конструктивист хуже пидораса. Иди нахуй, хуйло!

>>983498

Двай, конструктивный петушок, попрыгай покукарекивая

ЦЕ КОК ЦЕ КОК ЦЕ КОК ЦЕ КОК ЦЕ КОК ЦЕ КОК ЦЕ КОК ЦЕ КОК ЦЕ КОК ЦЕ КОК ЦЕ КОК ЦЕ КОК ЦЕ КОК ЦЕ КОК ЦЕ КОК ЦЕ КОК ЦЕ КОК ЦЕ КОК ЦЕ КОК ЦЕ КОК ЦЕ КОК ЦЕ КОК ЦЕ КОК ЦЕ КОК ЦЕ КОК ЦЕ КОК ЦЕ КОК ЦЕ КОК ЦЕ КОК ЦЕ КОК ЦЕ КОК ЦЕ КОК ЦЕ КОК ЦЕ КОК ЦЕ КОК ЦЕ КОК ЦЕ КОК ЦЕ КОК ЦЕ КОК ЦЕ КОК ЦЕ КОК ЦЕ КОК ЦЕ КОК ЦЕ КОК ЦЕ КОК ЦЕ КОК ЦЕ КОК ЦЕ КОК ЦЕ КОК ЦЕ КОК ЦЕ КОК

КТО НЕ СКАЧЕТ ТОТ ЦЕ КОК

>>982878
Вы бы хоть между собой определились, дурики. А то в соседнем разделе какое'то чучело кукарекает, что ви все врети, нет никаког кризиса оснований. Здесь другое чучело визжит, что конструктивный подход кризиса оснований не разрешает, т.е кризис все'таки есть. Я надеюсь, вы с тем довном хоття бы разные петушки, а то такой плюрализм мнений в одной голове, это не норма. Так вот, программа Брауэра, изложенная им в его диссере в 1907 году, кризис оснований разрешает полностью. Оказалось, для этого достаточно дропнуть неаычислимую фофудью, закон исключенного третьего, актуальную бесконечность, и еще кое'что по мелочи. И все, в математике нужна только вычислимость, вере место в церкви.

>>983613
что б ты ЗНАЛ мы с бесконечность НА ОДНОМ ГЕКТАРЕ СРАЛИ а ты хочеш её изключить

>>983613

Это как лечить импотенцию отрубание хуя.

>>983613
>И все, в математике нужна только вычислимость

Ты только математикам этого не говори, рискуешь получить хуй в рот.

>>983613

Брауэр мудак, он даже определение натурального числа не мог дать.

>>983652
Папа твой мудак, потому что не предохранялся. Так ему и передай. А натуральные числа у Брауэра определены точно, задолго до фон Неймана и Черча.

Брауэр не мудак. Это Мартин-Леф мудак, а Брауэр просто затравленный петух-газонюх. Вот Гильберт, Кантор и Гёдель - тру математики, и все они ссали в рот интуиционистам.

>>983665

Ты малограмотное, пиздливое хуйло. У брауэра, как и у всех интуиционистов, натуральное число это исходное, неопределяемое понятие.

>>983690
N-петух, ты ведь даже не читал Брауэра. Натуральное число определяется у него как построение на основе two-ity, как и все остальное.

пассал в натуральный ротешник матанопитухам и брауэругильбертхуялеру тоже

>>983674
Гильберт просрал свою программу по формализации арифметики. Кантор просрал основания, придумав протеворечивую теорию множеств, в которой выразимы всякие парадоксы, н'р Рассела. Гедель теоремой о неполноте окончательно похоронил формально'аусиоматический подход в математике. Я ничего не забыл? Ах, да, Мартин'Леф создал вычислимые конструктивные основания, а Брауэр основоположник подхода, сделавший это возможным.

>>983725
анон, поясни, кокое отношение эта наркрмания имеет к погромированию, не говоря о прикладных задачах реального мира? кокое?

>>983727
Прямое. Интерпретация логических констант по Колмогорову делает теорию типов Мартин'Лефа не только основаниями математики, но и основой всех в т.ч возможных, языков программирования.

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

>>983741
НО ЭТО НАСТОЛЬКО СМРАДНЫЙ ПУК ЧТО ЗАСЛУЖИВАЕТ ТЩАТЕЛЬНЕЙШЕГО, ТАК-ТО!

>>983613
Гофера дауна не спрашивали.

>>983741
Ты слишком тупой для этого. И это даже не оскорбление, просто констатация факта. Все равно не поймешь ни хуя, так стоит ли мне распинаться, как думаешь? Только честно.

>>983843
>как думаешь?
думаю стоит, но ты не сможешь

>>983862
Думаю сможет, но согласен, не стоит.

>>983873
>думаю сможет
никто до него не смог и он не сможет

>>983876
Ну так'то да, я тоже думаю жто бесполезно. Какой смысл пытаться объяснить связь млтт с языками программирования тому, кто даже про типизированное лямбда'исчисление не слыхал. А если слыхал, то не понял, а если понял, то не так. Про куб Барендрегта, наверное и упоминать не стоит, это для мейлру совсем сложна.

>>983907
>типизированное лямбда'исчисление
>куб Барендрегта
ты нормально скажи, зачем эта наркоманская хуета нужна? вот есть прикладная задача, ее нужно решить, без типизированной пиздлы барендрегта ее никак не решить, просто ну совсем никак.

>>983907
>лямбда'исчисление
Хаскелоблядь детектед

Вся история развития языков и прикладного программирования опускает любые маняфантазии петушков что мол матан охуительно важен в индустрии.
Взять самые основы: машина Тьюринга и лямбда исчисление. Две эквивалентные формальные системы, одна легкая на восприятие, образная и в целом элементарная как для понимания, так и для вополщения т.к. отражает в себе свойства НАШЕГО мира и наших возможностей исходя их представлений на момент ее "изобретения".
Вторая - попытка зайти со стороны матана и аналитики, полностью отвязанной от реального мира.
Ну и что мы видим, практически вся отрасль развивается на благодатной почве машины Тьюрина, в то время как церебральные онанисты уже больше полувека витают в своих абстракциях бесконечного порядка. Другие искуственно загоняют себя в жесткие рамки из которых потом же десятилетиями вылазят истошно превозмогая и придумывая новые ограничения и математические системы. В это время "обычное" программирование идет по прямому пути, решая проблемы по мере поступления. Но в целом как и матанопетухи, так и мартыханы нужны, в конце-концов мейнстрим таки взял некоторые вещи у формалистов-аналистов, алмазы попадаются и тут и там, другое дело что мамкины теоретики пытаются их искать в другом месте, если не в другой вселенной.
И поэтому когда в очередной раз будете доказывать охуительную важность своих кластеров метапарадигм и лямбдакубов, не забывайте что по вкладу в отрасль сидите не на параше, однако совсем недалеко от нее.

>>983928
>машины Тьюрина
петухмаштина с бесконечной лентой. единственная заслуга тьюринка, в том, что он был петух и выпилился. а за няшу с опенцв плюсую.

>>983937
>няша с опенцв
Новый способ детектировать школоту - узнать как они называют Лену.

>>983937
>а за няшу с опенцв плюсую.
За твой пост плюсую, дико проиграл

>>983911
А я нормально и говорю. Просто тема не для дурачков.

>>983940
>Лену
я с ней только в опенцв игрался

>>983928
Лол, ты лямбда калькулюс штоле ниасилил? Мдауш, аппликация, абстракция и бета'редукция это ебать как сложно. С кем сижу на одном мейлру, пиздец просто.

>>983946
Что там неосиливать мань, и где в моем посте написано что это сложно?

>>983946
Кстати вот еще что всегда забавляет. При любом упоминании лямбда исчисления не важно в каком, но не в положительном контексте обязательно появляется перец вроде тебя и говорит вот эту вот хуйню "ТЫ НИОСИЛИЛ? ЭТО ЖИ ТАК ПРОСТО" и похуй что об осиливании\неосиливании речи вообще не шло, триггерятся ВСЕГДА и с одинаковыми "аргументами". Что наводит на мысль о неком матанофюррерке от которого это все пошло и за которым теперь тупо повторяют.

>>983947
Ну а чего тогда ноешь, все элементарно же. Любой ЯП представим в лямбде, смотрим куб Барендрегта, там грани'стрелки это отношение включения. Нижний левый угол простая типизированная лямбда, правый верхний лямбда С, исчисление построений или говоря поняьнее для местной школуйни, це кок.

>>983948
Речь как раз о неосиливании, иначе не было бы и вопросов о связи конструктивной математики с программированием. Сами сначала навалите себе в штаны, а потом кукарекуете что это ржавчина. Пиздец, зоопарк.

>>983999
И как это мне поможет с созданием персональных домашних страниц?

>>984032
Их сможет выполнять машина Тьюринга-Чёрча, очевидно же.

>>983999
Ну и? Представим, дальше что? Польза какая от этого?

>>984001
Лол, но его и нет. Математики захотели прикрутить и описать программирование матаном, а то как это, ЦАРИЦА ВСЕХ НАУК же.
Но практической ценности от этого минимум.

>>984086
>Польза какая от этого?
Вычислимые основания математики без парадоксов, ошибок и кризиса оснований + абсолютно корректные программы, работающие точно по заданной спецификации, без сбоев и глюков, впервые с самого начала существования программирования.
>практической ценности от этого минимум.
Довну с мейлру - безусловно. Математике и программированию польза огромная, т.к. большой шаг вперед, можно даже сказать беспрецедентный.
>>984032
>как это мне поможет с созданием персональных домашних страниц?
>созданием персональных домашних страниц
Тебе уже ничто не поможет, смирись.

>>984092
>абсолютно корректные программы, работающие точно по заданной спецификации, без сбоев и глюков, впервые с самого начала существования программирования.
Слышу эти кукареки уже лет пятнадцать и до меня лет двадцать об этом талдычат. Шел 2017 год, а воз и ныне там. И еще через 20 лет это никому не нужно будет ибо затраты несоизмеримы + гибкость на уровне железного прута, покрытого сверхпрочным графеновым покрытием

>>984097
>Шел 2017 год, а воз и ныне там.
Ну раз школьник с мейлру так сказал, то ладно.

>>984101
Проецируешь юноша?
Код обрезанного по самые уши микроядра верифицировали, достижение уровня зк

>>984104
Про идрис ты тоже не слышал, а ведь это первый ЯП с зависимыми типами с претензией на общее назначение, там даже тип IO запиили специально для работы с программами, имеющими интерфейс с пользователем. Прогресс есть и он заметен даже за последние пару лет, если не писать всякую хуйню просто чтобы возразить/поспорить, как это делаешь ты.

>>984108
Могу представить в какой анальный карнавал превращается написание чего-то более менее реального на идрисе, если даже в хаскеле идет пустая выдрочка побочного состояния, которое все равно никуда не девается, вместе с сопуствующими проблемами. Зато как охуенно рефакторить половину проекта, когда нужно внести даже самое небольшое изменение, которое не планировалось вносить изначально. Воистину, с таким подходом абстрактФакториАбстрактСинглтонПроксиНетБеан выглядит просто школьным поделием.
Но самое смешное, с чего я постоянно проигрываю, это стандартная библиотека хачкеля и почти все популярные либы\фреймворки. Как же забавно после всех кукареков об изоляции, чистоте, контроле побочного состояния и слежке за типами заглянуть в исходники и увидеть везде самую дикую империативную дрисню, которую даже сишники уже лет 20 не пишут. Огромные портянки ансейф кода, обращение к низкоуровневым примитивам, {-# UNPACK #-} {-# PACK #-}, хаки тайпчекера, инлайны, сишные вызовы, IORef, в общем открывайте любой исходник сложнее laba3 и наслаждайтесь передовыми достижениями уровня фортрана.

И еще матанопетушки, поясните почему вы так держитесь за монадки, когда посоны придумали уникальные типы, которые и применять проще и оптимизировать намного легче?

Нет, ну, серьезно. есть хоть какой-то пример решаемой задачи? Да, цифровая реализация всей математики и всё в таком духе это конечно здорово, но не сейчас. Что я могу с этими Coq сделать? Писать какие-то топологические пространства и быть уверенным, что показывая что-то по них другим Наполеонам в палате я не ошибся? Определить суммы углов треугольника для разных (евклидовая, римановая, лобачевского, сферическая) геометрий и доказать что программа сможет в любой из них работать? Доказать, что этот протокол для сетевых данных написан оптимально с точки зрения теории информации и ни больше, ни меньше учитывая костыли и старое дерьмо сделать нельзя? Может как-то удобно можно доказать (верифицировать, то есть) ядро L4, проще чем та верификация на хаскелле?

И что, вообще не будет никаких уязвимостей и ошибок?

аминь

>>984141
>>984152
>>984154
Иди нахуй, быдло.

>>984162
А могли бы выпустить брошурку с основами объясняющую даже олигофренам, все бы вступали к вам и уже через неделю всё ПО было бы свободным и без ошибок.

>>984205
>А мавроди бы мог выпустить брошурку с основами, объясняющую суть пирамиды и уже бы через неделю все вклады стали бы свободными и без процентов.

>>984205
>объясняющую даже олигофренам
Нет, такие как ты здесь не нужны.

>>984207
Да, я про это.
>>984208

>>972961 (OP)
>Target Languages (Pascal Replacement):
> LLVM
Ой бля, почему еще кто-то отвечает?

>>983715
>у него как построение на основе two-ity, как и все остальное.

Это образоное описание интуитивной идеи, а не определение. Точно так же как Марков рисовал палочки для натуральных чисел.

>>984217
Это построение натуральных чисел. Тебе уже сто раз сказали, что N исчерпывающе определяется через:
- первый акт интуиционизма Брауэра.
- нумералы Черча.
- ординалы фон Неймана.
Так нет, ты каждую весну и осень будешь вылезать и нести все ту же хуйню.

>>983843
Тогда мне объясни, я другой анон, только что вкатился. Поясни, пожалуйста, и ответь человеку, равноудалённому от абстрактной алгебры и формальной верификации программ. А то я прочитал тред по диагонали, подсматривая в вики, и кроме срача необучаемых, срача обучаемых скептиков, трололо, и чудовищного самомнения ОПа мало что понял. возможно, я сам необучаемый. Если ты ваннаби учоный, то на учоном языке есть смысл разговаривать с учоными. Представляю, как ОП пришёл в садик, и вместо того, чтобы учить детей математики на яблоках, начал с законов ассоциативности, коммутативности и дистрибутивности мложения и умножения. Ты слегка напоминаешь не ученого, а поехавшего гуру, вкатившегося суда проповедовать как будто что-то плохое, но всё же.

Короче, у меня несколько вопросов к тебе, правильно ли я понял а скорее правильно ли интуиция мне подсказывает:
1. Эта вся магия позволяет хакнуть построить более ощую теорию и разрешить проблему вычислимости и остановки программы, и, например, показать, что конкретная программа нене остановится, или не остановится, чисто формальными методами, не исполняя саму программу?
2. Это значит, что любой алгоритм можно будет выразить на каком-то метаматанязыке, и формально доказать, например, что программа остановится?
3. Можно будет делать какие-то обобщения и выводы о невычислимых проблеммах или Тьюринг-невычислимых. Что делять с невычислимыми проблемами? Они становятся манявычислимыми в этой новой системе наверное нет, не могу представить обратного?
4. Правильно ли я понял, если любой яп представим в лямбде что на этом метаязыке можно будет описать и верифицировать любую программу/подпрограмму, и перегнать ее в любой язык программирования любой парадигмы с гарантией корректного выполнения? Что сейчас мешает сделать то же самое, если выбросить требование доказанной корректности?
5. А можно будет поиметь конвертор с произвольного ЯП в ваш манязык, для того, чтобы верифицировать программу, а потом прегнать в ещё какой-то язык? Ведь если будут гарантии, то пох на чём исходник, можно и дальше на том же пилить, и конфертировать?

Ну и вдогонку более общие вопросы:
1. Где я нафантазировал, или неверно угадал?
2. Как вкатиться ньюфане как мимимум чтобы пони мать тему разговора?
3. Что из матана для этого нужно?
4. Сколько времени это учить среднеговнокодеру средней тупости, понимающему какие-то базовые основы лямбды типа аппликации, редукции, абстракции, каккирования, етц и не понимающему как работает типизированная лямбда?
5. А сколько непрограммисту?

Второй блок это даже скорее не для меня, а так, для любого интересующегося анона. Мало ли. Ты ведь проповедуешь, должен буклетики с собой носить, лал.
Есть же спискота по калкулусу, коре матх етц, по которой ньюфаги начинают учить математику в вузике. Мне вот тема чисто гипотетически интересна, но я тупой совершенно, и мне, наверное лет 100 придётся разбираться, так что пока зоонаблюдаю.

Добра тебе.

>>984231
>формально доказать, например, что программа остановится
Толсто, дальше не читал.

>>984231
Уточню немного. В общем вопрос стоит ли и как вкатиться среднекодеру, у которого недавно появился праздный интерес к лямбде и хаскелю, и как вкатываться.

>>984235
А почему нет? История показывает, что рано или поздно, вещи, неизучабельные в како-то теории, становятся изучабельными в другой теории, в которой прежняя теория или опровергается новыми данными, или уточняется и становится всего лишь частным случаем. Я вот могу понять остановится алгоритм или нет. Если взять алгоритм простейший, то могу не догадаться, а действительно понять его. А переход от простейших алгоритмов к более сложным мне выглядит похожим на индукцию. Я пони маю, что ты сейчас будешь втирать мне за нейронки и машобчик, но на самом деле никто пока не понимает как работают человеческие мозги. Может действительно можно задать коко-куюто формальную систему, и в рамках этой системы писать алгоритм, и в рамках её же проверять вычислимость по Тьюрингу.

>>983913
>Хаскелоблядь детектед
Ох как же я проиграл со слоупока в конце треда. Вголосину.

>>984216
>Ой бля, почему еще кто-то отвечает?

Это наезд на LLVM или на Pascal, или я чего-то не понял?
LLVM годная современная машина, тем более она опенсурсный конкурент проприетарщине, и будет развиваться. Только у ленивых нет компиляции в LLVM.
Pascal годный простой и мощный язык для общего назначения, дающий бинари, которые в эффективности сопоставимы с сишными. При большей вісокоуровневости языка, простоте конструкций, и турбобыстрой компиляции. Язык и компилятор тоже развиваются, смотри FreePascal. Компилятор имеет оптимизации и да'т пососать. Просто непопулярный.

>>984243
>Target Languages
>Pascal Replacement
>LLVM
У тебя в голове - каша, иди нахуй, долбоеб.

>>984239
>Я вот могу понять
Нет, ты ничего не можешь.

>>984239
Проблема останова вообще никаким боком не относятся к лямбдам хуямдам, это ты понял нихуя неправильно.
Хуй знает что ты там погугливал, но вот 4 строчка в вики Алан Тьюринг доказал в 1936 году, что проблема остановки неразрешима на машине Тьюринга.
В первых строчках вики на остальные баззворды тебе выдаст что частично рекурсивные функции, лямбды-хуямды, машина тьюринга это все разные, но эквивалентные формальные системы.
Надеюсь теперь понятно почему анон выше тебя сразу не читал. Я бы и сам на тебя желтым сбрызнул
Типизированное лямда исчиление, кубы, верификация программ, коки-поки это все про другое.
> Я вот могу понять остановится алгоритм или нет. Если взять алгоритм простейший, то могу не догадаться, а действительно понять его. А переход от простейших алгоритмов к более сложным мне выглядит похожим на индукцию. Я пони маю, что ты сейчас будешь втирать мне за нейронки и машобчик, но на самом деле никто пока не понимает как работают человеческие мозги. Может действительно можно задать коко-куюто формальную систему, и в рамках этой системы писать алгоритм, и в рамках её же проверять вычислимость по Тьюрингу.
Вот ту желание обоссать тебе лицо становиться еще сильнее, ПОНЯТЬ понимаешь ли, ты там вчера "филология во время менструаций, как найти мужа в университете" закончил читать или критику чистого разума, гумик ты наш?
То что ты по колхозно-деревенскому написал как понимание это и есть решение проблемы остановки. И она касается возможности доказать для ЛЮБОГО алгоритма, есть множество програм(алгоритмов) на которые одназначно можно определить что она таки остановиться, НО НЕ ДЛЯ ЛЮБОЙ.
Есть еще такая хуитка как недетерминированная машина тьюринга и короче мне уже лень дальше тебе расписывать.
По твоему "топику" идельаная книжка это Introduction to Automata Theory, Languages, and Computation, недавно даже видел курс на edx или udacity, специально для ленивых, я его не проходил, но вроде бы он полностью повторяет материал книги.
Однако она мало имеет отношения к темам из за которых тут неблагородные господа перекидываются какахами.

Тута еще тетраграмматон рабби Лёфа, MLTT, не вспоминали - 4 операции формирования выражений - аппликатор, абстрактор, селектор и комбинатор, 4 вида суждения, в т.ч. гипотетических, 4 правила работы с типами - formation, introduction, elimination, computation, 4 типа - Pi, Sigma, Universe, Wellordering. Основных перечисленных аспектов тоже 4, как и букв в названии теории. Давайте подумаем, кому это выгодно, и нет ли тут какого заговора.

>>984248
Почему каша? У меня всё логично. Я мог выйти из неверных предположений, так как не в теме, но это необязательно означает кашу. Я поясню.

Target language я воспринял как целевой язык кодогенерации. C llvm всё понятно, насчёт паскаля, так наверное кто-то в голове ОПа рассматривает его как целевой язык кодогенерации. Он простой, процедурный, наверное может иметь смысл перегонять алгоритм в Pascal и воспользоваться существующими плюшками компилятора, а не писать годами, фиксить, и оптимизировать компилятор. Если другие ЯП бывают целевым язвком компиляции, то почему паскаль не может?


>>984260
Для тебя, наверное, будет сюрпризом, но на большинстве естественнонаучных факультетов в наших заборостроительных вузах этот компьютер саенс не преподают. Мое невежество устранимо, а вот говённость, выливающуюся в грубость, гордыню и заносчивость устранить сложнее.

Подожду ответ ОП-а.

>>984275
>тетраграмматон
тетраграммафон

фикс

>>984280
>Pascal
содомит

>>984280
>Для тебя, наверное, будет сюрпризом, но на большинстве естественнонаучных факультетов в наших заборостроительных вузах этот компьютер саенс не преподают.
Для тебя, наврено, будет сюрприрозом но на большинстве естественнонаучных факультетах в вузах этот компьютре саейнс не преподают.
Я и есть оп, и просто копирнул шизойдный бред максимки с эрлача, чтобы посмотреть на срач. К чести анонов срач именно такой, какого я ожидал.
И я сомневаюсь что бородатый кОзак сюда захаживает, так что можешь сразу разрабатыват сраку и регаться в жж

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

>>984292>>984295

Значит я спутал того анона с тобой, и подожду его ответа. Я совершенно нихуя не понял, и мне стало интересно, что это все значит, и я спросил анона, который отстаивает отдельные вещи из ОП-поста. Но так как ОП-пост это паста, не исключено, что я спросил тоже у пасты.

>>984292
Псих был здесь и даже отписался в ЖЖ, типа анон щекочет ему тщеславие.

>>984275
Согласно Каббале, Далет, четвертая буква древнееврейского алфавита, символизирует собой физическое существование вещей, оживленных Гимело, и питается материнскими водами, источником всякой жизни (Мем, сорок).

Согласно книге Зогар: Адам, вылепленный из глины, стал результатом союза всех сторон света, соединившихся в процессе творения с природными стихиями.

в каббале — память. Четыре мира каббалы, четыре направления в пространстве и четыре иерархических уровня Торы.

>>984308
Открытую букву мем можно себе представить как источник, воды которого текут на поверхности земли, а замкнутую букву мем — как подземный источник, воды которого скрыты под землей.
Форма буквы мем напоминает лоно, являющееся «источником жизни» для материнского плода. Находясь в утробе, плод «плавает» в воде. На древнееврейском языке слово «мать» (эм), означает также «лоно». Основная согласная буква в этом слове — мем. В большинстве языков мем — доминирующий звук в слове «мать» (мама). Вообще, символом матери -природы, Хавы, «матери всего живущего», является лоно всего сущего на уровне сотворенного — после того, как она поднимается навстречу (в этом тайна приподнятой буквы ламед), чтобы принять от Адама семя жизни.
На уровне миров всякое воспроизведение рода от лона природы подчиняется своим ограничениям – «закону сохранения материи».
Лоно покидает только тот, кто когда-то вошел в него, чтобы получить питание от матери. Это питание исходит от самой природы, и оно в свою очередь питает эмбрион, пока он не достигнет полного развития, завершаемого рождением. Семя Адама, оплодотворяющее природу, является тайной постоянного превращения вселенной из небытия в реальность.
«Текущий поток, источник мудрости» намекает на душу, как бы проистекающую к низу, к телу, от ее Источника Наверху. Это происходит в основном в момент зачатия души (мир Брия), формирования (мир Иецира) , рождения (мир Асия) и в другие ключевые моменты жизни, когда духовный «корень» человека, его мазаль («мазаль» образовано от корня «назал», «течь»), светит особенно ярко. На более низких, естественных уровнях энергии этот поток продолжается в течение всей жизни. Два разных потока, представленные открытой и замкнутой буквой мем соответствуют уровням душ. Открытая мем представляет поток уровня души, осознающей себя, а замкнутая буква мем — поток уровня души, который не осознает саму себя.
Как в стихе «Кто исчислит прах Яакова и сочтет число «зачатий» Израиля», под словом «зачатий» (слово «зачатие» образовано от корня «рвиа», означающего «квадрат» (а также «четыре»)), подразумевается акт воспроизведения рода. При минимальном исполнении заповеди «плодитесь и размножайтесь», первой и потому в определенном смысле наиболее важной заповеди Торы, родители «возводят себя в квадрат», рожая сына и дочь, как это объяснялось при рассмотрении числового значения буквы далет.
Размножение, на уровне душ, не подчиняется ограничениям «закона сохранения материи». Оно скорее приносит по-настоящему новую энергию в мир. Поэтому сила размножения в душах евреев называется в теории хасидизма «силой Бесконечности».

>>984275
Когда ты пишешь на CoС, возникает стойкое понимание и ощущение, что ты пишешь не на языке придуманном человеком, а на самом языке пространства @ maxim

>>984308
Как знал, анон, как знал

>>984314

>>984332
>2017
>Гои до сих пор верят в рептилоидов

>>984341
>2017
>не верить в рептилоидов

>>984220

Все три пункта это сведение к равносильному понятию которое само нуждается в определении. Ничего нового.

>>984561
Мань, определение конструктивного объекта есть его построение. Никакого определения, оторванного от самого объекта быть не может. Правила построения сами по себе есть конструктивный объект, как и проверка корректности вывода по ним. Конструктивная система полна и выводима по Геделю. Никаких внешних определений и определений определения не требуется.

>>984561
Ты даже не можешь дать определение тому, что для тебя есть определение, веруешь в какие'то сферическик определения в вакууме. А я точно могу сказать, что определение есть вычисление, определимость есть вычислимость. Если в номинальной дефиниции дефиниенс вычислим в дифиниендум, то это и есть определение, т.е построение. А ты веруешь сам не знаешь во что и даже не можешь дать определение тому, что называешь определением. Это манярелигия, а не математика, сбрызнул желтеньким тебе з шиворот.

>>984578
>определение есть вычисление, определимость есть вычислимость
Уносите поехавшую маньку, даже в собственной конструктивной петушне не разбирается

>>984569

Т.е. ты исходишь из интуитивного представления о конструткивном процессе, а потом просто берешь N как его частный случай. Ты часом не охуел?

Как любил говаривать кнуёбок. ты попутал дискурс.

>>984578

Это у тебя манярелигия раз в базовых понятиях не можешь разобраться. Определение как минимум не должно содержать в себе самореференции иначе это хуета, а не определение. Твое "вычисление" ровно оно и есть, тоже самое как и "конструктивный процесс" у маньки потом выше.

>>984646
>потом

*постом

У меня дед шурупы закручивал ударами молотка.

Так вот, для разных задач - свои инструменты, а этот спор - контрпродуктивен.

>>984578
>А я точно могу сказать, что определение есть вычисление, определимость есть вычислимость.
Ты хоть SICP бы почитал. Как тебе определение квадратного корня поможет его вычислить?

В общем надо гнать хипстеров из професси, им всегда будет мало и они продолжат мешать говно в ведре и создавать каждый день новые языки и реплейсменты, при этом ничего не проивзодя. Всё было нормально до развития веба, из которого к нам пришли все эти петушки и превратили IT в анальную клоунаду. Тем временем технологий 30летней давности хватит для любых современных задач.

>>984639
>>984646
А я ведь сто раз на пальцах объяснял, как это возможно, с цитатами Мартин-Лёфа. Кто же вам виноват кроме ваших родителей, что вы такие тупенькие и элементарных вещей понять не можете? Каких-то самореференций навыдумывали на ровном месте, хотя у меня нигде ничего похожего нет. Залил из жопы всех ебанашек-неосиляторов ИТТ.

>>984686
У них там в конструктивном манямирке определения по другому работают, так что как раз ты обосрался.

>>984696

Обосрался - обтекай, маня. И цитатки свои в жопу засунь, ты нихуя их не понял.

>>984704
Нет, это ты нихуя не понял. Потому что ты петух с мейлру.

>>984704
>>984707
>петух с мейлру.
Вы оба.

>>984707

Хуй тебе в рыло.

>>984711
>Хуй
Не льсти себе, школьник, и не смеши своей мелкописькой.

>>984714

[Проводит шершавым по губам собеседника]

Сколько тебе лет?

>>984724
>этот школотящий школотун
Ясно.

>>984728

Съеби уже, опущенный конструктивных петух. Не позорь Маркова.

>>984732
>конструктивных
>ых
А ручонки-то дрожат, волнуется школьничек :3

Для формальной верификации программ на практике всегда использовался computation as model подход, с интенсиональными операторами, например, тройками Хора для установления состояния программы.
Computation as deduction интересует только мочёных, и к прикладному программированию отношения не имеет. Если же говорить конкретно про proof-normalization, то даже математикам похуй на эти пруверы, так что используют их только хотт-фанбои, вчера вкатившиеся из сдувшегося хаскеля. Простой индикатор: если поциент много кукарекает про основания (99% работающим математикам основания вообще похуй) - перед вами модная гуманитарная хипстоманя, ссыте ей за воротник и гоните в /math/ /ph/ /b/ на хуй.

>>972961 (OP)
>тройками Хоара

fix

>>984739
Вся вот эта бессмысленная и беспощадная функциональщина типа хаскеля и агды - это скорее computation/deduction as model.
Контрол флоу в 1м и пруфы во 2м выражаются структурами данных - чем не модель?

>>984751
Чистые ФП языки и большинство современных пруверов - это computation as deduction с использованием proof-normalization подхода.

Нужно понимать разницу.
Computation as model, это когда вычисления рассматриваются как некие мат. структуры с ипользованием таких понятий как узлы, переходы и состояния. Т.е. логика используется только как внешний инструмент, позволяющий делать те или иные утверждения об этих стуктурах. Здесь, вычисления являются моделями для логики.
В подходе же computation as proof логические выражения, например, формулы, термы, типы и доказательства сами являются частью программы, сами принимают участие в вычислениях. В этом подходе два основных метода: proof-normalization, являющийся теоретическим базисом для функциональной парадигмы и большинства пруверов и proof-search, являющийся теоретическим базисом для логического программирования и специфических систем, где доказательство нужно не строить, а скорее просто искать.

>>984950
Ну т.е. proof-normalization это когда состояние программы это некий proof-term, а её выполнение - это рекуция этого терма к нормальной форме с помощью, например, бета-редукции.
А proof-search это когда состояние программы это последовательность, включающая в себя форумулу, которую нужно доказать и набор предположений и фактов из которых она должна быть доказана, а выполнение программы - это поиск производной от этой последовательности.

Вы мне объясните, что не так с изоморфизмом Карри.Говарда? Почему логика Хоара жто тип для чотких пасанов, а пропозишены как множества своих пруф'объектов это для хипсторов, вкптившихся из хаскеля?

>>985056
Наверное, потому что второе - это программирование доказательсв (например, теорем), а первое - это доказательство программ (их свойств)? Наверное, поэтому, вся та небольшая доля формально верифицированного софта (эти в основном IBM занимается и другие любители Cleanroom), верифицированны именно тройками Хоара и тому подобным.

>>985954
>Наверное, потому что второе - это программирование доказательсв (например, теорем), а первое - это доказательство программ (их свойств)?
Но ведь свойства программ можно доказывать и через изоморфизм Карри-Говарда, достаточно применять колмогоровскую интерпретацию логических констант. Поэтому кок там и идрис вполне годятся и для верификации программ.

Успешный в треде, пишу в проде на AutumnAI, ссу на кодомакак с пирамиды маслоу.

>>986432
>AutumnAI
пиши лучше на вижуалбасике

http://maxim.livejournal.com/518690.html
Бля лол.

>>986510
Максим иди нахуй, вниманиеблядина ты этакая. Все уже видели.

>>986513
Да ладно тебе. Я вот вообще удивлен что такие люди читают двачи, т.е. тратят своё время на абсолютно ноубрейн хуйню, во как оно выходит. А вообще почитал его ЖЖ и ещё раз убедился в том, что такого рода технари как правило неприятные в общении люди. Не, я понимаю что он входит в 5% людей, но зачем так ярко этим кичиться?

>>986514
>Я вот вообще удивлен что такие люди читают двачи
>Не, я понимаю что он входит в 5% людей
Ты что ебанулся? Обычный средней скиловости прогер.

>>986518
Ну хуй знает. Средней скиловости прогер всю жизнь пишет промышленный код на жаве и даже не помышляет по части маняматики, в лучшем случае ограничиваясь сугубо прикладной хуйней типа теории графов. Максимка скорее уж бородатый задрот из университета. Непонятно, кстати, что его в хохляшке держит.

>>986528
>Средней скиловости прогер всю жизнь пишет промышленный код на жаве
Хех, это тебе в pr сказали? Всю жизнь пишут тупые макаки без особых запросов, биомусор с личиниусами к 25 годам либо вкатывальщики около 30, ну и фрилансеры 300к\с.
Любой более-менее нормальные человек потом начинает куда-то углубляться или расширятся, а сейчас особенно модно стало становиться евангелистами и форсить разную хипсторсткую хуиту. Просто максимка выбрал матан. Если бы ты крутился столько лет в этой кухне то и сам смог бы задвигать любую заумную поеботу.

>>986537
>Хех, это тебе в pr сказали? Всю жизнь пишут тупые макаки без особых запросов, биомусор с личиниусами к 25 годам либо вкатывальщики около 30, ну и фрилансеры 300к\с.
Буд-то таких не большинство.
>Любой более-менее нормальные человек потом начинает куда-то углубляться или расширятся, а сейчас особенно модно стало становиться евангелистами и форсить разную хипсторсткую хуиту.Просто максимка выбрал матан. Если бы ты крутился столько лет в этой кухне то и сам смог бы задвигать любую заумную поеботу.
Это что-то уровня подворотов и функционального программирования на жаваскрипте. Не, ну есть такой тренд, тут ты прав. Но дальше выебонов с типа блямбдой анонимной функцией тобишь дело как правило не заходит.

>>986542
>Буд-то таких не большинство.
Хуй знает как у вас в раше, сужу по говногалере в РБ, тут даже ссаные джуны с первого дня начинают дрочить разные хипсторские технологии и ебать ими мозги. Не то чтобы я считаю это чем-то плохим, не подумай. Серьезные прогеры валят те же хипстерские технологии, но уже на гораздо более солидном уровне. Распределение где-то 30-70, 70% - похуистов которые шли за деньгами ибо в РБ с зарплатой >1000 ты уже почти мажор, 30 - тех, кому это все интересно и не западло дрочить разные узкие области. Напомню что это ссаная галера с такой лютой легаси жавапарашей и астрактФакториПроксиСинглтонБинами, про которые так любят шутить в зк.
Судя по рассказам друзей, в нормальных конторах этот процент куда больше, так что про 5% ты меня посмешил. Статистика уровня "мы вам перезвоним 299 тред"

>>986599
Чисто так, не со зла, перечисли ка ты эти технологии. Я с жавомирком не слишком знаком, если что, но вроде не слыхал о том что бы ты там особые технологии народ массово юзал, ну окромя 100500 фреймворков. Хотя есть ещё котлин какой-нибудь, лол.

>>986632
Ты про то на чем пишут на работе или про трендовые вещи?

Если первое то это разная внутреняя корпоративная хуита, свои велосипеды и т.д. Какой-нибудь спринг версий где еще пишут портянки xml конфигураций - это в мире галер заебись какая прогрессивность. Тут на пятой яве далеко не все. Возможно у тебя сложилось впечатление что вся эта прогрессивщина используется на работе, но нет, ЛИГОСИ ЭВЕРИВЕР, наверняка пытаются пропихивать разное говно, однако бизнесу и тем более галере похуй на вскукареки программистов, даже адекватные

Про второе особо писать нечего. Погугли все современные тренды. Что касается ява то тут в топе биг дата с ее петушиным стеком, хотя конечно для себя все юзают скалку. Не сильно далеко от нее идет машин лернинг. Продвинутые акка посоны пояснят тебе почему эрланг и динамическая типизация говно, впрочем и его тоже любят. Ну и весь остальной хайп\нехайп типа разных, каждый год новых, уникальных nosql бд, какие-то новые суперсовременные недописанные фреймворки вроде списка Максимки. Отдельная опущеная каста функциональщиков со своими хачкелями и агдами с завтипами, дрочем на матан, куда уж без них. Лиспоебов разве что не встречал. В общем полистай зекач, тут все современные тенденции достаточно полно отражены, хоть и в извращенныой сектанской манере.

>>986655
А, понел. Правда биг дата с жавой это как по мне пиздец какой-то.

Скоро коммунизм в программировании уже?

>>992559
Нет

>>983642
К петухам из теоретической математики в самый раз. Их место всегда было у параши.

>>972961 (OP)
>Для петухов:
Требую причисления опа к лику святых программача.

>>972961 (OP)
Проиграл с наркомана.

>>996704 - вот этого, очевидно, пидорнули даже из его усть-засранского государственного, за какую-нибудь парашу даже не могу представить.

>>975711
Это сводится к проблеме останова, если доказать, что язык для описания объектов должен быть Тьюринг-полным.

>>984280
Лол, я то же самое про таргет лангуагес подумал, учитывая ллвм и то, что в окамль этот кок вроде как транслироваться может.

>>972961 (OP)
PHP 7.1 топчик для веба.
ну и Java респект!

>>986655
Петух, бигдаты, нескуэль, скалы, ерланги и Акки это вполне работающие в проде технологии, которые использует множество людей и на которые есть вакансии по всему миру.

А нытье сохацкого про матан, пруверы и какую-то ебаматематику - это просто бред поехавшего илиария, который к реальной жизни отношения не имеет вообще.

>>972961 (OP)
Какая же ОСь труъ? Темпл-ОС?

>>1011435
На экзоядре что-то.

>>1011435
https://www.youtube.com/watch?v=vOqKq9La0aw

У него, кстати, стрим.

>>1011456
> This is NOT streamed by Terry A. Davis and it's unlikely he's in the chat.
> This is a stream of archived videos from misc sources selected at random.

>>972961 (OP)
Опять технологии успешных программистов оканчиваются обсуждением экзистенциальных угроз математики. Ну ладно, хоть почитать будет чего.

>>981582
Лучше это какие? Scala, Elixir/Erlang, Clojure?
Ну да, не поспоришь, только вакансий хуй или требования пиздос.
Жаба, сишарп, питухон это то же говно только недостатки с другой стороны. Рельсы... Мне кажется что с каждым годом они всё ближе к своей смерти, неплохая идеология, но держалась лишь на энтузиастах.

>>1011528
Максим, а ты сосешь хуи?

>>1011685

Только у бандеры при этом причмокивая со словами "це КОК".

>>1011833
LEAN лучше Coq.

>>1011834
Чем лучше? inb4: чем Coq

>>1011435
Винда.

>>972977
Такое чувство что ты переписал историю становления и развития компьютерного програмиррования

>>972961 (OP)
Не назвал самую главную технологию успешных программистов ™
А именно 1С

>>972976
>>972977
Это все и 10 жизней не выучишь.

>>972961 (OP)
Язык R для статистики и другого матана.
Быдломакаки его не знают, потому работы полно, платят неплохо и конкуренция небольшая.

>>1011385
Я и не спорю, ну а про йоба математику я вообще не в курсах. О сохацком первый раз в твоем посте прочитал.

>>984737
Зайди в дискорд.

>>1019963
Сслыка?