العلامات الشائعة：
الافتراضية أمان DNS التحقق الرسمي تحليل قابلية الوصول أخطاء المترجم تضارب الماكرو امتدادات الويب إطار عمل تطوير كومودور 64 بياسيك 2.0 جميع العلامات

جسر بين الرسمي وغير الرسمي: تصميم DSL في عصر نماذج اللغات الكبيرة

2025-06-17

يستكشف هذا المنشور اتجاهًا جديدًا عند تقاطع لغات المجال المحدد (DSLs) ونماذج اللغات الكبيرة (LLMs): تصميم DSLs تتكامل بسلاسة مع سير عمل الترميز القائم على LLMs. يفصل الكاتب تجربته في استخدام LLMs لإنشاء نصوص برمجية، واكتشف أن LLMs تتفوق في إنشاء "شيفرة الربط" - ملء الهيكل الأساسي بناءً على أوصاف بلغة طبيعية، مع ترك المنطق المعقد للترميز اليدوي. تطرح هذه التجربة سؤالاً رئيسيًا: كيف يمكننا دمج هذا سير العمل بمساعدة LLMs في DSLs نفسها؟ الهدف النهائي هو سد الفجوة بين الشفرة الرسمية والمواصفات غير الرسمية بلغة طبيعية، ربما من خلال إنشاء مواصفات بلغة طبيعية تلقائيًا بناءً على تحليل نوع DSLs.

اقرأ المزيد
(kirancodes.me)
التطوير

تصور الإثبات الرياضي: رؤى من Lean Blueprints

2025-05-11

Lean Blueprints، وهي أداة تخطيط للمشاريع مستوحاة من أسلوب المخططات الذي يستخدمه الرياضيون لتوثيق الأدلة، توفر رؤى فريدة حول عملية الإثبات. تستخدم هذه الأداة رسمًا بيانيًا حيث تمثل العقد التعريفات والنظريات والفرضيات، مع ألوان تشير إلى حالتها (أخضر: مثبت، أزرق: تم ذكره ولكنه غير مثبت، أسود: غير مكتوب). من خلال تتبع التحكم في الإصدارات الخاصة بمشاريع Lean (مثل توثيق Terrence Tao للفرضية PFR)، يمكننا تصور تطور الأدلة، وكشف كيفية عمل الرياضيين وتوفير البيانات اللازمة لبناء أدوات لمساعدتهم. يوفر هذا التصور رؤى خفية سابقًا حول كيفية بناء الأدلة الرياضية.

اقرأ المزيد
(kirancodes.me)
التطوير إثبات رسمي