?

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

TeX [May. 18th, 2016|10:43 pm]
beroal
[Tags|]

Постепенно осваиваю TeX. Не для интереса, а по нужде. Чудны дела твои, Господи.
Link8 comments|Leave a comment

амёба и человек [May. 11th, 2016|10:28 am]
beroal
[Tags|, ]

Несколько раз наблюдал следующий феномен на постсоветском пространстве. Человек заявляет, что он будет что-то учить, и приглашает других, но очень быстро это начинание глохнет. Я насчитал 5 случаев. Именно с нашими, советскими людьми. :-) Возможно, просто мне такие люди попадаются или я настолько не интересен. Причины феномена можно выдумать разные.

А заголовок имеет следующий смысл. Есть поговорка, что неправильное поведение амёбы устраняется только вместе с амёбой, потому что амёба не способна учиться. Естественный отбор. Учится популяция.
LinkLeave a comment

потому что мы пилоты [May. 6th, 2016|06:28 pm]
beroal
[Tags|, , ]

Видел вакансию «Работник в фирму Intel на конвейер в Польше». Вспомнил анекдот: «Как, мне уйти из авиации?!»
Link1 comment|Leave a comment

a working XFS driver for Windows [Apr. 28th, 2016|11:51 pm]
beroal
[Tags|, ]

Introduction

When you are looking for a driver of XFS, a well-known filesystem for Unix, for the Windows operation system, Linux forums leave the bitter word “impossible” in your heart. If you end up here for the same reason, I have good and bad news for you. The good news is, there is a XFS driver for Windows by Crossmeta/Pavitrasoft. Yes, it works despite what you read on the web. The bad news is, it works with old versions of XFS only. I guess this is a stumbling point for many users. Another obstacle is the absence of reasonable documentation for the driver and the presence of outdated skimpy tutorials. This is true even for the official manual. No wonder users feels frustrated.

This manual expects you to know basic commands and command-line shells of Linux and Windows, for example, how to view contents of a directory.

to be continuedCollapse )

Conclusion

Actually, this task turned out to be easy in contrast to what I was preparing for. In its current state, the driver is not as useful as it can be. I believe that Crossmeta programmers are able to upgrade their driver so it will support the newest version of XFS, but, unfortunately, I was not able to reach them.
LinkLeave 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

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