lapkin25 16 окт 2023 в 13:56

Язык программирования Sound

3 мин

6.7K

Программирование*Ненормальное программирование*

Комментарии 44

Zenitchik 16 окт 2023 в 14:37

Где почитать спеку языка?

lapkin25 16 окт 2023 в 14:39

В разработке. Пока спецификация - только в примерах.

Zenitchik 16 окт 2023 в 15:15

Толку от примера, который я даже прочитать не могу, потому что синтаксис не понимаю?

lapkin25 16 окт 2023 в 21:11

Синтаксис пока можно считать плавающим.

includedlibrary 16 окт 2023 в 14:59

Честно говоря, ничего из написанного не понял. Чем Sound отличается от любого существующего средства проверки теорем типа Coq или Agda, на которых можно формально доказывать корректность кода?

Технология Sound может быть реализована в рамках любого языка
программирования, поэтому язык Sound можно транслировать в любой ЯП

Что вообще значит это предложение? Sound - это язык или технология? Если язык, то возможность реализации компилятора Sound на языке X не доказывает возможность трасляции Sound в язык X. Если технология, то вообще не понятно, что такое Sound и как его траслировать.

В единственном приведённом примере кода не понятно, где собственно формальная верификация.

lapkin25 16 окт 2023 в 21:14

Спасибо за ответ, про саму верификацию ничего не говорилось. В рамках традиционного программирования спецификация в программу должна вводиться косвенно.

includedlibrary 16 окт 2023 в 22:56

Понятнее не стало. Вот, например, есть программа на си, вычисляющая сумму массива. Как мне в неё спецификацию на Sound ввести?

int sum_arr(int *arr, size_t size) {
  int result = 0;
  for(size_t i = 0; i < size; i++)
    result += arr[i];
  return result;
}

lapkin25 16 окт 2023 в 23:32

func sum (a: Sequence[Range]) -> Int = {
    k = Range.begin
    s = calc_sum(a, k) = {
        if k == Range.end:
            return 0
        else:
            return a[k] + calc_sum(a, k + 1)
    }
    return s
}

И дальше может потребоваться указать детали структуры данных ("внутренний интерфейс"), обозначенной через абстрактный тип Sequence, чтобы указать транслятору представление данных.

includedlibrary 16 окт 2023 в 23:54

Код на Sound, который вы написали, потом транслируется в код на си? Если да, то как вызывать получившуюся функцию из другого кода на си так, чтобы формальная спецификация имела смысл? Вот мы получили calc_sum, которая соответствует формальной спецификация, а потом где-то ошиблись в вызове:

int arr[12] = {0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11};
// Тут произойдёт выход за границу массива
int result = calc_sum(arr, 15);

Если нет, что с ним после написания делать?

lapkin25 17 окт 2023 в 00:18

В данном случае calc_sum - это функциональный блок внутри функции sum. Это означает, что его использование предполагается только внутри функции sum, и код составлен с проверкой выхода за границы диапазона индексов. Если функция sum составлена неточно и учтены не все случаи, то это приведет к ошибке при трансляции в язык C.

includedlibrary 17 окт 2023 в 00:23

Я перепутал название функции. Я имел в виду вызов sum в коде на си.

int arr[12] = {0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11};
// Тут произойдёт выход за границу массива
int result = sum(arr, 15);

lapkin25 17 окт 2023 в 00:27

В этом примере sum принимает на вход всю последовательность. Если допустить, что sum принимает на вход диапазон, то на C входные параметры превратятся в пару индексов, но в рамках Sound это будет поддиапазон, который по определению будет корректен.

includedlibrary 17 окт 2023 в 01:08

А можете привести пример вызова функции sum, полученной из вашего кода на си, а то я не очень понял?

lapkin25 17 окт 2023 в 01:47

int __calc_sum(int a[], int n, int k)
{
  if (k >= n)
    return 0;
  else
    return a[k] + __calc_sum(a, n, k + 1);
}

int sum(int a[], int n)
{
  int k = 0;
  int s = __calc_sum(a, n, k);
  return s;
}

Zenitchik 16 окт 2023 в 17:51

В чём генеральная мысль статьи? В системе именования переменных и типов данных?

lapkin25 16 окт 2023 в 21:13

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

Zenitchik 16 окт 2023 в 21:42

Тогда статья провальная. Проблема толком не сформулирована. Элементы, которые нужно добавить в язык - не названы. Много словоблудия и непонятный код.

Tzimie 17 окт 2023 в 08:07

Она невнятная)

AlexTOPMAN 17 окт 2023 в 07:49

Лично я против названия "звук" для языка, который к звуку даже отношения не имеет, но "протому что просто красиво".

cher-nov 17 окт 2023 в 08:08

Лично я против названия "звук" для языка, который к звуку даже отношения не имеет, но "протому что просто красиво".

Так речь здесь не про тот sound, который audio, а тот, который soundness и в "safe and sound".

Статья интересная, спасибо. Несколько пространная и путаная, но такое бывает. Поглядим, что из этого выйдет. Если я прочитал её правильно, то получается, что и сам думал над похожими вещами.

Название только и впрямь неудачное - по такому искать в интернете неудобно. Затем бренды и нужны.

habrolog 17 окт 2023 в 16:09

Так речь здесь не про тот sound, который audio, а тот, который soundness и в "safe and sound".

Отлично. И как это понять априори? Вот есть такой язык csound, 40 лет ему скоро будет, и он непосредственно про звук. И тут появляется некий sound, который не только не имеет отношения к csound, но и к звуку вообще.

funny_falcon 17 окт 2023 в 13:45

Почему в NumberToDigits next_digit и lowest_digit оформлены образом, похожим на функции? При этом вызова их нет. Очень запутывает. Тем более, что next_digit возвращает ok : Bool, но его использования не видно.

Кажется, что это - основная особенность языка, но в статье она не разжёвана.

lapkin25 17 окт 2023 в 14:07

Это именованные блоки, к которым не обязательно обращаться. Имя блока вводится для уточнения, что он делает, и чтобы обособить переменные, которые он использует. Переменная ok используется после блока next_digit, она указывает, следует ли завершить цикл.

funny_falcon 17 окт 2023 в 14:25

Если бы было ok = next_digit, я бы понял. А так вообще не понятна связь if ok и именем результирующего параметра. Почему-то с lowest_digit использовано присваивание.

lapkin25 17 окт 2023 в 14:54

Насколько допустимо такое сокращение - это сделано, чтобы не дублировать имена переменных внутри блока и вне него.

lapkin25 16 ноя 2023 в 15:45

Другой вариант функции перевода числа в список цифр:

def f(x: Num -> @a: Seq<Num>)) = {
  @a = for({@y = x; @a = []};  # здесь y - локальная переменная, @a - единственная внешняя изменяемая переменная в блоке for
    {
      @a = @a + last_digit(y, 10)
      @y /= 10
    };
    {y > 0}
  )
  def last_digit(y: Num; base: Num -> @d: Num) = {
    @d = y % base
  }
}

Здесь Num и Seq<Num> - абстрактные типы данных.

lapkin25 17 ноя 2023 в 07:09

Если нужно точнее указать зависимости,

def f(x: Num -> @a: Seq<Num>) = {
  x -> @a = for({let @y = x; @a = []};
    {
      @a.append(last_digit(y, 10))
      @y /= 10
    };
    {y > 0}
  )
  def last_digit(y: Num; base: Num -> @d: Num) = {
    @d = y % base
  }
}

В качестве одной из идей языка - максимально разграничить независимые части описания вычислений. Не только горизонтально (классическая модульность), но и вертикально (например, отделить техническую часть от логики вычислений).

lapkin25 12 янв в 10:41

Схему языка нужно будет переработать. Сначала планируется реализовать библиотеку на C++, включающую в себя классы:

type: описание типов данных с помощью индуктивно-рекурсивных определений;
purpose: описание назначений вычислений над этими типами, для чего вводится специальный класс объектов - "назначение", выражающий цель вычислений;
eval: собственно вычисления, гарантирующие решение класса задач, подпадающих под выделенное назначение.

Например, для примера с нахождением цифр числа,

type вводится так: если a - последовательность, то a x - тоже последовательность;

purpose определяет отображение x -> a, где x - число, a - последовательность, следующим образом:

f : x -> a d,

где d = x % base, a = f(x // base)

eval выполняет указанные действия.

lapkin25 13 янв в 01:44

def convert(x: Num) -> a: Seq<Num> = {
  def f(x: Num) -> a: Seq<Num> = {
    if x == 0:
      return []
    else:
      return [f(x // base), [x % base]]
  }
  y = f(x)
  return y if y else [0]
}

Теперь остается в обрамляющем блоке определить типы Num, Seq<Num>, сказать, откуда брать параметр base, и указать способ имплементации вычислений (вплоть до уточнения деталей выполнения операции []).

Zenitchik 17 янв в 20:20

Так что там на счёт спеки? Так и не разработали? Когда ждать?

lapkin25 18 янв в 01:10

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

Zenitchik 18 янв в 01:28

Не придумав способ записи, вы не сможете преобразовать свою мысль в общепонятный текст. Поэтому это именно что первой важности.

lapkin25 18 янв в 14:24

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

Zenitchik 18 янв в 15:25

Вы хотите вариться в собственном соку, или всё-таки суметь рассказать нам, в чём прикол Вашего языка?

lapkin25 18 янв в 15:37

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

Zenitchik 19 янв в 14:41

Приколов может быть сколько угодно.

Т.е. исходная статья, которую мы сейчас комментируем, утратила актуальность?

Языка не будет, расходимся?

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

Зачем?

Простите, но не похоже, что Вы пытаетесь решить какую-то реальную проблему. Похоже скорее на изобретательский зуд.

lapkin25 19 янв в 15:25

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

f(x) = f(x // base) + [x % base] при x > 0 и f(x) = [] при x = 0.

По умолчанию этот код будет транслироваться и выполняться так, как он написан.

Но если сказать, как будет выполняться + и в каком виде будут храниться данные - то могут быть разные варианты. Для этого потребуется переопределить во обрамляющем блоке способ работы со списком.

Можно заметить, что вычисление сведется к подстановкам

f(12345) =

= f(1234) + [5] =

= (f(123) + [4]) + [5] =

= ((f(12) + [3]) + [4]) + [5] =

= (((f(1) + [2]) + [3]) + [4]) + [5] =

= ((((f(0) + [1]) + [2]) + [3]) + [4]) + [5] =

= (((([] + [1]) + [2]) + [3]) + [4]) + [5] =

= ((([1] + [2]) + [3]) + [4]) + [5] =

= (([1, 2] + [3]) + [4]) + [5] =

= ([1, 2, 3] + [4]) + [5] =

= [1, 2, 3, 4] + [5] =

= [1, 2, 3, 4, 5],

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

Сделать это можно так ($ - от слова storage - указание на способ хранения данных):

def convert(x: Num) -> a: Seq<Num> = {
  def f(x: Num) -> a: Seq<Num> = {
    $a = reverse_array()  # массив, который растет влево
    if x == 0:
      return []
    else:
      return f(x // base) + [x % base]
  }
  y = f(x)
  return y if y else [0]
}

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

Zenitchik 19 янв в 16:29

Я не понимаю Ваш код. Т.к. Вы так и не выкатили спеку языка.

Пока не будет спеки - ваши опусы будете понимать только Вы сами.

lapkin25 21 янв в 00:21

Вас понял. Тогда буду постепенно формулировать спецификацию, исходя из примеров.

def reverse (a: Seq<Num> -> Seq<Num>):
  reverse([a' x]) = x, reverse(a')
  reverse([]) = []

Это пример простой левой списочной рекурсии. Запятая - операция продолжения списка. Штрих создает дамми-переменную такого же типа, которая распространяется только на текущий оператор. "Имя функции от выражения" транслируется в if, в котором проверяется равенство этого выражения и входного аргумента.

Простая правая списочная рекурсия:

def sum (a: Seq<Num>) -> Num:
  sum([x a']) = x + sum(a')
  sum([]) = 0

Стандартные операторы:

def foreach (a: Seq<Num>, op: Num -> Num) -> Seq<Num>:
  foreach([x a'], op) = op(x), foreach(a')
  foreach([], op) = []

def reduce (a: Seq<Num>, op: Num, Num -> Num, e: Num) -> Num:
  reduce([x a'], op, e) = op(x, reduce(a', op, e))
  reduce([], op, e) = e

def filter (a: Seq<Num>, pred: Num -> Bool) -> Seq<Num>:
  filter([x a'], pred) = {
    if pred(x):
      x, filter(a')
    else:
      filter(a')
  }
  filter([], pred) = []

lapkin25 21 янв в 03:46

Еще пример:

def bubble_sort (@a: Seq<Num>):
  def pass_number (@a: Seq<Num>):
    Num n = a.length
    for i in reversed_range(n - 1, 1):
      if a[i] > a[i + 1]:
        swap(@a[i], @a[i + 1])

  def sort (@a: Seq<Num>):
    pass_number(@a)
    sort(@a[range(a).remove_first()])

  sort(@a)

includedlibrary 19 янв в 14:51

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

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