LINUX.ORG.RU

Albatross 0.1 — это язык программирования со статической верификацией

 albatross, , proof assistant,


0

2

Albatross — это язык программирования со статической верификацией и средство доказательства теорем. Компилятор написан на OCaml 4.

Описание языка (PDF)

Страница загрузки

>>> Подробности

★★★★★

Проверено: fallout4all ()
Последнее исправление: fallout4all (всего исправлений: 1)

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

Napilnik ★★★★★
()
Ответ на: комментарий от Napilnik
модуль Список это
  тип 'а т = Ничего | Пара 'а * 'а т
  пусть голова список =
    сопоставить список с_образом
      Ничего -> ошибка "Пустой список"
    | Пара (а, б) -> а
  пусть хвост список =
    сопоставить список с_образом
      Ничего -> ошибка "Пустой список"
    | Пара (а, б) -> б
  пусть рекурсивно применить_к фун список =
    сопоставить список с_образом
      Ничего -> Ничего
    | Пара (а, б) -> Пара (фун а, (применить_к фун б))
конец
olibjerd ★★★★★
() автор топика
Ответ на: комментарий от Napilnik

Это лишнее, в данном контексте. Тем более, точка нужна для перехода к типам и значениям внутри модуля.

olibjerd ★★★★★
() автор топика
Ответ на: комментарий от olibjerd

Это лишнее, в данном контексте.

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

Тем более, точка нужна для перехода к типам и значениям внутри модуля.

Так в этом случае слева и справа от точки буквы, а когда в конце программы - за точкой уже ничего не следует.

Napilnik ★★★★★
()
Ответ на: комментарий от loz

А конец с точкой - для грамотных русских. Очень прикольная фича, если не поломана, когда после окончания программы компилятор не разбирает что написано дальше и не выдаёт ошибок по поводу написанных там шпаргалок и пояснений с фрагментами кода. Поэтому окончание программы надо прописывать конкретно, а без точки - не очень конкретно. Мало ли сколько «концов» будет внутри программы.

Napilnik ★★★★★
()
Последнее исправление: Napilnik (всего исправлений: 1)
Ответ на: комментарий от Napilnik

Очень прикольная фича, если не поломана, когда после окончания программы компилятор не разбирает что написано дальше и не выдаёт ошибок по поводу написанных там шпаргалок и пояснений с фрагментами кода

Ты сейчас описал литературное программирование для идиотов.

loz ★★★★★
()
Ответ на: комментарий от loz

Хотя нет, до ЛП твоему описанию еще далеко.

loz ★★★★★
()
Ответ на: комментарий от olibjerd

конец

в данном случае заканчивает
модуль

Ну и как этот конец не перепутать с концом заканчивающим блок?

Napilnik ★★★★★
()
Ответ на: комментарий от loz

Ты сейчас описал литературное программирование для идиотов.

анеидиотызнакипрепинаниянеставятиразбираюткодиспользуябиблиотекулибастрал

Napilnik ★★★★★
()
Ответ на: комментарий от Napilnik

В каком месте тебе не хватает тут знаков препинания? Алсо при чем тут код? И вобще это чятик по линуксу или углубленному изучению русского языка?

loz ★★★★★
()
Ответ на: комментарий от loz

В каком месте тебе не хватает тут знаков препинания?

Везде где они нужны.

Алсо при чем тут код?

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

И вобще это чятик по линуксу или углубленному изучению русского языка?

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

Napilnik ★★★★★
()
Ответ на: комментарий от Napilnik

Везде где они нужны.

Кому нужны?

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

Ты еще скажи на паскале нельзя написать систему верстки уровня TeХ.

А нужно делать так

Кому нужно?

loz ★★★★★
()
Ответ на: комментарий от loz

Кому нужны?

Человекам.

Ты еще скажи на паскале нельзя написать систему верстки уровня TeХ.

На паскале можно написать практически всё и скриптовой паскаль тоже есть, но при чём тут сейчас он? У него с синтаксисом всё в порядке, патчика для русификации только не хватает.

Кому нужно?

Людям говорящим на русском языке и умеющим писать не только транслитом. Невозможность нормально написать английским недоалфавитом имя функции или переменной - вымораживает.

Napilnik ★★★★★
()
Ответ на: комментарий от olibjerd

Осталось понять для чего нужен альбатрос. Функциональщина предполагает задрачивание на математику, которая не математикам не очень то и необходима, мягко говоря. В императивщине же всё конкретно: если видишь репу, то размахнись и стукни по ней без танцев с бубном и хождения кругами.

Napilnik ★★★★★
()
Последнее исправление: Napilnik (всего исправлений: 1)
Ответ на: комментарий от Napilnik

В Смолтоке есть конец с точкой. А Смолток был когд-то переведен на русский язык, называлось оно «Полиглот». Вот.

yoghurt ★★★★★
()
Ответ на: комментарий от Napilnik

Осталось понять для чего нужен альбатрос.

Для доказательства теорем.

Функциональщина предполагает задрачивание

Не предполагает.

В императивщине же всё конкретно

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

olibjerd ★★★★★
() автор топика
Ответ на: комментарий от SystemD-hater

Просто ещё никто не собрал PCIE-плату для аппаратного ускорения арифметики Пеано.

thriller ★★
()
Ответ на: комментарий от buddhist

Всем, очевидно

Ну, не знаю. Какая-то помесь Eiffel и Coq. Может, что-то еще. Может, на Haskell замахнулись? :)

Zubok ★★★★★
()
Последнее исправление: Zubok (всего исправлений: 1)
Ответ на: комментарий от Napilnik

Функциональщина предполагает задрачивание на математику

Нет.

ymn ★★★★★
()

Интересно посмотреть как оно устроено унутре. Сорцов вроде бы не очень много, надо будет потыкать на досуге.

ymn ★★★★★
()

Сколько для него вакансий в рф и какая средняя зп?

DELIRIUM ☆☆☆☆☆
()

Авторы Тернера перечитали штоле?

anonymous
()
Ответ на: комментарий от Napilnik

Кажется, у клоуна обострение по весне началось. Пора санитаров звать.

anonymous
()

allthough version 0.1 is not yet able to compile real programs

risenshnobel ★★★
()
Ответ на: комментарий от Napilnik

Поэтому окончание программы надо прописывать конкретно, а без точки - не очень конкретно.

А многотичие что будет обозначать?

mandala ★★★★★
()
Ответ на: комментарий от bookman900

Область применения сего чуда?

На лоре холиварить.

mandala ★★★★★
()
Ответ на: комментарий от mandala

А многотичие что будет обозначать?

Две горизонтальные точки хорошо применять при определении диапазонов массивов и множеств

[1..100]

Napilnik ★★★★★
()

Альбатрос

Застрахуй братуху.

x4DA ★★★★★
()
Вы не можете добавлять комментарии в эту тему. Тема перемещена в архив.