идрис сыр, см. посты lj\thedeemon. Лучше кококо бери. Хоть возни побольше, зато и уверенности в результате больше.

опа опа

@gds говно для академопетухов, без будущего в ирл жизни

@ulidtko ну пиздец, ты вообще понел что сказал? Куча проектов, куча применений, сравни с идрисом. Тот же CompCert чего стоит. Frama-C, Why. Теорема о четырёх красках (ведь она очень важна для картографии!11111). Я вон порой проверяю логику своего кода в кококо, потом уверен в результате. Ну пиздец ты.

@gds бля ну лемму йонеды и в агде тоже доказывали, и чо? на кокококе написали уже хотя бы [тотальный брейнфак], ну или тетрис/змейку на худой конец? [тотальный брейнфак]: https://github.com/wouter-swierstra/Brainfuck

@gds Почитаю по тегу идрис, спасибо. Та я чисто пока обед жую глянул, если всерьёз браться -- можт и Coq, не шарю. В целом -- понравился из видео ответ Идриса на монад-трансформеры хаскеля для эффектов (в язык встроили костыли прикольные, кароч, в квадратных скобочках в определении типа тупо перечисляешь всякое списком).

@ulidtko БНВ.Атмосфера // две, по сути схожие вещи, обе крутые, обе мало кому нужны -- и всё равно обязательно обговнить одну из них, ну

@ulidtko йонеда лол, нахуй она нужна, тривиальщина эта. Если про игрушки, кококо написали хрень по решению-доказательству игрушки 2048, например. Брейнфак пишется легко, коиндукция в руки и вперде, с теми же свойствами, как по твоей ссылке. Просто никому нахуй не нужно. А про нужное -- ты CompCert посмотрел?

@kb так прикольно же!11

@kb в идрисе есть ещё такая ультраприколюха: [кодген в жс](http://bnw.im/t/idris) и баги в тайпчекере лол (на самом деле не баги, но пиздец бугур когда там "Name {a1039} is not bound", а у тебя в коде даже Ctrl+F не находит такое (уже зарепорчено (вроде дизайнят какой-то там фикс для етого)))

@gds а лол, я как раз на подобном хачкелеговне (Copilot) кой-чего писать начал

@kb t

@ulidtko Да. Будь я менее ленивым -- сделал бы ответ Соловьёву с его КложеСкриптом, который в живую писал змейку на прошлой фпрог-конференции со сцены. Особенно круто было бы писать без просмотра того, что она работает, а потом хуяк-хуяк, скомпилировалась => работает.

@ulidtko > http://meow.bnw.im/p/C9UUDK > @238328 что ж ты делаешь :'(

@kb ахахахах // сорь, тоже *боль*

@ulidtko coq умеет экстрактить в ocaml и в haskell, а из них уже в жс легко, причём не только доказанный код, но и остальное, что там рядом в проекте. Не такая уж приколюха.