Lösen Sie die Speicherverwaltungsprobleme, indem Sie die Programmkorrektheit wie mit coq?

Ich wollte nur fragen, ob es möglich wäre, eine Sprache mit einem Typ-System zu konstruieren, die die Speicherverwaltung Probleme lösen kann (Speicherlecks, Dangling Pointers, Doppel free(), etc.), indem automatisch versucht, die Richtigkeit eines Programms zu beweisen mit seinen Typen als Propositionen wie mit einem integrierten coq-artigen Theorembeweiser (in der Denkweise von Programmen als Beweisen)?Lösen Sie die Speicherverwaltungsprobleme, indem Sie die Programmkorrektheit wie mit coq?

Gibt es ein grundlegendes logisches Problem bei diesem Ansatz (Stopp-Problem vielleicht?) Oder ist es nur undurchführbar? Danke für alle Antworten und es tut mir leid, dass ich nicht so versiert in diesem Bereich bin, will nur aus Neugier wissen;)

Quelle

2017-12-06 Supergravitation

Ja, indem Programmierer niemals direkten Zugriff auf Zeiger erhalten. Ähnliches geschieht in Linux mit dem 'ln'-Befehl. Normale Benutzer können damit keine Verzeichnisse verknüpfen. Verzeichnisse können nur mit dem Befehl 'mkdir' erstellt werden. Dies verhindert Speicherverwaltungsprobleme des Dateisystems. – shawnhcorey

Ja, es gab eine Menge Forschung in Sprachen, die kompilieren- Zeitspeicherverwaltung. Rust und sein Eigentumsmodell sind die branchenweit bekannteste Sprache in diesem Bereich. Vielleicht möchten Sie immer in "linear types" schauen.

Quelle

2017-12-06 20:38:57 munificent

Aber gibt es eine Möglichkeit, die Verantwortung vom Programmierer vollständig zu entfernen, während die Kompilierungszeit des Problems gelöst wird? Wie ich gehört habe, kann der Kampf mit dem Borrow-Checker in Rust ziemlich anstrengend sein. Und lineare Systeme scheinen mir ein bisschen eingeschränkt, zum Beispiel wären persistente Datenstrukturen unmöglich. – Supergravitation

Lösen Sie die Speicherverwaltungsprobleme, indem Sie die Programmkorrektheit wie mit coq?

Antwort

Verwandte Themen