HasLin - ett DSL för linjär algebra

Sammanfattning: Matematik är en viktig del av datavetenskap och ett vanligt förekommande ämne på teknikinriktade program på universitet är linjär algebra. Om matematik tolkas inom kontexten av ett domänspecifikt språk kan klyftan mellan matematik och datavetenskap överbryggas. Målet med projektet var därmed att skapa ett domänspecifikt språk för linjär algebra, benämnt HasLin. Arbetet var menat till att undersöka hur HasLins korrekthet kan bevisas samt hur domänen kan pedagogiskt förmedlas för att stärka framtida användares kunskaper inom domänen och datavetenskap. HasLin är inbäddat i det funktionella programmeringsspråket Haskell. För att visa HasLins korrekthet konstruerades tester i Haskell samt bevis i bevisassistenten Agda. Resultatet visar att HasLin stödjer en stor mängd grundläggande operationer för linjär algebra, däremot visas inte korrekthet i den mån syftet ämnade. HasLin är anpassat för att vara lätt-använt och är publicerat via ett webbbaserat användargränssnitt vilket tillåter användning av programmet utan ett behov av installerad mjukvara. Viss vidareutveckling behövs, främst inom test och verifikation, för att bevisa HasLins korrekthet för att bättre tjäna projektets syfte.