LINUX.ORG.RU

KISS языки


1

1

Кроме ближайших родственников Оберона. С тривиальным синтаксисом, интуитивной и формально определенной семантикой. Есть такие?

PS Брейнфак не предлагать.

PPS Желающие предложить СИ отправляются учить стандарт в целом, и лютое количество таких выкрутасов в частности.

★★★★★
Ответ на: комментарий от www_linux_org_ru

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

Можно, конечно. Доказано Адой.

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

> Какое бесполезное знание. Ты должен знать, что _каждая_ из сумм лежит в диапазоне. FWIW, любой язык с «обычными» целыми не даст тебе гарантию вычисления такой суммы.

Бгг. Любой ассемблер железки с дв.-доп. кодом даст.

Пример для знаковых байтов: 127+126+125+(-124)+(-123)+(-122)=9

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

> Можно, конечно. Доказано Адой.

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

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

>> А теперь пример для 32-бит чисел на 32-бит машине.

2147483647+2147483646+2147483645+(-2147483644)+(-2147483643)+(-2147483642)=9

Что это? Где ассемблерный код, который я могу запустить и проверить?

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

> Какое бесполезное знание. Ты должен знать, что _каждая_ из сумм лежит в диапазоне.

Это вполне может быть инвариантом моего алгоритма.

любой язык с «обычными» целыми не даст тебе гарантию вычисления такой суммы


Хм. Кроме языка ассемблера, контпримеров не знаю :)

Правда, в случае какого-нибудь SML у тебя не будет и UB - будет исключение. Тебе это нужно?


Я где-то говорил, что мне нужен SML? .)

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

>> Правда, в случае какого-нибудь SML у тебя не будет и UB - будет исключение. Тебе это нужно?

Я где-то говорил, что мне нужен SML? .)

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

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

> Что это? Где ассемблерный код, который я могу запустить и проверить?

ты не врубился

пойнт в том,

ЕСЛИ программисту известно, что РЕЗУЛЬТАТ будет между INT_MIN и INT_MAX (и это отнюдь не бесполезное знание)

ТО слагаемые на асме (и -О0, хотя последнее никто не обещал) можно складывать в любом порядке (и оптимизатор это активно юзает); это характерно для дв. доп. кода, вот почему остальные вымерли

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

> Что это? Где ассемблерный код, который я могу запустить и проверить?

код мне писать влом, если тебе очень захочется — сгенерю через -О0

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

> ЕСЛИ программисту известно, что РЕЗУЛЬТАТ будет между INT_MIN и INT_MAX

Да епт... если Питон мне не врет:

>>> 2147483647+2147483646+2147483645

>>> 6442450938L

Скади, каким волшебным образом ассемблер втиснет число 6442450938 в 32-бит регистр?

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

> я бы хотел оспорить: 1. продвижения беззнакового типа к знаковому

А я бы вообще запретил любые неявные преобразования типов.

Вообще типизация в Си не достаточно сильная. Например, ptr_diff_t и size_t должны быть самостоятельными типами, а не тайпдефами. И enum-ы тоже отдельно должны быть, причем с запретом арифметики над ними.

если у целевого проца, допустим, нет байтового оператора сдвига вправо (а есть только двухбайтовый), то надо его эмулировать, а не заставлять разраба писать код под эту редкость


А я бы выкинул вообще все short/long модификаторы. И типы (u)intN_t, (u)int_leastN_t. Оставил бы только: char, int, unsigned и (u)int_fastN_t.

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

> Скади, каким волшебным образом ассемблер втиснет число 6442450938 в 32-бит регистр?

он и не втиснет; это число возьмется по модулю 2**32, но поскольку это промежуточный результат, то его неправильность нас не колышит; а вот окончательный результат будет верен

я щас тебе напишу совсем реалистичный пример, только опять для байтов — иначе придется писать мат. символы

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

>> Скади, каким волшебным образом ассемблер втиснет число 6442450938 в 32-бит регистр?

он и не втиснет; это число возьмется по модулю 2**32, но поскольку это промежуточный результат, то его неправильность нас не колышит

Короче, код в студию. Разговор уже стал бессмысленным.

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

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

Я мечтаю об упрощенном (в смысле семантики) потомке Си. Еще я подозреваю, что у меня «Си головного мозга». Поэтому и завел этот топик - посмотреть, какие есть языки с простой семантикой.

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

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

Я мечтаю об упрощенном (в смысле семантики) потомке Си.

Заметь, ты снова не ответил на вопрос о желаемой семантике. Походу, ты и сам ее не знаешь.

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

int у нас 8 бит

pi(x)=4+x-[x/2]-[x/3]-[x/5]-[x/7]+[x/6]+[x/10]+[x/14]+[x/15]+[x/21]+[x/35]-[x/30]-[x/42]-[x/70]-[x/105]

int x;

[] это целая часть

pi(х) это количество простых чисел от 0 до х

формула верна при 7<x<121

при этих х доказано, что 4<pi(x)<x

____________________________________________

в результате:

1. на си ты не имеешь права складывать слагаемые в любом порядке, а должен следить, чтобы после *каждого* сложения не было переполнения

2. на асме можно складывать в любом порядке

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

> Короче, код в студию. Разговор уже стал бессмысленным.

я не представляю, чем тебе поможет простыня, сделаная objdump -S из gcc -О0

возможно, *ты* считаешь си тем, что предлагает жцц, но *я* говорю о *стандарте* си

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

> я не представляю, чем тебе поможет простыня, сделаная objdump -S из gcc -О0

Ничем. Мне поможет короткий столбик из movl и addl

возможно, *ты* считаешь си тем, что предлагает жцц

Речь вообще не о Си, а об ассемблере.

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

че-то я записал слишком математически; на си это будет проще (7<x<121):

int pi(int x) { return 4+x-x/2-x/3-x/5-x/7+x/6+x/10+x/14+x/15+x/21+x/35-x/30-x/42-x/70-x/105; }

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

Речь вообще не о Си, а об ассемблере.

я щас запустил gcc -g -Wall -O0 и немного охренел

да, видимо придется руками написать цепочку... хотя лень


#include <stdio.h> 
#include <stdlib.h> 

int pi(int x) { return 3+x+x/6+x/10+x/14+x/15+x/21+x/35-x/2-x/3-x/5-x/7-x/30-x/42-x/70-x/105; }

/* 1 мы не считаем простым числом */

int main(int argc, char** argv)
{
    if( argc!=2 ) return 1;
    printf("pi(%d)=%d\n", atoi(argv[1]), pi(atoi(argv[1])));
    return 0;
}
www_linux_org_ru ★★★★★
()
Ответ на: комментарий от www_linux_org_ru

движок не принимает целиком (это objdump -S)

int pi(int x) { return 3+x+x/6+x/10+x/14+x/15+x/21+x/35-x/2-x/3-x/5-x/7-x/30-x/42-x/70-x/105; }
 80483d4:	55                   	push   %ebp
 80483d5:	89 e5                	mov    %esp,%ebp
 80483d7:	53                   	push   %ebx
 80483d8:	83 ec 08             	sub    $0x8,%esp
 80483db:	8b 45 08             	mov    0x8(%ebp),%eax
 80483de:	8d 58 03             	lea    0x3(%eax),%ebx
 80483e1:	8b 45 08             	mov    0x8(%ebp),%eax
 80483e4:	89 45 f8             	mov    %eax,-0x8(%ebp)
 80483e7:	c7 45 f4 ab aa aa 2a 	movl   $0x2aaaaaab,-0xc(%ebp)
 80483ee:	8b 45 f4             	mov    -0xc(%ebp),%eax
 80483f1:	f7 6d f8             	imull  -0x8(%ebp)
 80483f4:	89 d1                	mov    %edx,%ecx
 80483f6:	8b 45 f8             	mov    -0x8(%ebp),%eax
 80483f9:	c1 f8 1f             	sar    $0x1f,%eax
 80483fc:	89 ca                	mov    %ecx,%edx
 80483fe:	29 c2                	sub    %eax,%edx
 8048400:	89 d0                	mov    %edx,%eax
 8048402:	01 c3                	add    %eax,%ebx
 8048404:	8b 4d 08             	mov    0x8(%ebp),%ecx
 8048407:	c7 45 f4 67 66 66 66 	movl   $0x66666667,-0xc(%ebp)
 804840e:	8b 45 f4             	mov    -0xc(%ebp),%eax
 8048411:	f7 e9                	imul   %ecx
 8048413:	c1 fa 02             	sar    $0x2,%edx
 8048416:	89 c8                	mov    %ecx,%eax
 8048418:	c1 f8 1f             	sar    $0x1f,%eax
 804841b:	89 d1                	mov    %edx,%ecx
 804841d:	29 c1                	sub    %eax,%ecx
 804841f:	89 c8                	mov    %ecx,%eax
 8048421:	01 c3                	add    %eax,%ebx
 8048423:	8b 4d 08             	mov    0x8(%ebp),%ecx
 8048426:	c7 45 f4 93 24 49 92 	movl   $0x92492493,-0xc(%ebp)
 804842d:	8b 45 f4             	mov    -0xc(%ebp),%eax
 8048430:	f7 e9                	imul   %ecx
 8048432:	8d 04 0a             	lea    (%edx,%ecx,1),%eax
 8048435:	89 c2                	mov    %eax,%edx
 8048437:	c1 fa 03             	sar    $0x3,%edx
 804843a:	89 c8                	mov    %ecx,%eax
 804843c:	c1 f8 1f             	sar    $0x1f,%eax
 804843f:	89 d1                	mov    %edx,%ecx
 8048441:	29 c1                	sub    %eax,%ecx
 8048443:	89 c8                	mov    %ecx,%eax
 8048445:	01 c3                	add    %eax,%ebx
 8048447:	8b 4d 08             	mov    0x8(%ebp),%ecx
 804844a:	c7 45 f4 89 88 88 88 	movl   $0x88888889,-0xc(%ebp)
 8048451:	8b 45 f4             	mov    -0xc(%ebp),%eax
 8048454:	f7 e9                	imul   %ecx
 8048456:	8d 04 0a             	lea    (%edx,%ecx,1),%eax
 8048459:	89 c2                	mov    %eax,%edx
 804845b:	c1 fa 03             	sar    $0x3,%edx
 804845e:	89 c8                	mov    %ecx,%eax
 8048460:	c1 f8 1f             	sar    $0x1f,%eax
 8048463:	89 d1                	mov    %edx,%ecx
 8048465:	29 c1                	sub    %eax,%ecx
 8048467:	89 c8                	mov    %ecx,%eax
 8048469:	01 c3                	add    %eax,%ebx
 804846b:	8b 4d 08             	mov    0x8(%ebp),%ecx
 804846e:	c7 45 f4 31 0c c3 30 	movl   $0x30c30c31,-0xc(%ebp)
 8048475:	8b 45 f4             	mov    -0xc(%ebp),%eax
 8048478:	f7 e9                	imul   %ecx
 804847a:	c1 fa 02             	sar    $0x2,%edx
 804847d:	89 c8                	mov    %ecx,%eax
 804847f:	c1 f8 1f             	sar    $0x1f,%eax
 8048482:	89 d1                	mov    %edx,%ecx
 8048484:	29 c1                	sub    %eax,%ecx
 8048486:	89 c8                	mov    %ecx,%eax
 8048488:	01 c3                	add    %eax,%ebx
 804848a:	8b 4d 08             	mov    0x8(%ebp),%ecx
 804848d:	c7 45 f4 eb a0 0e ea 	movl   $0xea0ea0eb,-0xc(%ebp)
 8048494:	8b 45 f4             	mov    -0xc(%ebp),%eax
 8048497:	f7 e9                	imul   %ecx
 8048499:	8d 04 0a             	lea    (%edx,%ecx,1),%eax
 804849c:	89 c2                	mov    %eax,%edx
 804849e:	c1 fa 05             	sar    $0x5,%edx
 80484a1:	89 c8                	mov    %ecx,%eax
 80484a3:	c1 f8 1f             	sar    $0x1f,%eax
 80484a6:	89 d1                	mov    %edx,%ecx
 80484a8:	29 c1                	sub    %eax,%ecx
 80484aa:	89 c8                	mov    %ecx,%eax
 80484ac:	8d 0c 03             	lea    (%ebx,%eax,1),%ecx
 80484af:	8b 55 08             	mov    0x8(%ebp),%edx
 80484b2:	89 d0                	mov    %edx,%eax
 80484b4:	c1 e8 1f             	shr    $0x1f,%eax
 80484b7:	01 d0                	add    %edx,%eax
 80484b9:	d1 f8                	sar    %eax
 80484bb:	89 cb                	mov    %ecx,%ebx
 80484bd:	29 c3                	sub    %eax,%ebx
 80484bf:	8b 45 08             	mov    0x8(%ebp),%eax
 80484c2:	89 45 f8             	mov    %eax,-0x8(%ebp)
 80484c5:	c7 45 f4 56 55 55 55 	movl   $0x55555556,-0xc(%ebp)
 80484cc:	8b 45 f4             	mov    -0xc(%ebp),%eax
 80484cf:	f7 6d f8             	imull  -0x8(%ebp)
 80484d2:	89 d1                	mov    %edx,%ecx
 80484d4:	8b 45 f8             	mov    -0x8(%ebp),%eax
 80484d7:	c1 f8 1f             	sar    $0x1f,%eax
 80484da:	89 ca                	mov    %ecx,%edx
 80484dc:	29 c2                	sub    %eax,%edx
 80484de:	89 d0                	mov    %edx,%eax
 80484e0:	29 c3                	sub    %eax,%ebx
 80484e2:	8b 4d 08             	mov    0x8(%ebp),%ecx
 80484e5:	c7 45 f4 67 66 66 66 	movl   $0x66666667,-0xc(%ebp)
 80484ec:	8b 45 f4             	mov    -0xc(%ebp),%eax
 80484ef:	f7 e9                	imul   %ecx
 80484f1:	d1 fa                	sar    %edx
 80484f3:	89 c8                	mov    %ecx,%eax
 80484f5:	c1 f8 1f             	sar    $0x1f,%eax
 80484f8:	89 d1                	mov    %edx,%ecx
 80484fa:	29 c1                	sub    %eax,%ecx
 80484fc:	89 c8                	mov    %ecx,%eax
 80484fe:	29 c3                	sub    %eax,%ebx
 8048500:	8b 4d 08             	mov    0x8(%ebp),%ecx
 8048503:	c7 45 f4 93 24 49 92 	movl   $0x92492493,-0xc(%ebp)
 804850a:	8b 45 f4             	mov    -0xc(%ebp),%eax
 804850d:	f7 e9                	imul   %ecx
 804850f:	8d 04 0a             	lea    (%edx,%ecx,1),%eax
 8048512:	89 c2                	mov    %eax,%edx
 8048514:	c1 fa 02             	sar    $0x2,%edx
 8048517:	89 c8                	mov    %ecx,%eax
 8048519:	c1 f8 1f             	sar    $0x1f,%eax
 804851c:	89 d1                	mov    %edx,%ecx
 804851e:	29 c1                	sub    %eax,%ecx
 8048520:	89 c8                	mov    %ecx,%eax
 8048522:	29 c3                	sub    %eax,%ebx
 8048524:	8b 4d 08             	mov    0x8(%ebp),%ecx
 8048527:	c7 45 f4 89 88 88 88 	movl   $0x88888889,-0xc(%ebp)
 804852e:	8b 45 f4             	mov    -0xc(%ebp),%eax
 8048531:	f7 e9                	imul   %ecx
 8048533:	8d 04 0a             	lea    (%edx,%ecx,1),%eax
 8048536:	89 c2                	mov    %eax,%edx
 8048538:	c1 fa 04             	sar    $0x4,%edx
 804853b:	89 c8                	mov    %ecx,%eax
 804853d:	c1 f8 1f             	sar    $0x1f,%eax
 8048540:	89 d1                	mov    %edx,%ecx
 8048542:	29 c1                	sub    %eax,%ecx
 8048544:	89 c8                	mov    %ecx,%eax
 8048546:	29 c3                	sub    %eax,%ebx
 8048548:	8b 4d 08             	mov    0x8(%ebp),%ecx
 804854b:	c7 45 f4 31 0c c3 30 	movl   $0x30c30c31,-0xc(%ebp)
 8048552:	8b 45 f4             	mov    -0xc(%ebp),%eax
 8048555:	f7 e9                	imul   %ecx

www_linux_org_ru ★★★★★
()
Ответ на: комментарий от www_linux_org_ru
 8048557:	c1 fa 03             	sar    $0x3,%edx
 804855a:	89 c8                	mov    %ecx,%eax
 804855c:	c1 f8 1f             	sar    $0x1f,%eax
 804855f:	89 d1                	mov    %edx,%ecx
 8048561:	29 c1                	sub    %eax,%ecx
 8048563:	89 c8                	mov    %ecx,%eax
 8048565:	29 c3                	sub    %eax,%ebx
 8048567:	8b 4d 08             	mov    0x8(%ebp),%ecx
 804856a:	c7 45 f4 eb a0 0e ea 	movl   $0xea0ea0eb,-0xc(%ebp)
 8048571:	8b 45 f4             	mov    -0xc(%ebp),%eax
 8048574:	f7 e9                	imul   %ecx
 8048576:	8d 04 0a             	lea    (%edx,%ecx,1),%eax
 8048579:	89 c2                	mov    %eax,%edx
 804857b:	c1 fa 06             	sar    $0x6,%edx
 804857e:	89 c8                	mov    %ecx,%eax
 8048580:	c1 f8 1f             	sar    $0x1f,%eax
 8048583:	89 d1                	mov    %edx,%ecx
 8048585:	29 c1                	sub    %eax,%ecx
 8048587:	89 c8                	mov    %ecx,%eax
 8048589:	29 c3                	sub    %eax,%ebx
 804858b:	8b 4d 08             	mov    0x8(%ebp),%ecx
 804858e:	c7 45 f4 9d c0 09 9c 	movl   $0x9c09c09d,-0xc(%ebp)
 8048595:	8b 45 f4             	mov    -0xc(%ebp),%eax
 8048598:	f7 e9                	imul   %ecx
 804859a:	8d 04 0a             	lea    (%edx,%ecx,1),%eax
 804859d:	89 c2                	mov    %eax,%edx
 804859f:	c1 fa 06             	sar    $0x6,%edx
 80485a2:	89 c8                	mov    %ecx,%eax
 80485a4:	c1 f8 1f             	sar    $0x1f,%eax
 80485a7:	89 d1                	mov    %edx,%ecx
 80485a9:	29 c1                	sub    %eax,%ecx
 80485ab:	89 c8                	mov    %ecx,%eax
 80485ad:	89 da                	mov    %ebx,%edx
 80485af:	29 c2                	sub    %eax,%edx
 80485b1:	89 d0                	mov    %edx,%eax
 80485b3:	83 c4 08             	add    $0x8,%esp
 80485b6:	5b                   	pop    %ebx
 80485b7:	5d                   	pop    %ebp
 80485b8:	c3                   	ret

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

> очень интересный ассемблер из -О0

Каие-то конкретные претензии есть?

ты не находишь?

Я на него внимательно даже не смотрел. Мне нужно было выражение 2147483647+2147483646+2147483645+(-2147483644)+(-2147483643)+(-2147483642) на ассемблере, а не дамп результатов работы компилятора.

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

> Походу, ты и сам ее не знаешь.

Вот моя ultimate fantasy.

1. Zero overhead. Код должен более-менее прозрачно мапиться в ассемблер. Для широкого круга процессоров, от армов до итаников.
2. Контракты вместо интерфейсов. Объект может находиться в одном из классов состояний. Методы переводят объект из одного класса состояний в другой.
3. Валидация. Выполнение контрактов формально проверяется компилятором. Параллельно основному коду программы расположены подсказки для валидаторного солвера. Можно подключать формально доказанные где-то в сторонке теоремы. Можно вводить аксиомы («на коране клянус!1»), о которых валидатор будет отчитываться. Аксиомы нужны как минимум для описания поведения системных вызовов.
4. Анализ сложности. Вместе с валидацией должна строиться worst-case оценка сверху количества операций (арифметических, обращений в память, разных классов системных вызовов), оценка сверху потребляемого места (стек, куча, диск). Требования к классу сложности - часть контракта.

Семантика должна быть простой, чтобы хоть как-то облегчить ужасный пункт 3.

======

Можно вообразить полностью замкнутую систему, с валидированной ОС (очевидно, микроядерной), валидированной файловой системой (параллельно с файлом может храниться класс его состояния; например, что это валидный jpeg), и запуском только валидированных программ.

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

Мир безглючного софта.

======

Сейчас все дружно напишут, что эта корова никогда не взлетит. Но помечтать-то можно? :D

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

s/cx/cl/g

и напомню, что инт у нас 8 бит — иначе формула дохрена большая нужна

mov  %cl,  %bl ; %bl = x 
add  %cl,  3   ; %cl = result 
mov  %ax,  %bl 
idiv $0x3 
sub  %cl,  %al 
mov  %ax,  %bl 
idiv $0x5 
sub  %cl,  %al 
mov  %ax,  %bl 
idiv $0x7 
sub  %cl,  %al 
www_linux_org_ru ★★★★★
()
Ответ на: комментарий от www_linux_org_ru

> асм предполагался типа такого:

Сколько стоит idiv, ты в курсе? Если гугль мне не врет, то 46 циклов на P1 (при делении 32-битовых чисел - ты оперируешь именно ими). В твоей функции 14 делений. Тебе всё еще кажется странным ассемблер, выданный gcc?

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

> Сколько стоит idiv, ты в курсе? Если гугль мне не врет, то 46 циклов на P1 (при делении 32-битовых чисел - ты оперируешь именно ими). В твоей функции 14 делений. Тебе всё еще кажется странным ассемблер, выданный gcc?

в 0 приближении: мне насрать на такты, я просил -О0

в 1 приближении: все те эквивалентные вроде бы преобразования, что сделал жцц, имеют право использовать то, что в стандарте переполнение целых — это UB; и ты по-прежнему утверждаешь, что в этой каше мне не надо следить за переполнением *каждого* результата (вместо переполнения окончательного результата, которое не может случиться — это доказано)?

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

> Wet dream.

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

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

1. микроядерность нереалистична пока что

2. верифицированный файл без ЦП требует неких новых механизмов от ОС и неизвестно насколько надежен

а в целом — думаю взлетит.

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

> в 0 приближении: мне насрать на такты, я просил -О0

Ясно. И результат -O0 определен как «то, что смог придумать www_linux_org_ru».

все те эквивалентные вроде бы преобразования, что сделал жцц, имеют право использовать то, что в стандарте переполнение целых — это UB

Ты хочешь сказать, что твой код с idiv выдаст на каких-то входных данных ответ, отличный от кода gcc, или что?

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

> На пк общего назначения - пожалуй, да.

какой-то мягко говоря странный подход

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

опять же, надо предоставлять возможности, а не требовать «все программы верифицированы для исполнения в RT»

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

> На кардиостимуляторе или на бортовом компьютере пассажирского лайнера - оно того стоило бы.

Wet dream в том смысле, что кроме слова «валидация сделает всё заипись», в твоей фантазии вообще ничего нет. Это всё равно, что сказать «Хотел бы я трахнуть Анджелину Джоли» (или кто там сейчас считается фап-мишенью планеты).

А так - Шапиро уволили из M$ и он вернулся к разработке BitC.

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

> Ты хочешь сказать, что твой код с idiv выдаст на каких-то входных данных ответ, отличный от кода gcc?

Я хочу сказать, что ни ты, ни стандарт си не гарантируют, что такой казус невозможен.

Тогда где мне взять кроссплатформенный ассемблер?

И результат -O0 определен как «то, что смог придумать www_linux_org_ru»

нет. это всего лишь инвалидирует твой аргумент про такты.

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

> то по каким-то причинам, пусть даже не очень четко, но причины эти должны быть описаны

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

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

>> И результат -O0 определен как «то, что смог придумать www_linux_org_ru»

нет. это всего лишь инвалидирует твой аргумент про такты.

Доо. Определи мне «результат -O0», а?

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

> Wet dream в том смысле, что кроме слова «валидация сделает всё заипись», в твоей фантазии вообще ничего нет.

Идея-то простая как два пальца: чтобы программа сопровождалась доказательством, что она ведет себя более-менее вменяемо.

И акцент не на «заипись», а на том, как оно (доказательство) могло бы выглядеть.

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

> И акцент не на «заипись», а на том, как оно (доказательство) могло бы выглядеть.

Я не понял даже, что именно должно доказываться (только не говори «корректность».

P.S. тебе-то самому твои слова не напоминают бессмертное «можно грабить корованы»? :)

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

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

Что программный код в самом деле реализует контракт.

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

> А так - Шапиро уволили из M$ и он вернулся к разработке BitC.

А вот это интересно. Спасибо за линк.

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

> Определи мне «результат -O0», а?

Я не утверждал, что та простыня не -О0, а утверждал что она странная — а точнее, нет гарантии, что в ней не использовано предположение о непереполнении.

И кстати — раньше ты напирал на «здравый смысл при -О0»; как твой здравый смысл поживает вместе с такой простыней?

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

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

Так это очевидно. Взлетать должна система, которая предоставляет возможность сосуществовать верифицированной и невирифицированной частям.

И еще — софт, особенно серверный, более-менее стабилизировался, и надежность может привлечь больше внимания, чем свистелки-перделки.

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

> А так - Шапиро уволили из M$ и он вернулся к разработке BitC.

да, интересно.

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

ну так ты проигнорировал пока неудобный вопрос

ты мне сможешь гарантировать, что та жцц-шная хрень при переполнении целых выдаст тот же результат, что очевидный код mov ... idiv ... sub ... ?

а если не сможешь, то исполняет ли си роль кроссплатформенного ассемблера даже с -О0?

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

> раньше ты напирал на «здравый смысл при -О0»

Если не хочешь неоправданных предположений оптимизатора - не исполльзуй оптимизацию.

как твой здравый смысл поживает вместе с такой простыней?

Пока ты не предъявишь реальных претензий к коду, с моим здравым смыслом всё нормально.

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

ну так ты проигнорировал пока неудобный вопрос

ты мне сможешь гарантировать, что та жцц-шная хрень при переполнении целых выдаст тот же результат, что очевидный код mov ... idiv ... sub ... ?

а если не сможешь, то исполняет ли си роль кроссплатформенного ассемблера даже с -О0?

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