?

Log in

язык, на котором не говорят [entries|archive|friends|userinfo]
beroal

[ website | personal website ]
[ userinfo | livejournal userinfo ]
[ archive | journal archive ]
[ tags | journal tags ]

in English [Jul. 1st, 2020|12:00 am]
beroal
[Tags|]

Welcome!

Posts in English in this blog.

Functional programming, computer science, mathematics.

My favorite links from Diigo: RSS, HTML.

OpenSearch plugin for searching on:

Short proofs in Coq.

test link
Link2 comments|Leave a comment

по-русски [Jun. 1st, 2020|12:00 am]
beroal
Добро пожаловать!

Для обратной связи пишите сюда комментарии. Если я вас не добавляю в друзья, это не значит, что я вас не читаю.

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

Поисковые системы на платформе Google Custom Search Engine:
против мошенничества

only Haskell (the programming language)

OpenSearch plugin (то есть для Firefox) для поиска по:

Математические доказательства на языке Coq. В основном мелочь, среди крупных модулей можно выделить CategoryTheory, IntBipart (целые числа как кольцо Гротендика), TakeDrop («take» и «drop» из Haskell.Data.List).

Лента выбранных мною из чужих блогов записей: RSS, HTML. Содержание примерно такое же, как и у данного блога, то есть функциональное программирование, программирование в целом, информатика, реже математика и физика. Надеюсь, вы найдёте в ней интересных людей.

Кто не является моим другом, должен вводить CAPTCHA при добавлении комментария. Я добавляю в друзья всех вменяемых комментаторов, поэтому стукните мне, если я конкретно о вас забыл.

У меня есть личный веб-сайт.
Link6 comments|Leave a comment

программы-спецификации, или как философия обманывает [Dec. 25th, 2015|10:07 am]
beroal
[Tags|, , ]

Я думаю, вы слышали утверждение, что в хорошем языке программирования программы являются спецификациями. Мол, к этому мы все должны стремиться. Почему, собственно, программы должны быть спецификациями? Если программа отличается от спецификации, тогда надо доказать, что программа удовлетворяет спецификации, то есть верифицировать эту программу. А верификация — это кака (при обосновании этого утверждения могут ссылаться на Гёделя). Если программа есть спецификация, то ничего доказывать не надо (утверждение 0). Круто!

Читати даліCollapse )
Link7 comments|Leave a comment

почему стандарты написаны плохим языком [Dec. 21st, 2015|12:30 pm]
beroal
[Tags|]

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

Когда я взял в руки книгу «Java precisely» by Sestoft, я увидел, что есть донкихоты, которые пытаются разрушить эту монополию. Она точный документ (стандарт), и она показывает, как надо писать стандарты. Но она не официальный стандарт. Я надеюсь, что таких ударов по монополиям будет больше.
Link3 comments|Leave a comment

edX/Paradigms of Computer Programming – Fundamentals [Dec. 8th, 2015|10:43 pm]
beroal
[Tags|, , ]

Originally posted by beroal at edX/Paradigms of Computer Programming – Fundamentals
First, I should say that I am no newbie in programming, so I don't know how newbies will perceive this course. As you probably know, there are two courses: “Fundamentals” and “Abstraction and Concurrency.” I took “Fundamentals” as a prerequisite to “Abstraction and Concurrency.”

This course starts with functional programming which is a good thing because it prevents the imperative mindset. The course introduces an operational semantics of a programming language and its use in verification. This heavy lean to computer science is unusual among programming courses. Even some elementary exercises got me thinking. So this approach definitely is good. It's a pity that it is almost neglected in “Abstraction and Concurrency.”

There are lectures on data structures (for example, trees) and efficiency (complexity) of algorithms. IMHO, they are a bit shallow. The Courseware of this course is short on code examples and exercises. If this is your first programming course, read the provided textbook.

Exercises should be done in the Oz programming language. Oz is exotic. I recommend you to read the part of the textbook on its syntax and semantics. Thus you avoid frustration. And the semantics of Oz studied here will be used in “Abstraction and Concurrency.” So this course really is required for “Abstraction and Concurrency.”
LinkLeave a comment

обучение и оценка [Nov. 23rd, 2015|07:07 pm]
beroal
[Tags|]

By way of comparison, the arrangement of having teachers act as both instructors and assessors is akin to asking the judges in a gymnastics competition to also coach the gymnasts leading up to the event, or asking a restaurant manager to conduct official food handling inspections at his restaurant. In many domains of life, we recognize that we create problematic conflicts of interest if we ask people who produce or perform to also provide the ratings of their outputs for external audiences. Yet, in education it is the norm to ask teachers to both coach their students and rate their students’ academic achievements.

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

источник

Читати даліCollapse )
Link3 comments|Leave a comment

закрыть TCP-соединение [Nov. 20th, 2015|05:46 pm]
beroal
[Tags|, ]

Никогда не мог понять, зачем в TCP позволено закрывать трубы по отдельности. (TCP-соединение состоит из 2 антипараллельных труб.) Если надо обозначить, что по какой-то трубе больше не будет данных, это можно встроить в протокол. Скорее всего, это уже встроено, например, по трубе передаётся 1 сообщение, которое содержит свою длину. Если связь рвётся или компьютер выключается, закрываются обе трубы. Программа, которая обрабатывает закрытие соединения, сложнее в случае, если позволено закрывать трубы по отдельности.
Link1 comment|Leave a comment

recursion is fast, bro [Nov. 19th, 2015|12:42 pm]
beroal
[Tags|, , , ]

Originally posted by beroal at recursion is fast, bro
“Use recursion to solve problems much faster than conventional Java technqiues.” Нашёл эту фразу в описании курса по программированию. Что бы она значила?
Link2 comments|Leave a comment

Coursera/Introduction to Mathematical Thinking [Oct. 3rd, 2015|12:11 am]
beroal
[Tags|]

Это отзыв о курсе по дедукции от Стэнфордского университета.

Под дедукцией я понимаю умение читать и писать математические доказательства. То есть этот курс помогает перейти от школьной математики к абстрактной математике, где надо доказывать. Ну, в школьной математике тоже иногда надо доказывать, но там можно как-то опереться на практический опыт. На английском такие курсы называются transition, то есть (introduction|transition) to (abstract|advanced) mathematics.

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

Читати даліCollapse )
Link7 comments|Leave a comment

прототип программы для peer-to-peer обмена статьями [Sep. 20th, 2015|11:34 pm]
beroal
[Tags|, ]

Когда-то я описывал идею системы для кросспостинга на форумы. Я сделал прототип. Он примитивен и предназначен для программистов. Инструкция вложена. Параметры моего узла:
  • cert: file
  • host: home.beroal.in.ua
  • port: 13950
LinkLeave a comment

navigation
[ viewing | most recent entries ]
[ go | earlier ]