Cảm ơn bạn vì câu hỏi tuyệt vời @EliBenSasson!

"Ngôn ngữ mà mọi người sẽ lập trình trong."

Như bạn đã biết, mạch đa thức được sử dụng để *xác minh*. Cairo làm mờ đi sự phân biệt này để trình bày một ngôn ngữ lập trình cụ thể cho người dùng (Cairo VM), điều này là ổn, nhưng nhiều mô hình lập trình là có thể và trong mọi trường hợp điều quan trọng không phải là những gì được mã hóa mà là những gì được xác minh.

Ví dụ: các chức năng có thể được chỉ định trực tiếp trong logic (độ đầu tiên). Đoạn 3 của bài viết cho thấy cách làm, và đặc biệt nó trình bày một số lựa chọn các chức năng, bao gồm các chức năng tự phát sinh, trong khuôn khổ của Gabbay. Trong bài viết như đã viết, đây là một định nghĩa thuyết lý nhằm mục đích đối với các nhà lý thuyết, và do đó Gabbay sử dụng số thực thay vì trường hữu hạn - nhưng rất rõ ràng các nguyên tắc tương tự sẽ áp dụng trên trường hữu hạn. Đây không phải là sự phân biệt cốt lõi.

Một trường hợp đặc biệt liên quan: rất rõ ràng từ bài viết của Gabbay rằng tính hợp lệ của cây từ điển có thể được chỉ định bằng khuôn khổ này - ví dụ, sự chỉ định của cây từ điển cho quá trình giảm tổ hợp SK, điều này thú vị bởi chính nó và bởi vì nó là điển hình cho nhiều định nghĩa khác như vậy. Các định nghĩa tự phát sinh là một nền tảng đủ và thuận tiện cho lập trình tuyên bố. Vì vậy, nếu chúng ta muốn trình bày một lập trình trừu tượng cho người dùng, đó là một cách trực tiếp, có nguyên tắc toán học để làm điều đó, bao gồm ít chi phí. Có những cách khác.

Mặc dù đoạn trên không phải là một bằng chứng toán học, tôi hy vọng điều này cho bạn cảm nhận được một phần câu trả lời cho câu hỏi.