Rekisteröidy

Ilmoitukset

Ladataan…

    Näytä kaikki

    Lean ohjelmointi

    Lean ohjelmointikielellä voi varmistaa matemaattisia todistuksia ja sen mathlib sisältää yli 70 000 teoreemaa/lemmaa.

    Onko mitään oppikirjaa tai youtube luentosarjaa aiheesta, mistä kyseisen ohjelmointikielen voisi oppia. Oletteko kokeilleet?
    6112
    Äänestä

    Muut lukivat myös

    Vastaukset 6

    Vanhimmat

    Vaikuttaa hyvältä kieleltä. En ole kovin guru osaaja. Olen koettanut guuglailla ohjeita ja kysyä kielimalleilta.

    Äänestä

    Kaikki missä kirjotetaan komentoja ja "koodia" ei ole ohjelmointia Toi kuullostaa enemmänkin matemaattiselta kuvauskieleltä eikä niinkään ohjelmointikieleltä. Ihan vastaavasti en ole koskaan ymmärtänyt sitä miksi jotkut laskee SQL:n muka ohjelmointikieleksi vaikka kyseessä on kieli millä tehdään kyselyitä tietokantaan..

    Äänestä

    • Lean on ihan oikea ohjelmointikieli (puhtaan funktionaalinen ohjelmointikieli)
      mutta sen lisäksi se on matemaattisten todistusten oikeellisuuden tarkastusjärjestelmä.
      Algoritmitkin eli ohjelmat voidaan todistaa oikeiksi (eli ne tekee sen mitä väitetään tekevän)

      Periaatteessa Leanilla tehdyt ohjelmat ovat aina toimivia ja virheettömiä. Tosin siinäkin on mahdollisuus käyttää "do" komentoa joka ohittaa verifioinnit. "Do" periaatteessa on komento joka tarkoittaa "tee niin kuin käsketty äläkä kysele"

      Äänestä

    Jokaisen matemattikon olisi syytä opetella Lean. Eikä haittaa olisi jos ohjelmoijatkin tutustuisivat siihen, koska se on ylivertainen ohjelmointikieli (kun pysytään teoreettisessa tietojenkäsittelyssä). Tietenkään Leania ei ole tarkoitettu pelien, tietokantojen käsittelyn, käyttöliittymien ohjelmointiin eli pragmaattiset ohjelmat tehdään edelleen muilla kielillä (c,c++,c#,java)

    Äänestä

    Curry-Howardin lause kertoo, että
    matemaattiset todistukset ovat isomorfisia eli yhtä pitäviä
    algoritmien eli ohjelmien kanssa.

    Äänestä

    Mathlibissä on jo 240 000 teoreemaa...and counting...

    Äänestä

    Odottaa vastausta

    Näihin keskusteluihin ei ole vielä vastattu. Ole ensimmäinen.

    Luetuimmat keskustelut

    Kommentoi aloitusta

    Anonyymi-ap kirjoitti:

    Lean ohjelmointikielellä voi varmistaa matemaattisia todistuksia ja sen mathlib sisältää yli 70 000 teoreemaa/lemmaa.

    Onko mitään oppikirjaa tai youtube luentosarjaa aiheesta, mistä kyseisen ohjelmointikielen voisi oppia. Oletteko kokeilleet?

    Anonyymi
    5000

    Ilmoita asiaton sisältö

    • Sisältää materiaalia, joka on loukkaavaa, herjaavaa, rasistista, uhkailevaa tai ahdistelevaa.

    • Materiaali sisältää nimiä, yhteystietoja tai muita henkilökohtaisia tietoja. Julkisuuden henkilöistä, julkisissa viroissa toimivista ihmisistä sekä yritysten vastuuhenkilöistä saa keskustella työhön liittyen. Myös yksityiselämään liittyvistä asioista voi keskustella siltä osin, kuin niistä on julkisesti kerrottu.

    • Sisältää lapsille haitallista tai heiltä kiellettyä materiaalia. Seksuaalinen sisältö on sallittua aiheeseen tarkoitetuilla palstoilla, joiden ikäraja on 18 vuotta.

    • Lainvastaista sisältöä voi olla mm. yksityiselämää loukkaavan tiedon levitys, kiihottaminen kansanryhmää vastaan, laiton uhkaaminen, alaikäisiin liittyvä seksuaalinen sisältö/grooming, petokset, identiteettivarkaudet, kunnianloukkaukset ja tekijänoikeusrikkomukset.

    • Sisältö ei liity palstan tai keskusteluketjun aiheeseen.

    • Viesti ei ole suomea tai ruotsia (pl. International Forums), se sisältää mainontaa, se sisältää tekijänoikeuksin suojattua materiaalia, se on massapostitus tai jokin muu syy.

    Jaa keskustelu