Lean ohjelmointi

Anonyymi-ap

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?

4

82

Äänestä

    Vastaukset 4

    Anonyymi (Kirjaudu / Rekisteröidy)
    5000
    • Anonyymi00001

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

    • Anonyymi00002

      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..

      • Anonyymi00003

        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"

    • Anonyymi00004

      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)

    Ketjusta on poistettu 0 sääntöjenvastaista viestiä.

    Takaisin ylös

    Luetuimmat keskustelut

    1. Kysely : Juuri kukaan ei halua nykyisen hallituksen jatkavan

      Ylen kysely: Juuri kukaan ei halua nykyisen hallituksen jatkavan – eivät edes halli­tus­puolueiden omat kannattajat Kes
      Hallitus
      126
      1486

    2. Salaisuudet paljastuu

      Viimeiset hetket meneillään ottaa yhteyttä. Kertoa totuus ja selvittää asioita. Viimeiset hetket meneillään jos joku
      Ikävä
      142
      1304

    3. Kelan mukaan veronpalautukset ovat tuloa tuet lähti

      https://www.is.fi/taloussanomat/art-2000012225387.html Verohallinnon maksama veronpalautus tulee niille, jotka ovat mak
      Maailman menoa
      109
      784

    4. Sinkkujen tilanne kiinassa katastrofaalinen

      800 naista osallistui sinkkujen iltaan, paikalle saapui 0 miestä. Ei mahdollisuuksia, kun nainen on 38 -vuotias, ja
      Sinkut
      118
      750

    5. Mies, minkä tiedon juuri nyt haluaisit

      tietää hänestä, naisesta?
      Ikävä
      55
      653

    6. Luulin sua silloin 10 vuotta nuoremmaksi..

      🤣
      Ikävä
      47
      618

    7. Aloitan kiertotalouden

      Aloitin tänään kiertotalouden, ei mulla nyt oikeastaan muuta MOI
      Lieksa
      36
      568

    8. Minne katosi Sofian Jeff-rakas ystävä?

      Seiskalehden mukaan Jeffreytä ei ole näkynyt, kuin kesäkuussa maininta Sofian ommissassa insramissa. Onko jo tullut ero
      Kotimaiset julkkisjuorut
      144
      539

    9. Kuka hukkui

      Kuka hukkui eilen kätkytniementiellä?
      Pyhäjärvi
      6
      505

    10. Stubbin ylimielinen uho vie Suomea sotaan!!?

      https://m.youtube.com/watch?v=aQ3c540lm9o Miten voi olla että maamme presidentii toimii näin vastuuttomasti kuten hölöt
      Maailman menoa
      279
      485
    Aihe
    TietosuojaselosteKäyttöehdotEvästeasetuksetSäännöt