主要观点：

• 类型系统（尤其是依赖类型系统）可增加所描述对象的可信度，需明确规范并静态检查其实现，但要信任类型系统本身的正确性。
• Agda 未定义核心语言，现启动“Agda Core”项目，旨在构建其正式指定的核心语言及类型检查器参考实现。
• Agda Core 的目标包括减少可信代码库、实现独立检查器等，需满足有正式规范、小类型检查器等条件，且全部用 Agda 实现。
• 实现 Agda Core 面临诸多挑战，如变量和定义符号的作用域、表示 case 树、保留归约期间的共享、处理非终止性、类型化与非类型化转换、处理擦除注释以及 agda2hs 的相关问题等。

关键信息：

• Agda 无核心语言，“Agda Core”项目旨在构建。
• 项目目标及需满足条件。
• 实现过程中的各种设计挑战和基础设施挑战。
• 结论是虽耗时且仍有很多工作，但这是有意义的项目，欢迎交流讨论。

重要细节：

• 不同类型系统目的及信任问题。
• Agda Core 各主要组件及相关实现细节。
• 设计挑战如变量作用域表示、case 树表示、共享保留、非终止处理、类型化转换等的具体情况。
• 基础设施挑战如擦除注释相关问题、agda2hs 的局限性及改进等。