http://ivan-gandhi.livejournal.com/3493927.html?thread=57238311#t57238311
Я общался со спутникостроителями, а также с любителями Ады (я не спрашивал где они работали, насколько я понимаю - военка).

Так вот если в двух словах, на спутниках ничего не верифицируют, но в правильных конторах у них есть стенды - софтверный эмулятор спутника и в особо правильных еще и хардверный эмулятор спутника (то есть буквально макет спутника, в котором есть часть исполнительных устройств и датчиков, и программа на нем отрабатывает какие-то этапы полета).

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

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

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

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

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

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

Вобщем какой там ООП - там процедурно всё.

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

Теоритически можно ожидать что верификацию делают энергетики и химпром, и тут это как раз моя первая специальность, я живьем часть проектов видел и с людьми общался, но реально у них контроллеры часто эмулируют релейные схемы, и тоже методология водопад, так что там все проверки делаются на уровне главного инженера и/или архитектора и плюс закладывается некоторая избыточность средств защиты от ошибок, а потом во время эксплуатации объекта ошибки постепенно отлавливают (естественно вместе с аварийными отключениями).

На Маска выйти пока не довелось. Допускаю что у него несколько иначе, поскольку Маск автомобилист по образованию.

С самолетчиками общался, так у них автопилот совершенно тупая, но чувствительная машина, чуть кто на борту чихнет, он сразу отключается и больше рулить не пытается.

А эти которые "буран" делали, у них тоже был водопад, и они для типа верификации сделали язык графический, у которого программы являются чертежами, которые соответствуют требованиям госта на ЕСКД :))))

Sparse Procedural Volumetric Rendering

Один из главных отососов в современных языках программирования - это отсутсвие во многих из них поддержки keyword arguments.

Эта хуйня существенно повышает читаемость и, как следствие, качество кода.

В некоторых ЯП, в которых есть встроеные литералы для словарей проблема может решаться ими.
В остальных - это мрак, отсос и говно.

Как ни странно, божественная статическая типизация тут не роляет совершенно. Ведь очень легко перепутать аргументы с одинаковыми типами местами и потом долго ломать голову какого Х не работает. В случае keyword args достаточно поверхностного осмотра кода, чтобы понять что не так.

GPU text rendering with vector textures.
http://wdobbie.com/post/gpu-text-rendering-with-vector-textures/
demo

Вот тут кто-то [наговнил] либу для параллелизма для Rust:

let total_price = stores.par_iter()
.map(|store| store.compute_price(&list))
.sum()


Конечно мало сделать параллелизм простым, его надо сделать ещё и безопасным. Rayon гарантирует, что использование его API никогда не приведёт к гонке данных.

Мне вот интересно, неужели в rust нет способа захватить ref на Weak Box и таким образом выстрелить себе в ногу (ну или организовать race condition).

Не слишком ли громкое заявление?

Олсо, реквестирую подобных либ для плюсцов.

ADTs in Typed Racket with macros

Немного изящного (макроебства)[http://lexi-lambda.github.io/blog/2015/12/21/adts-in-typed-racket-with-macros/] и в тайпед/ракетке можно юзать ADT с паттерн матчингом.
(Прямо как во взрослых крутых языках).

(define-datatype Expr
  (Value Number)
  (Add Expr Expr)
  (Subtract Expr Expr)
  (Multiply Expr Expr)
  (Divide Expr Expr))

(: evaluate (Expr -> Number))
(define (evaluate e)
  (match e
    [(Value x)      x                            ]
    [(Add a b)      (+ (evaluate a) (evaluate b))]
    [(Subtract a b) (- (evaluate a) (evaluate b))]
    [(Multiply a b) (* (evaluate a) (evaluate b))]
    [(Divide a b)   (/ (evaluate a) (evaluate b))]))

> (evaluate (Add (Value 1)

                 (Multiply (Divide (Value 1) (Value 2))
                           (Value 7))))
4 1/2

Интересно, ебанется ли кто-нить достаточно чтобы набыдлить какой-нить аналог хаскеля или scalaz?

Просто и элегантно.
Спасибо динамической типизации!

#lang racket
(require math)
(require racket/match)

(define (inverse func)
  (match func
    ['exp log]
    ['cos acos]
    [_ #f]))

(printf "Inv[~a](~a) = ~a\n" 'exp (exp 1) ((inverse 'exp) (exp 1)))
(printf "Inv[~a](~a) = ~a\n" 'cos 1       ((inverse 'cos) 1))

http://pasterack.org/pastes/74110

Inv[exp](2.718281828459045) = 1.0
Inv[cos](1) = 0


Охуенно выразительно и красиво. Спасибо статической типизации.

struct Node<T> { 
    prev: Raw<T>, 
    next: Link<T>, 
    elem: T, 
} 

type Link<T> = Option<Box<Node<T>>>; 

struct Raw<T> { 
    ptr: *mut Node<T>, 
} 

pub struct LinkedList<T> { 
     len: usize, 
     head: Link<T>, 
     tail: Raw<T>, 
} 

Новая ракетка вышла.

Roughly, hygienic macro expansion is desirable for the same reason as lexical scope: both enable local reasoning about binding so that program fragments compose reliably. The analogy suggests specifying hygienic macro expansion as a kind of translation into lexical-scope machinery. In that view, variables must be renamed to match the mechanisms of lexical scope as macro expansion proceeds. A specification of hygiene in terms of renaming accommodates simple binding forms well, but it becomes unwieldy for recursive definition contexts (Flatt et al. 2012, section 3.8), especially for contexts that allow a mixture of macro and non-macro definitions. The renaming approach is also difficult to implement compactly and efficiently in a macro system that supports “hygiene bending” operations, such as datum->syntax, because a history of renamings must be recorded for replay on an arbitrary symbol.

In a new macro expander for Racket, we discard the renaming approach and start with a generalized idea of macro scope, where lexical scope is just a special case of macro scope when applied to a language without macros. Roughly, every binding form and macro expansion creates a scope, and each fragment of syntax acquires a set of scopes that determines binding of identifiers within the fragment. In a language without macros, each scope set is identifiable by a single innermost scope. In a language with macros, identifiers acquire scope sets that overlap in more general ways.

http://www.cs.utah.edu/plt/scope-sets/index.html

yay отличная книжка чтобы освежить память и накидать пару несложных нейронок на своем уютном маня-язычке.

http://neuralnetworksanddeeplearning.com/

Почему python популярнее рубей, хотя Руби превосходит python по следующим пунктам:
- Метапрограммирование (т.е возможность написания DSL)
- Более серьезная поддерка FP (TCO, простой function composition syntax, pattern matching)
- Более серьезная поддержка OOP (mixins)
- Более серьезная функциональность для обработки текста
- Больший динамизм/расширяемость
- Поддержка continuations
- Однозначность синтаксиса
- Нет такого цирка как python2 vs python3
- Многострочные лямбды

Srsly python выигрывает только за счет того, что для него тупо больше биндингов ко всяким либам.

Пока что вижу ответ: так получилось. Prove me wrong.

the Strict language extension*

Add a new language extension -XStrict which turns all bindings strict
as if the programmer had written a ! before it. This also upgrades
ordinary Haskell to allow recursive and polymorphic strict bindings.

https://github.com/ghc/ghc/commit/46a03fbec6a02761db079d1746532565f34c340f

Все теперь можно думать о том, чтобы учить хаскель. // Ну или Ocaml

Кстати, спалите haskell vs ocaml в вопросах:
* C-FFI
* многопоточности
* ease of deployment
* поддержки ARM
* легкости получения soft realtime

Олсо, кто-нить объекты в Ocaml юзает или это шутка?
Наткнулся на такой комент на HN:
/However, with a few minor tweaks (e.g. an option type), I would rather have the C# type inference than the OCaml one. The reason is that, if I want to do something very clever, I will not find myself limited to code that I can actually prove to the OCaml compiler as correct: I have, time and time again, resorted to reflection and code generation to work around such situations. In other words C#'s Obj.magic is a lot more powerful (and safe, and expressive) than OCaml's.

A fairly good example is Eliom's way of expressing the parameters of a service. In C# you would write in a PageController class

public Details Update(PageId id, UserId user, [PostBody] Details body) 

and have your web framework automatically bind this to POST /page/update/{id}?user={user} with the appropriate serialization for PageId and UserId. And writing such a framework is easy: a couple hundred lines of code, with run-time type safety.

In OCaml you have to understand the entire Eliom_parameter framework: https://ocsigen.org/eliom/4.2/api/server/Eliom_parameter Just think of the mental firepower needed to create that framework in the first place!/

What Every Computer Scientist Should Know About Floating-Point Arithmetic
http://docs.oracle.com/cd/E19957-01/806-3568/ncg_goldberg.html

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

Вот, например:

bool result =
  a_if_and<boost::variant<T>,  boost::none> (
    {msg.getString(v[1]), msg.getString(v[2]), msg.getString(v[3]), msg.getString(v[4])},

  // at least one operand == boost::none
  [&](unisgned int first_null, const std::tuple<boost::variant<T>, boost::variant<T>, ...> &evalValues) { 
    std::cerr << "value " << first_null "is bad" << std::endl;
    return false;
  },

  // otherwise                                                  
  [&](const std::tuple<boost::variant<T>, boost::variant<T>, ...> &evalValues) {
    std::cout << "value 0 =" << evalValues.get(0).get<T> << std::endl;
    std::cout << "value 1 =" << evalValues.get(1).get<T> << std::endl;
    // ...
    return true;
  });

То есть, a_if_end eval-ит аргументы и каждый на неравенство boost::none.
И в зависимости от этого дергает мою лямбдочку.
Что есть чо похожее? Или я слишком охуел?

http://www.cs.kent.edu/~jmaletic/papers/ICPC2010-CamelCaseUnderScoreClouds.pdf

tldr: camelCase - хуйта

cedet - это огромный такой (поэтому хуево протестированый) кусок кода.

Сегодня обнаружил, что company-complete отваливается со стектрейсом в буферах где нет активного semantic-mode.

Оказывается эта падла модифицирует completion-at-point-functions', который юзает бекенд company-capf, своими хуками, которые отвалиюваются сerror' если в буфере не включен semantic-mode, а кроме как для C или C++ он нахер не упал.

Набыдлил хак, может кому пригодится.

Аноны, меня вдруг осенило, что всякое дрочево типа ФП и модных фреймворков нинужны и в 99% случаев мы занимаемся скучным говном. 

Это норма. Большая часть программистской работы это айти-сантехника - создание машинных переводчиков с одного языка на другой (с HTTP-запросов в SQL-запросы и т.д. и т.п. в интерпрайзе программирование это сплошная серилизация и десериализация).

Когда программисты это понимают они придумывают новые языки и фреймворки чтобы быть сантехником было веселее - получается что ты совмещаешь рутинную работу и решение головоломки о том как соединить твои новые трубы причудливой формы чтобы по ним потекли данные. (есть правда ещё деталь - если сантехник изобретает новую трубу/фреймворк которая входит в моду у других прогрессивных сантехников то он может добавить это в своё резюме и требовать больше денег за свою работу). Больше всего в этом преуспели хаскеллисты которые сделали целый язык-головоломку в котором простейшие задачи требуют решения кубиков-рубиков абстрактной теории групп. Чтобы головоломки в хаскиле всегда оставались свежими постоянно выходят расширения его системы типов. Этот язык успешно распространяется тем же принципом что и головоломки "а тебе слабо решить? чё, тупой чтоли?".

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

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

sooqa, раньше SDL2 глючил и бажил под wayland, теперь вот cairo-gl забагованый.