some code using ur/web, a language/web framework based on dependent types (ie, Coq, Agda, etc) - a login mechanism with salting (http://www.impredicative.com/ur/)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
| some demo code for ur/web, demonstrating user authentication/sessions.
- 30th december 2009 - daniel patterson (http://dbpmail.net)
- 16th december 2011 - all code that I've written is put in the public
domain. enjoy!
- 6th march 2013 - adding more code, refactoring, now into a hello
module and a userpass module
to build, run make - it will compile the c libraries (for hashing and
random numbers) and the app, which for the sake of demo-ease, uses
sqlite3.
$ make
(NOTE: this uses the absolute url for the urweb libraries - if you did
not install urweb to the default location, edit the makefile!)
and then to run it, first populate the database:
$ sqlite3 userpass.db < userpass.sql
then run it:
$ ./hello.exe
and visit in your webbrowser http://localhost:8080
you should be able to sign up, log in, log out, and see a list of all users on the system.
|