coqのようなプログラムの正確性を証明することによってメモリ管理の問題を解決しますか？

Question

私は、メモリ管理の問題（メモリリーク、ダングリングポインタ、ダブルfree()など）を解決できるタイプシステムで、プログラムの正確性を自動的に証明することで言語を構築することが可能かどうかを質問したかっただけです統合されたcoqのような定理証明（証明のようなプログラムの考え方のような）のような命題としての型を持つか？

このアプローチには根本的な論理的な問題がありますか（問題はおそらく停止していますか？）、それとも実現不可能なのでしょうか？お返事ありがとうございます。私はこの分野に精通しておらず、好奇心から知りたいと思って申し訳ありません）

Answer 1

はい、コンパイルを実行する言語については、リアルタイムメモリ管理。 Rustとそのオーナーシップモデルは、この分野で最も重要な業界言語です。いつでも "linear types"を調べることができます。