Почему для проверки по типу записи необходимо делать процедуру с параметрами VAR или IN ?

Не совсем так, такой необходимости нет. Дело в другом - в языке была сделана попытка сделать недопустимыми бессмысленные проверки, которые всегда имеют одно и то же значение. В большинстве случаев для записей проверка имеет смысл только для ссылок, поставляющие данные извне, которые неявным образом задаются VAR и IN -параметрами. Отсутствие возможности проверки типа для разыменованного указателя - это побочный эффект такого ограничения и его можно считать упущением языка, так как здесь она тоже осмысленна. Это некритично, так как в таких случаях всегда можно проверить тип по указателю, не прибегая к разыменованию, хотя и может потребоваться объявить именованный указатель на соответствующую запись, если он не был предоставлен с самого начала.



Это, скорее, для раздела Почему в Обероне сделано так?

По поводу бессмысленных проверок с заранее известным результатом - можно ли вот такой пример считать примером бессмысленных проверок:

Я скорее думаю, что реализация оператора IS (и оператора WITH) не подразумевает прямое использование разыменованного указателя (динамического типа) как статического типа записи, поэтому требуется отдельная процедура, где разыменованный указатель (с помощью идентификатора VAR или IN) приводится к статическому типу записи

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

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

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

1. Можете сказать, зачем Вам нужна проверка типа записи у разыменованного указателя вместо проверки непосредственно указателя?

И вернёмся к примеру.
2. Понимаете, почему в процедуре проверка типа записи VAR-параметра осмысленна, так как фактический тип параметра в вызванной процедуре неизвестен?
3. Понимаете, почему проверка типа записи непосредственно объявленной переменной бессмысленна, так как её тип в момент проверки известен?

1. Разыменованный указатель не подобен статической записи, так как точный тип структуры разыменованного указателя в общем случае неизвестен статически и здесь, действительно, можно было бы проверять тип, но эта проверка легко заменяется на проверку указателя без его разыменования и это по сути ничего не меняет. Большинство людей никогда не встречается с необходимостью проверки типа разыменованного указателя, а не его самого. То есть, смысл есть, но насущной потребности нет.
2. Параметры-переменные для записей по своим свойствам частично подобны указателям на записи.
3. В КП указатели и VAR и IN-параметры и только они позволяют ссылаться как на непосредственно тот тип записи, что был указан в объявлении, так и на номинально расширенные от него записи, поэтому в этих и только в этих случаях проверка имеет смысл.

1. Разыменованный указатель не подобен статической записи, так как точный тип структуры разыменованного указателя в общем случае неизвестен статически и здесь, действительно, можно было бы проверять тип, но эта проверка легко заменяется на проверку указателя без его разыменования и это по сути ничего не меняет. Большинство людей никогда не встречается с необходимостью проверки типа разыменованного указателя, а не его самого. То есть, смысл есть, но насущной потребности нет.
2. Параметры-переменные для записей по своим свойствам частично подобны указателям на записи.
3. В КП указатели и VAR и IN-параметры и только они позволяют ссылаться как на непосредственно тот тип записи, что был указан в объявлении, так и на номинально расширенные от него записи, поэтому в этих и только в этих случаях проверка имеет смысл.

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

Вы очень странно интерпретируете правила языка. Рассматривайте язык как простейшую машину, которая способна выполнять код согласно описанию языка. Это, кстати, правда - язык программирования - это абстракция вычислительной машины.

Конкретно WITH можно конструктивно выразить через IS и var(Type), ровно как и наоборот. Не стоит искать сложные интерпретации в духе того, как это может делать человек. Конструкцию языка ничего не рассматривают.