А что такое "контекст типов"?.

типы типы бла бла бла. BLAH BLAH fucking BLAH.

будущее за логическим программированием, natural language processing, автокомплиты

короче я предлагаю можно сказать новую дисциплину для разработки софта на го, что судя по всему решает все проблемы связанные с тестами, логами и бенчмарками. разработчику предлагается думать про код на нескольки уровнях одновременно и перейти из однопоточного в двупоточный режим, где у него перед глазами есть как код и использование этого кода (тесты) одновременно, например. рабочий процесс программиста делится на написание, тестирование и измерение кода.
при написании кода, программист должен помнить и активно экплуатировать тот факт, что его текст будет выполняться в трех режимах: стандаратном, отладочном и трассировочном.
в стандартном режиме лог информация это то, что обязательно должны будут увидеть операторы этого кода. это варнинги, некоммуницируемые состояния и вывод. “compilation successful” не входит в число таких логов. спасибо, блядь, но лучше перезвоните нам когда compilation не будет successful… там, где писать тесты не целесообразно, достаточно log() который направляет всю информацию в пользовательский логгер: logrus, glog или что ты там будешь использовать.
в отладочном режиме по тексту лога можно понять что он делает с точностью до логических операций, объема оперируемых данных, времени исполнения отдельных рутин (это то, что касается speed но об этом чуть позже)
в трассировочном режиме текст лога должен предоставлять достаточно информации, чтобы произвести все необходимые вычисления если не в уме, то с помощью SQL терминала или его аналога под рукой. это полный уровень прозрачности, где код делает все возможное чтобы кооперировать с тобой, в т.ч. создает доп аналитику, визуализацию, выполняет вспомогательные вычисления и т.д.
тестирование становится неотъемной частью рабочего процесса. то, что ты привык делать руками, тебе теперь предлагается документировать в виде кода. предписание подразумевает что ты будешь выполнять все эксперименты с кодом посредством  зондирования. в этом режиме ты получаешь отладочный лог и все связанные с ним привелегии, но важно помнить что на минимальном уровне, зондирование — это не более чем выполнение теста. если тест валится, probe программа предлагает тебе выполнить его трассировку. особенность трассировки и главное ее отличие в том, что отладочный вывод сопровождаются ∆t информацией, а помимо доп трассировочного вывода, код полагается на speed микробенчмарки.
эта модель программирования так же адресует критику отладчиков, по типу gdb или если мы говорим про мейнстрим го, то еще и delve. существует школа prinf дебагинга и в то время как я не могу сказать что я ее приверженец, я прекрасно понимаю о чем они говорят. gdb отладочный стейт это эфемерный инструмент, варварский взгяд во внутренности программы. это не то, что поможет тебе приобрести аналитику, данные о производительости или банально лучше ее понять. в то время, как предлагаемая модель программирования опирается на несколько логов для обратной связи с кодом, во время его отладки было бы глупо не использовать отладчик.
и наконец измерение кода. если probe программа это интерфейс для проведения экспериментов, тестов кода, то speed это одновременно бенчмаркинг, нагрузочное и fuzz тестирование в одном лице. каждый программист должен понимать, что и как он измеряет. грубо говоря, можно измерять время ∆t, а можно измерять пропускную способность ∆d/∆t. это две принципиальные вещи, которые ты как правило хочешь измерять во время отладки или трассировки.
v1 версия предоставит примитивный api где данные измерений будут разноводиностью текстового лога, т.е. на экране будет рисоваться красивые ascii графики, а в файл будет писаться json с точными измерениями.
v2 версия будет полностью совместима и единственная ее функция будет заключаться в том, чтобы на основе приобретенного опыта в результате использования модели на практике, понять как именно стоит агрегировать и делать breakdown анализ измеряемых данных на уровне кода. в отношении speed программы, вторая версия добавит простой интерфейс для измерения и профилирования ∆a (allocations) и cache efficiency анализ. (для оптимизации кода)

мне кажется, что будущее это за чем-то типа agda2, когда оно тебе само программирует, а ты только подсказываешь :)

Ты изобрёл http://lighttable.com/ на который все забили

мне кажется, что будущее это за чем-то типа agda2, когда оно тебе само программирует, а ты только подсказываешь :)

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